Newest at the top
| 2024-12-24 04:42:08 +0100 | terrorjack4 | (~terrorjac@2a01:4f8:c17:dc9f::) (Quit: The Lounge - https://thelounge.chat) |
| 2024-12-24 04:42:04 +0100 | <haskellbridge> | <thirdofmay18081814goya> uh sorry the right-hand-side term |
| 2024-12-24 04:41:48 +0100 | <haskellbridge> | <thirdofmay18081814goya> to truly recapture our original context, the left-hand-side term "Gamma" in "[] Gamma |- Gamma" must in fact specify a partial order, which has type "[Chain]" |
| 2024-12-24 04:41:30 +0100 | td_ | (~td@i53870924.versanet.de) (Ping timeout: 252 seconds) |
| 2024-12-24 04:41:21 +0100 | rekahsoft | (~rekahsoft@76.69.85.220) (Remote host closed the connection) |
| 2024-12-24 04:40:52 +0100 | <haskellbridge> | ... |-)" to a type (effectively a projection function with extracts the type from the pair. But this is just a product type which does not carry any meaningful network configuration information! The second possible interpretation is "Gamma :: (varSymbol, Type) -> varSymbol, Type -> ..." which is a "lengthOf ([] Gamma) = lengthOf (Gamma |-)" function which can only encode a singular, totally ordered sequence of signals |
| 2024-12-24 04:40:46 +0100 | <haskellbridge> | <thirdofmay18081814goya> ski: I don't think so! it seems to me that "Gamma" is a syntactic abbreviation and not a term, so "|- Gamma" is not well defined, but we can attempt to give it two macro-expansions into a well-formed term. A first possibility is "Gamma :: Finite (lengthOf ([] Gamma)) -> Type", which associates the (lengthOf ([] Gamma) 'th pair in "macroExpand ([] Gamma)" or "removeIdenticalTerms $ macroExpand (Gamma... |
| 2024-12-24 04:35:03 +0100 | <ski> | (but i'm probably not following the FRP context here that well ..) |
| 2024-12-24 04:34:48 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-24 04:34:44 +0100 | <ski> | (also not sure if i should interpret `ButtonStates >-> ComponentStates >-> IndexedLayout >-> CurrentViewport >-> (ScreenCoordinates -> Color)' as a sequence/graph with five nodes, the last of which is a function type ?) |
| 2024-12-24 04:34:18 +0100 | <ski> | (also not sure if i should interpret `ButtonStates >-> ComponentStates >-> IndexedLayout >-> CurrentViewport -> (ScreenCoordinates -> Color) |
| 2024-12-24 04:29:49 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 04:28:46 +0100 | CrunchyFlakes | (~CrunchyFl@31.19.233.78) |
| 2024-12-24 04:28:26 +0100 | <ski> | ("there is nothing that prevents us from duplicating that signal and also sending it forward in the circuit" -- sounds like comonadic preservation of context, if `[] A |- B', then `[] A |- [] B', `Comonad w => (w a -> b) -> (w a -> w b)') |
| 2024-12-24 04:26:18 +0100 | CrunchyFlakes | (~CrunchyFl@ip1f13e94e.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-12-24 04:24:58 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2024-12-24 04:24:17 +0100 | ski | . o O ( <https://en.wikipedia.org/wiki/L%C3%B6b's_theorem>,<https://en.wikipedia.org/wiki/Curry%27s_paradox>,<https://en.wikipedia.org/wiki/Provability_logic>,<https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems> ) |
| 2024-12-24 04:21:06 +0100 | <ski> | thirdofmay18081814goya ^ |
| 2024-12-24 04:21:03 +0100 | <ski> | er |
| 2024-12-24 04:20:54 +0100 | <ski> | haskellbridge : hm, but wouldn't `[] Gamma |- Gamma' also hold (if `[]' is a "neccesary"-type modality) (this is not true in provability logic, a modal logic explored by George Boolos in "The Logic of Provability", related to stuff like Gödel's incompleteness theorems, and Löb/Curry's theorem), so how can `[] Gamma' then be weaker than `Gamma' ? |
| 2024-12-24 04:19:10 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 04:14:51 +0100 | dsrt^ | (~dsrt@c-98-242-74-66.hsd1.ga.comcast.net) |
| 2024-12-24 04:14:24 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 04:13:12 +0100 | _leo___ | (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 2024-12-24 04:08:06 +0100 | <haskellbridge> | <thirdofmay18081814goya> so your comments were very opportune heheh |
| 2024-12-24 04:07:11 +0100 | <haskellbridge> | <thirdofmay18081814goya> and this is in fact so: if "CurrentViewport" consumes a signal from "IndexedLayout", there is nothing that prevents us from duplicating that signal and also sending it forward in the circuit |
| 2024-12-24 04:07:04 +0100 | dsrt^ | (~dsrt@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 245 seconds) |
| 2024-12-24 04:04:20 +0100 | <haskellbridge> | ... "CurrentViewport". we only need their output signal |
| 2024-12-24 04:04:15 +0100 | <haskellbridge> | <thirdofmay18081814goya> then I worried a bit about whether this was a good implementation or a good network configuration or the unique way to obtain that particular function. but if this function is 100% reactive, then we can correctly infer "[] Gamma |- A", i.e., the reactive semantics of this configuration are not affected by the exact order of the signal functions "ButtonStates", "ComponentStates", "IndexedLayout",... |
| 2024-12-24 04:03:38 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-24 04:02:00 +0100 | <haskellbridge> | ... CurrentViewport -> (ScreenCoordinates -> Color)" |
| 2024-12-24 04:01:54 +0100 | <haskellbridge> | <thirdofmay18081814goya> i accidentally stumbled on this while trying to model an frp circuit and realized it has an extremely practical application: i was interested in having my circuit produce an "A" (more specifically, "ScreenCoordinates -> Color"), and realized that it could be constructed from a particular sequence of signals that looked something like "ButtonStates -> ComponentStates -> IndexedLayout ->... |
| 2024-12-24 04:00:57 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) (Quit: Leaving) |
| 2024-12-24 03:59:06 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 03:56:27 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 03:55:32 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) Feuermagier |
| 2024-12-24 03:54:55 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) (Remote host closed the connection) |
| 2024-12-24 03:54:31 +0100 | <haskellbridge> | <thirdofmay18081814goya> but realizes an equivalence relation on (some) permutations of the chains in the partial order given by "Gamma" |
| 2024-12-24 03:53:05 +0100 | <haskellbridge> | <thirdofmay18081814goya> "[] Gamma" contains significantly less information than "Gamma" |
| 2024-12-24 03:51:29 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 03:50:08 +0100 | <haskellbridge> | <thirdofmay18081814goya> the right statement is, if we interpret "Gamma |- A" holds and we interpret it as: "the sequence-dependent/ordered FRP-circuit "Gamma" propagates to "A"/produces a value of type "A"", then we can infer "[] Gamma |- A", that is, the sequence-independent/unordered total output of "Gamma" is enough to know that "A" will be propagated to/produced |
| 2024-12-24 03:46:02 +0100 | <haskellbridge> | <thirdofmay18081814goya> it was slightly wrongly formulated |
| 2024-12-24 03:45:40 +0100 | <ski> | thirdofmay18081814goya : hm, not sure i follow that FRP interpretation |
| 2024-12-24 03:40:59 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 03:36:08 +0100 | emmanuelux_ | (~emmanuelu@user/emmanuelux) (Ping timeout: 252 seconds) |
| 2024-12-24 03:34:44 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2024-12-24 03:33:03 +0100 | _leo___ | (~emmanuelu@user/emmanuelux) emmanuelux |
| 2024-12-24 03:31:47 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 03:22:35 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) (Ping timeout: 260 seconds) |
| 2024-12-24 03:20:54 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |