Newest at the top
| 2024-12-24 06:53:43 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 06:51:12 +0100 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/PBvgtawxtXnBJKOpEuWithmU/8CDgsIaqPKY (4 lines) |
| 2024-12-24 06:51:06 +0100 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: i have just discovered myself that it is possible to do this. in a non-modal frp setting, we can posit the context "Gamma = (mkStream : Type -> Type), (n : Nat), (worldVector abbrev wvec : Finite n -> Exists (T : Type). mkStream T), (worldClosure : (T : Type) -> mkStream T -> Exists (fin : Finite n). leftProjection (wvec fin) = T)" where "Exists ... : ... -> (..., ...)" is the dependent... |
| 2024-12-24 06:43:43 +0100 | esph | (~weechat@user/esph) esph |
| 2024-12-24 06:42:58 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-12-24 06:38:20 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 06:33:55 +0100 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
| 2024-12-24 06:27:57 +0100 | dsrt^ | (dsrt@c-98-242-74-66.hsd1.ga.comcast.net) |
| 2024-12-24 06:27:27 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-12-24 06:23:14 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 06:17:41 +0100 | xff0x | (~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp) |
| 2024-12-24 06:14:01 +0100 | robobub | (uid248673@id-248673.uxbridge.irccloud.com) robobub |
| 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 |