Newest at the top
| 2024-12-24 06:12:20 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-24 06:07:52 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 06:05:14 +0100 | <haskellbridge> | <Bowuigi> Notions of "past" and "future" imply this anyways |
| 2024-12-24 06:04:36 +0100 | <haskellbridge> | <Bowuigi> Note that this induces an ordering in time, but since it doesn't imply Peano-like axioms, you can have booleans as time if you wanted |
| 2024-12-24 05:56:53 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-12-24 05:56:15 +0100 | <haskellbridge> | <Bowuigi> t is the time here, F is the possibly empty type |
| 2024-12-24 05:55:35 +0100 | <haskellbridge> | <Bowuigi> I guess one can translate each type in this fashion into a type family indexed by time, with Box being "forall t. F t" and Diamond being "exists t, t>Now. F t" given some definition for "Now" |
| 2024-12-24 05:52:30 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 05:52:17 +0100 | <haskellbridge> | <Bowuigi> Never saw circuits as "possibly empty types depending on time" |
| 2024-12-24 05:51:40 +0100 | <haskellbridge> | <Bowuigi> That's pretty cool |
| 2024-12-24 05:51:36 +0100 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: interesting! I will read these articles |
| 2024-12-24 05:50:56 +0100 | <haskellbridge> | <thirdofmay18081814goya> or some variation of these themes |
| 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 |