Newest at the top
| 2024-12-24 05:49:38 +0100 | <haskellbridge> | ... "term :: diamond T" could mean: T is an empty type at the moment but there exists a point in time in the future where it is not empty. |
| 2024-12-24 05:49:33 +0100 | <haskellbridge> | <thirdofmay18081814goya> in the frp context above the following is one possible interpretation. generally " (T : Type) |- term : T" can be interpreted as the statement that "T" is a nonempty type, but in an frp circuit whose context is on a timeline it could be interpreted as: at the moment, "T" is a nonempty type. then, "term :: box T" could mean: since the beginning and until the end, "T" is a nonempty type. finally,... |
| 2024-12-24 05:49:20 +0100 | invariadic | (~invariadi@2405:201:5c16:894:60cf:104f:f572:3e41) |
| 2024-12-24 05:48:10 +0100 | invariadic | (~invariadi@2405:201:5c16:894:60cf:104f:f572:3e41) (Client Quit) |
| 2024-12-24 05:45:41 +0100 | rekahsoft | (~rekahsoft@bras-base-orllon1103w-grc-06-76-69-85-220.dsl.bell.ca) (Ping timeout: 265 seconds) |
| 2024-12-24 05:45:17 +0100 | <haskellbridge> | <Bowuigi> Or more generally, http://www.danielgratzer.com/papers/multimodal-dependent-type-theory.pdf |
| 2024-12-24 05:44:09 +0100 | invariadic | (~invariadi@2405:201:5c16:894:60cf:104f:f572:3e41) |
| 2024-12-24 05:43:34 +0100 | <haskellbridge> | <Bowuigi> Also how relevant is https://www.researchgate.net/publication/334752231_Implementing_a_modal_dependent_type_theory |
| 2024-12-24 05:42:00 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-12-24 05:41:54 +0100 | <haskellbridge> | <thirdofmay18081814goya> i am not sure of this I am trying to find an answer |
| 2024-12-24 05:41:25 +0100 | <haskellbridge> | <Bowuigi> Also is no modality a sort of middleground between "<>" and "[]"? Or is it a sort of modality polymorphism |
| 2024-12-24 05:40:21 +0100 | <haskellbridge> | <Bowuigi> "Unordered sequence of past effects" seems interesting |
| 2024-12-24 05:39:24 +0100 | <haskellbridge> | <Bowuigi> Oh it's modal logic in sequent-ish syntax |
| 2024-12-24 05:37:34 +0100 | <haskellbridge> | <thirdofmay18081814goya> yeah sorry |
| 2024-12-24 05:37:26 +0100 | <EvanR> | not brackets |
| 2024-12-24 05:37:13 +0100 | <EvanR> | so [] is the square modality |
| 2024-12-24 05:35:48 +0100 | dsrt^ | (~dsrt@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 244 seconds) |
| 2024-12-24 05:34:21 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 05:32:33 +0100 | <haskellbridge> | <thirdofmay18081814goya> ski helpfully suggests it can be interpreted generally as "necessity" or "it is necessary" |
| 2024-12-24 05:32:09 +0100 | <haskellbridge> | <thirdofmay18081814goya> it has no objective meaning (can be given multiple meanings, see the ski comment I quote) but in the syntax above it encodes either an unordered sequence of past effects. the quoted comment itself quotes where ski gives the comonadic laws it satisfies |
| 2024-12-24 05:28:43 +0100 | <haskellbridge> | <Bowuigi> What's this "[]" operator? I'd assume it isn't "List" |
| 2024-12-24 05:25:54 +0100 | aforemny_ | (~aforemny@2001:9e8:6cf3:d200:ed4d:2a81:f273:8171) (Ping timeout: 276 seconds) |
| 2024-12-24 05:24:52 +0100 | aforemny | (~aforemny@i59F4C727.versanet.de) aforemny |
| 2024-12-24 05:24:17 +0100 | tomboy64 | (~tomboy64@user/tomboy64) tomboy64 |
| 2024-12-24 05:23:12 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-24 05:16:18 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 05:10:51 +0100 | tomboy64 | (~tomboy64@user/tomboy64) (Ping timeout: 272 seconds) |
| 2024-12-24 05:10:10 +0100 | <haskellbridge> | <thirdofmay18081814goya> maybe (probably not) "GADTs" and something something "[]" |
| 2024-12-24 05:09:02 +0100 | rekahsoft | (~rekahsoft@bras-base-orllon1103w-grc-06-76-69-85-220.dsl.bell.ca) rekahsoft |
| 2024-12-24 05:07:59 +0100 | <haskellbridge> | <thirdofmay18081814goya> hm the above syntax could be interpreted in a dependently-typed type theory extended with only "[] : Type -> Type" or some form of higher order intuitionistic logic with a "[]" operator |
| 2024-12-24 05:05:34 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 05:03:37 +0100 | rekahsoft | (~rekahsoft@bras-base-orllon1103w-grc-06-76-69-85-220.dsl.bell.ca) (Remote host closed the connection) |
| 2024-12-24 05:02:30 +0100 | <haskellbridge> | <Bowuigi> Which logic is this one? It looks interesting |
| 2024-12-24 05:01:22 +0100 | tomboy64 | (~tomboy64@user/tomboy64) tomboy64 |
| 2024-12-24 05:01:11 +0100 | tomboy64 | (~tomboy64@user/tomboy64) (Read error: Connection reset by peer) |
| 2024-12-24 05:00:55 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 05:00:28 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 2024-12-24 04:56:33 +0100 | <haskellbridge> | <thirdofmay18081814goya> i.e., what we know from "[] Gamma" is that there is an frp circuit that will produce it, but we don't know the exact network configuration info that tells us which circuit precisely it is that will produce it |
| 2024-12-24 04:51:35 +0100 | <haskellbridge> | <thirdofmay18081814goya> uh not sure if that notation encodes it very well, but from "[] Gamma" we can infer that there exists a "frpCircuit :: [Chain]" that has "(\x -> [] x) frpCircuit = [] Gamma" |
| 2024-12-24 04:50:15 +0100 | <haskellbridge> | <thirdofmay18081814goya> a valid inference however would be something like "[] Gamma |- e : Exists (x :: [Chain]). [] x = [] Gamma" |
| 2024-12-24 04:49:59 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-12-24 04:45:43 +0100 | <haskellbridge> | <thirdofmay18081814goya> whoops, mistake on second interpretation equation, is wrong "lengthOf ([] Gamma) = lengthOf (Gamma |-)", it is instead "lengthOf ([] Gamma) = lengthOf $ removeIdenticalTerms (Gamma |-)" |
| 2024-12-24 04:45:34 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 04:43:51 +0100 | terrorjack4 | (~terrorjac@2a01:4f8:c17:dc9f::) terrorjack |
| 2024-12-24 04:43:10 +0100 | rekahsoft | (~rekahsoft@bras-base-orllon1103w-grc-06-76-69-85-220.dsl.bell.ca) rekahsoft |
| 2024-12-24 04:43:08 +0100 | td_ | (~td@i53870930.versanet.de) td_ |
| 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) |