Newest at the top
| 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) |
| 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 ..) |