| 2024-12-24 00:05:25 +0100 | son0p | (~ff@186.121.98.118) (Ping timeout: 252 seconds) |
| 2024-12-24 00:05:55 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2024-12-24 00:05:56 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2024-12-24 00:06:01 +0100 | califax | (~califax@user/califx) (Read error: Connection reset by peer) |
| 2024-12-24 00:06:11 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) chexum |
| 2024-12-24 00:06:18 +0100 | califax | (~califax@user/califx) califx |
| 2024-12-24 00:06:25 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2024-12-24 00:06:37 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 00:09:20 +0100 | esph | (~weechat@user/esph) (Ping timeout: 252 seconds) |
| 2024-12-24 00:10:49 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-12-24 00:11:40 +0100 | <hellwolf> | ski, show instance is actually "correct", I am sticking a weird domain where U256 means 256 bits. |
| 2024-12-24 00:11:40 +0100 | <hellwolf> | and thanks for your hint using case of, the TH code is actually quite easy, I have it done: https://play.haskell.org/saved/Hdf3hnIp |
| 2024-12-24 00:12:41 +0100 | <hellwolf> | still feel herculean, but now that I wrote couple of big TH code, it feels rather mechanical |
| 2024-12-24 00:22:00 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 00:28:43 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-12-24 00:29:38 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2024-12-24 00:39:02 +0100 | gorignak | (~gorignak@user/gorignak) (Ping timeout: 252 seconds) |
| 2024-12-24 00:39:39 +0100 | gorignak | (~gorignak@user/gorignak) gorignak |
| 2024-12-24 00:40:03 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 00:43:07 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 2024-12-24 00:45:03 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 00:46:15 +0100 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 260 seconds) |
| 2024-12-24 00:50:24 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) emmanuelux |
| 2024-12-24 00:50:49 +0100 | xff0x | (~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp) (Ping timeout: 244 seconds) |
| 2024-12-24 00:55:17 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 01:00:02 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 01:01:03 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-12-24 01:03:06 +0100 | Lears | Leary |
| 2024-12-24 01:03:11 +0100 | <haskellbridge> | <thirdofmay18081814goya> ski: these comments have suddenly made sense to me, thank you very much again! |
| 2024-12-24 01:03:17 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2024-12-24 01:04:21 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2024-12-24 01:05:59 +0100 | <haskellbridge> | <thirdofmay18081814goya> it suddenly made sense because as I was thinking about FRP, I realized, under the interpretation you give "[] Gamma |- A -> [] Gamma |- [] A" encodes that "[] Gamma" is sequence-independent in allowing the circuit to propagate to the next term, "A" |
| 2024-12-24 01:07:36 +0100 | <haskellbridge> | <thirdofmay18081814goya> i.e., that implication provides the semantics for: "it doesn't matter the order in which you evaluate/propagate through this part of the secret, it will yield "A" anyways |
| 2024-12-24 01:07:45 +0100 | <haskellbridge> | <thirdofmay18081814goya> * anyways" |
| 2024-12-24 01:08:02 +0100 | <haskellbridge> | <thirdofmay18081814goya> of the context*, don't know why I said of the secret |
| 2024-12-24 01:10:17 +0100 | loonycyborg_ | (loonycybor@chantal.wesnoth.org) (Quit: ZNC - http://znc.sourceforge.net) |
| 2024-12-24 01:10:29 +0100 | loonycyborg | (loonycybor@wesnoth/developer/loonycyborg) loonycyborg |
| 2024-12-24 01:10:40 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 01:12:36 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 2024-12-24 01:14:44 +0100 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2024-12-24 01:14:53 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-12-24 01:22:31 +0100 | rvalue | (~rvalue@user/rvalue) rvalue |
| 2024-12-24 01:26:02 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 01:30:58 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 01:31:44 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Remote host closed the connection) |
| 2024-12-24 01:33:18 +0100 | statusbot | (~statusbot@ec2-34-198-122-184.compute-1.amazonaws.com) (Read error: Connection reset by peer) |
| 2024-12-24 01:33:24 +0100 | statusbot8 | (~statusbot@ec2-34-198-122-184.compute-1.amazonaws.com) statusbot |
| 2024-12-24 01:34:59 +0100 | PotatoGim | (sid99505@id-99505.lymington.irccloud.com) (Ping timeout: 245 seconds) |
| 2024-12-24 01:35:04 +0100 | <loonycyborg> | what would be the best way currently to make a compile-time mapping from strings to types? |
| 2024-12-24 01:35:49 +0100 | snek | (sid280155@id-280155.lymington.irccloud.com) (Ping timeout: 245 seconds) |
| 2024-12-24 01:35:49 +0100 | cbarrett | (uid192934@id-192934.helmsley.irccloud.com) (Ping timeout: 245 seconds) |
| 2024-12-24 01:35:49 +0100 | rubin55 | (sid666177@id-666177.lymington.irccloud.com) (Ping timeout: 245 seconds) |
| 2024-12-24 01:35:49 +0100 | jonrh | (sid5185@id-5185.ilkley.irccloud.com) (Ping timeout: 245 seconds) |
| 2024-12-24 01:37:20 +0100 | <loonycyborg> | seems use case I have in mind mostly asks for "extensible records", but I don't care about order at all |
| 2024-12-24 01:38:41 +0100 | cbarrett | (uid192934@id-192934.helmsley.irccloud.com) cbarrett |
| 2024-12-24 01:38:43 +0100 | snek | (sid280155@id-280155.lymington.irccloud.com) snek |
| 2024-12-24 01:38:46 +0100 | rubin55 | (sid666177@id-666177.lymington.irccloud.com) rubin55 |
| 2024-12-24 01:38:54 +0100 | PotatoGim | (sid99505@id-99505.lymington.irccloud.com) PotatoGim |
| 2024-12-24 01:39:00 +0100 | jonrh | (sid5185@id-5185.ilkley.irccloud.com) jonrh |
| 2024-12-24 01:41:25 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 01:41:41 +0100 | sprotte24 | (~sprotte24@p200300d16f2af800514f7155ca1159f4.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 2024-12-24 01:45:46 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-24 01:47:33 +0100 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 272 seconds) |
| 2024-12-24 01:50:40 +0100 | rvalue | (~rvalue@user/rvalue) rvalue |
| 2024-12-24 01:56:50 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 01:57:02 +0100 | Guest78 | (~Guest78@2a02:8084:1:6500::db) (Quit: Client closed) |
| 2024-12-24 01:57:02 +0100 | <monochrom> | GHC has type-level string literals. |
| 2024-12-24 01:57:12 +0100 | Feuermagier_ | (~Feuermagi@user/feuermagier) Feuermagier |
| 2024-12-24 01:57:12 +0100 | Feuermagier | Guest5199 |
| 2024-12-24 01:57:12 +0100 | Guest5199 | (~Feuermagi@user/feuermagier) (Killed (lead.libera.chat (Nickname regained by services))) |
| 2024-12-24 01:57:12 +0100 | Feuermagier_ | Feuermagier |
| 2024-12-24 01:59:24 +0100 | <EvanR> | yes the string itself is a type of kind Symbol |
| 2024-12-24 02:00:31 +0100 | <EvanR> | there's "I don't care about order" and "we need the types to enforce nobody not even god can care about order" |
| 2024-12-24 02:00:42 +0100 | Feuermagier | Guest7514 |
| 2024-12-24 02:00:42 +0100 | Feuermagier_ | (~Feuermagi@user/feuermagier) Feuermagier |
| 2024-12-24 02:00:42 +0100 | Guest7514 | (~Feuermagi@user/feuermagier) (Killed (zirconium.libera.chat (Nickname regained by services))) |
| 2024-12-24 02:00:42 +0100 | Feuermagier_ | Feuermagier |
| 2024-12-24 02:00:50 +0100 | <EvanR> | the first ones easier |
| 2024-12-24 02:03:19 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-12-24 02:03:23 +0100 | <loonycyborg> | I was thinking more of " I don't care about order so I can do hashmap" but not sure how it applies to compile-time |
| 2024-12-24 02:06:09 +0100 | <loonycyborg> | Seems I can use string literals at compile time with -XDataKinds and -XTypeFamilies but not sure if it's best way currently |
| 2024-12-24 02:06:24 +0100 | <loonycyborg> | or how I can extract things back to runtime when needed |
| 2024-12-24 02:07:45 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 246 seconds) |
| 2024-12-24 02:07:55 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) (Read error: Connection reset by peer) |
| 2024-12-24 02:08:09 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
| 2024-12-24 02:08:11 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) Feuermagier |
| 2024-12-24 02:08:11 +0100 | <loonycyborg> | this really reminds me of C++ template magic though |
| 2024-12-24 02:08:51 +0100 | poscat0x04 | (~poscat@user/poscat) (Quit: Bye) |
| 2024-12-24 02:10:37 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f41b013a429fe4b7686.dip0.t-ipconnect.de) |
| 2024-12-24 02:11:03 +0100 | <geekosaur> | KnownSymbol and singletons (blech) |
| 2024-12-24 02:11:27 +0100 | <geekosaur> | you really want Idris or Agda; Haskell doesn't have a real dependent types story as yet |
| 2024-12-24 02:11:58 +0100 | <geekosaur> | ("dependent types" = types that depend on runtime values, not just the other way around) |
| 2024-12-24 02:12:11 +0100 | poscat | (~poscat@user/poscat) poscat |
| 2024-12-24 02:13:13 +0100 | <EvanR> | KnownSymbol lets you have the corresponding String at runtime |
| 2024-12-24 02:13:19 +0100 | <geekosaur> | also Haskell's type system isn't really up to things like hashmaps; the best it can do is linked lists |
| 2024-12-24 02:13:20 +0100 | <EvanR> | similar to KnownNat |
| 2024-12-24 02:13:30 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 2024-12-24 02:13:53 +0100 | <loonycyborg> | I was thinking to use array at runtime and calculate indices for it at runtime |
| 2024-12-24 02:13:53 +0100 | son0p | (~ff@186.121.100.67) son0p |
| 2024-12-24 02:13:56 +0100 | acidjnk_new | (~acidjnk@p200300d6e7283f25e9e9d221c37061e3.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 2024-12-24 02:14:03 +0100 | <loonycyborg> | at *compile time |
| 2024-12-24 02:14:07 +0100 | <EvanR> | if you're feeling nuts you might have success implementing a binary tree in the type system which serves the same purpose |
| 2024-12-24 02:14:21 +0100 | <EvanR> | but a list is probably the most realistic |
| 2024-12-24 02:14:52 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 02:14:57 +0100 | <EvanR> | if you literally don't care about order, then a list still works |
| 2024-12-24 02:15:55 +0100 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2024-12-24 02:15:57 +0100 | <loonycyborg> | ye but avoiding traversal of whole list would be nice |
| 2024-12-24 02:16:09 +0100 | <loonycyborg> | at least at runtime |
| 2024-12-24 02:16:26 +0100 | <EvanR> | it's not at runtime |
| 2024-12-24 02:16:37 +0100 | <EvanR> | or so I thought |
| 2024-12-24 02:18:24 +0100 | <loonycyborg> | ye I want to build mapping at compile time but make runtime structures based on it |
| 2024-12-24 02:19:01 +0100 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2024-12-24 02:19:35 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-12-24 02:21:51 +0100 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2024-12-24 02:23:24 +0100 | __monty__ | (~toonn@user/toonn) (Quit: Lost terminal) |
| 2024-12-24 02:24:34 +0100 | <EvanR> | and (before all that) verify what you plan to do at runtime makes any damn sense, which is where it gets complicated |
| 2024-12-24 02:24:59 +0100 | <EvanR> | any reasoning pattern you use must be reflected in the type system |
| 2024-12-24 02:25:34 +0100 | <EvanR> | or reasoning metapattern |
| 2024-12-24 02:25:36 +0100 | <geekosaur> | can you do something like reflecting a type level list into a runtime Vector? |
| 2024-12-24 02:25:52 +0100 | <geekosaur> | you'll need to think through what exactly you're doing to make that decision |
| 2024-12-24 02:26:43 +0100 | <loonycyborg> | current idea is to make mapping of strings to types at compile time then make some kind of structure that can be looked up by that string to get value of appropriate type |
| 2024-12-24 02:27:05 +0100 | <EvanR> | Symbols are already types and look like strings |
| 2024-12-24 02:27:23 +0100 | geekosaur | wonders if this is just a dependent map |
| 2024-12-24 02:27:31 +0100 | <haskellbridge> | <thirdofmay18081814goya> how many constructors does your type have? |
| 2024-12-24 02:27:32 +0100 | <geekosaur> | there's packages on Hackage for that already |
| 2024-12-24 02:27:39 +0100 | <EvanR> | was going to suggest looking at how dependent map works, which is already a library |
| 2024-12-24 02:27:48 +0100 | <EvanR> | but was too slow |
| 2024-12-24 02:28:03 +0100 | <loonycyborg> | HList seems to mostly fit |
| 2024-12-24 02:28:31 +0100 | <loonycyborg> | but they all seem to be abandoned by devs with version numbers before 1.0 |
| 2024-12-24 02:28:41 +0100 | <haskellbridge> | <thirdofmay18081814goya> are these any strings or a specific set of strings? |
| 2024-12-24 02:29:36 +0100 | <loonycyborg> | strings are determined by app or modules so it's pretty specific |
| 2024-12-24 02:29:50 +0100 | <Leary> | loonycyborg: There are also packages on hackage for vector/array backed extensible records. As for version numbers, being <1 doesn't mean anything. |
| 2024-12-24 02:30:14 +0100 | <haskellbridge> | <thirdofmay18081814goya> loonycyborg: and what is the target type? |
| 2024-12-24 02:30:15 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 02:30:34 +0100 | <loonycyborg> | each string has own type specified by app or module |
| 2024-12-24 02:30:51 +0100 | <loonycyborg> | but actual values could be got from command line and other places |
| 2024-12-24 02:30:53 +0100 | <EvanR> | loonycyborg, a lot of those libraries do exactly what they intended and have no need to keep updating |
| 2024-12-24 02:31:15 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 260 seconds) |
| 2024-12-24 02:31:31 +0100 | <EvanR> | it's not like shovelware apps that get kicked off the app store if the dev doesn't change *something* every month |
| 2024-12-24 02:31:35 +0100 | <haskellbridge> | <thirdofmay18081814goya> loonycyborg: that type is actually equivalent to the finite type counting the number of modules/app |
| 2024-12-24 02:31:37 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
| 2024-12-24 02:32:16 +0100 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2024-12-24 02:32:21 +0100 | <haskellbridge> | <thirdofmay18081814goya> i.e. the finite type whose size is the number of modules/apps will be equivalent to the type you seek |
| 2024-12-24 02:33:55 +0100 | <haskellbridge> | <thirdofmay18081814goya> quite literally: you will not be able to do a thing with the "TypeFrom String" that you can't do with the finite type counting the number of modules/apps |
| 2024-12-24 02:35:01 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-24 02:35:34 +0100 | <haskellbridge> | <thirdofmay18081814goya> * subtype of "TypeFrom String" that you're looking for |
| 2024-12-24 02:37:44 +0100 | <loonycyborg> | ye list size would be most definitely finite, app and modules will have to define variables they want to see as string->value mappings and they will have to be merged into single mapping |
| 2024-12-24 02:38:01 +0100 | <loonycyborg> | then total size would be known and indices could be assigned |
| 2024-12-24 02:38:09 +0100 | ft | (~ft@i59F4F0F5.versanet.de) (Ping timeout: 265 seconds) |
| 2024-12-24 02:39:53 +0100 | ft | (~ft@i59F4F055.versanet.de) ft |
| 2024-12-24 02:40:34 +0100 | <haskellbridge> | <thirdofmay18081814goya> do note that the string-indexing of a type here is not doing any "work" so to say |
| 2024-12-24 02:40:53 +0100 | <loonycyborg> | Basically I want to make a typesafe variant of system environment, and other structures that are inspired by it in some buildsystems :P |
| 2024-12-24 02:43:09 +0100 | califax | (~califax@user/califx) califx |
| 2024-12-24 02:45:38 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 02:49:57 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-12-24 02:52:50 +0100 | dsrt^ | (~dsrt@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 260 seconds) |
| 2024-12-24 03:00:01 +0100 | dsrt^ | (~dsrt@c-98-242-74-66.hsd1.ga.comcast.net) |
| 2024-12-24 03:01:02 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 03:05:42 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 03:06:03 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-12-24 03:10:04 +0100 | rekahsoft | (~rekahsoft@bras-base-orllon1103w-grc-06-76-69-85-220.dsl.bell.ca) (Remote host closed the connection) |
| 2024-12-24 03:11:59 +0100 | nadja | (~dequbed@banana-new.kilobyte22.de) (Ping timeout: 265 seconds) |
| 2024-12-24 03:12:12 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
| 2024-12-24 03:12:46 +0100 | nadja | (~dequbed@banana-new.kilobyte22.de) dequbed |
| 2024-12-24 03:13:36 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2024-12-24 03:16:24 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 03:17:20 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) (Remote host closed the connection) |
| 2024-12-24 03:17:40 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) Feuermagier |
| 2024-12-24 03:18:21 +0100 | rekahsoft | (~rekahsoft@76.69.85.220) rekahsoft |
| 2024-12-24 03:19:17 +0100 | emmanuelux_ | (~emmanuelu@user/emmanuelux) emmanuelux |
| 2024-12-24 03:20:54 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-12-24 03:22:35 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) (Ping timeout: 260 seconds) |
| 2024-12-24 03:31:47 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 03:33:03 +0100 | _leo___ | (~emmanuelu@user/emmanuelux) emmanuelux |
| 2024-12-24 03:34:44 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2024-12-24 03:36:08 +0100 | emmanuelux_ | (~emmanuelu@user/emmanuelux) (Ping timeout: 252 seconds) |
| 2024-12-24 03:40:59 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 03:45:40 +0100 | <ski> | thirdofmay18081814goya : hm, not sure i follow that FRP interpretation |
| 2024-12-24 03:46:02 +0100 | <haskellbridge> | <thirdofmay18081814goya> it was slightly wrongly formulated |
| 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:51:29 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 03:53:05 +0100 | <haskellbridge> | <thirdofmay18081814goya> "[] Gamma" contains significantly less information than "Gamma" |
| 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:54:55 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) (Remote host closed the connection) |
| 2024-12-24 03:55:32 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) Feuermagier |
| 2024-12-24 03:56:27 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-12-24 03:59:06 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 04:00:57 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) (Quit: Leaving) |
| 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:02:00 +0100 | <haskellbridge> | ... CurrentViewport -> (ScreenCoordinates -> Color)" |
| 2024-12-24 04:03:38 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 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:04:20 +0100 | <haskellbridge> | ... "CurrentViewport". we only need their output signal |
| 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: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:08:06 +0100 | <haskellbridge> | <thirdofmay18081814goya> so your comments were very opportune heheh |
| 2024-12-24 04:13:12 +0100 | _leo___ | (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 2024-12-24 04:14:24 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-24 04:14:51 +0100 | dsrt^ | (~dsrt@c-98-242-74-66.hsd1.ga.comcast.net) |
| 2024-12-24 04:19:10 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 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:21:03 +0100 | <ski> | er |
| 2024-12-24 04:21:06 +0100 | <ski> | thirdofmay18081814goya ^ |
| 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:24:58 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2024-12-24 04:26:18 +0100 | CrunchyFlakes | (~CrunchyFl@ip1f13e94e.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 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:28:46 +0100 | CrunchyFlakes | (~CrunchyFl@31.19.233.78) |
| 2024-12-24 04:29:49 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 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: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:48 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-24 04:35:03 +0100 | <ski> | (but i'm probably not following the FRP context here that well ..) |
| 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: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 |