2024/12/24

2024-12-24 00:05:25 +0100son0p(~ff@186.121.98.118) (Ping timeout: 252 seconds)
2024-12-24 00:05:55 +0100chexum(~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection)
2024-12-24 00:05:56 +0100ChaiTRex(~ChaiTRex@user/chaitrex) (Remote host closed the connection)
2024-12-24 00:06:01 +0100califax(~califax@user/califx) (Read error: Connection reset by peer)
2024-12-24 00:06:11 +0100chexum(~quassel@gateway/tor-sasl/chexum) chexum
2024-12-24 00:06:18 +0100califax(~califax@user/califx) califx
2024-12-24 00:06:25 +0100ChaiTRex(~ChaiTRex@user/chaitrex) ChaiTRex
2024-12-24 00:06:37 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 00:09:20 +0100esph(~weechat@user/esph) (Ping timeout: 252 seconds)
2024-12-24 00:10:49 +0100merijn(~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 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 00:28:43 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds)
2024-12-24 00:29:38 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2024-12-24 00:39:02 +0100gorignak(~gorignak@user/gorignak) (Ping timeout: 252 seconds)
2024-12-24 00:39:39 +0100gorignak(~gorignak@user/gorignak) gorignak
2024-12-24 00:40:03 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 00:43:07 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds)
2024-12-24 00:45:03 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-12-24 00:46:15 +0100sawilagar(~sawilagar@user/sawilagar) (Ping timeout: 260 seconds)
2024-12-24 00:50:24 +0100emmanuelux(~emmanuelu@user/emmanuelux) emmanuelux
2024-12-24 00:50:49 +0100xff0x(~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp) (Ping timeout: 244 seconds)
2024-12-24 00:55:17 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 01:00:02 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-12-24 01:01:03 +0100Sgeo(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2024-12-24 01:03:06 +0100LearsLeary
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 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2024-12-24 01:04:21 +0100weary-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 +0100loonycyborg_(loonycybor@chantal.wesnoth.org) (Quit: ZNC - http://znc.sourceforge.net)
2024-12-24 01:10:29 +0100loonycyborg(loonycybor@wesnoth/developer/loonycyborg) loonycyborg
2024-12-24 01:10:40 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 01:12:36 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds)
2024-12-24 01:14:44 +0100Sgeo(~Sgeo@user/sgeo) Sgeo
2024-12-24 01:14:53 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2024-12-24 01:22:31 +0100rvalue(~rvalue@user/rvalue) rvalue
2024-12-24 01:26:02 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 01:30:58 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-12-24 01:31:44 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Remote host closed the connection)
2024-12-24 01:33:18 +0100statusbot(~statusbot@ec2-34-198-122-184.compute-1.amazonaws.com) (Read error: Connection reset by peer)
2024-12-24 01:33:24 +0100statusbot8(~statusbot@ec2-34-198-122-184.compute-1.amazonaws.com) statusbot
2024-12-24 01:34:59 +0100PotatoGim(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 +0100snek(sid280155@id-280155.lymington.irccloud.com) (Ping timeout: 245 seconds)
2024-12-24 01:35:49 +0100cbarrett(uid192934@id-192934.helmsley.irccloud.com) (Ping timeout: 245 seconds)
2024-12-24 01:35:49 +0100rubin55(sid666177@id-666177.lymington.irccloud.com) (Ping timeout: 245 seconds)
2024-12-24 01:35:49 +0100jonrh(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 +0100cbarrett(uid192934@id-192934.helmsley.irccloud.com) cbarrett
2024-12-24 01:38:43 +0100snek(sid280155@id-280155.lymington.irccloud.com) snek
2024-12-24 01:38:46 +0100rubin55(sid666177@id-666177.lymington.irccloud.com) rubin55
2024-12-24 01:38:54 +0100PotatoGim(sid99505@id-99505.lymington.irccloud.com) PotatoGim
2024-12-24 01:39:00 +0100jonrh(sid5185@id-5185.ilkley.irccloud.com) jonrh
2024-12-24 01:41:25 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 01:41:41 +0100sprotte24(~sprotte24@p200300d16f2af800514f7155ca1159f4.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
2024-12-24 01:45:46 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-12-24 01:47:33 +0100rvalue(~rvalue@user/rvalue) (Ping timeout: 272 seconds)
2024-12-24 01:50:40 +0100rvalue(~rvalue@user/rvalue) rvalue
2024-12-24 01:56:50 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 01:57:02 +0100Guest78(~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 +0100Feuermagier_(~Feuermagi@user/feuermagier) Feuermagier
2024-12-24 01:57:12 +0100FeuermagierGuest5199
2024-12-24 01:57:12 +0100Guest5199(~Feuermagi@user/feuermagier) (Killed (lead.libera.chat (Nickname regained by services)))
2024-12-24 01:57:12 +0100Feuermagier_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 +0100FeuermagierGuest7514
2024-12-24 02:00:42 +0100Feuermagier_(~Feuermagi@user/feuermagier) Feuermagier
2024-12-24 02:00:42 +0100Guest7514(~Feuermagi@user/feuermagier) (Killed (zirconium.libera.chat (Nickname regained by services)))
2024-12-24 02:00:42 +0100Feuermagier_Feuermagier
2024-12-24 02:00:50 +0100 <EvanR> the first ones easier
2024-12-24 02:03:19 +0100merijn(~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 +0100tnt1(~Thunderbi@user/tnt1) (Ping timeout: 246 seconds)
2024-12-24 02:07:55 +0100Feuermagier(~Feuermagi@user/feuermagier) (Read error: Connection reset by peer)
2024-12-24 02:08:09 +0100tnt1(~Thunderbi@user/tnt1) tnt1
2024-12-24 02:08:11 +0100Feuermagier(~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 +0100poscat0x04(~poscat@user/poscat) (Quit: Bye)
2024-12-24 02:10:37 +0100acidjnk_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 +0100poscat(~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 +0100ljdarj(~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 +0100son0p(~ff@186.121.100.67) son0p
2024-12-24 02:13:56 +0100acidjnk_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 +0100merijn(~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