| 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 |