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
2024-12-24 02:15:55 +0100j1n37(~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 +0100j1n37(~j1n37@user/j1n37) j1n37
2024-12-24 02:19:35 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
2024-12-24 02:21:51 +0100weary-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 +0100geekosaurwonders 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 +0100merijn(~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 +0100tnt1(~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 +0100tnt1(~Thunderbi@user/tnt1) tnt1
2024-12-24 02:32:16 +0100califax(~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 +0100merijn(~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 +0100ft(~ft@i59F4F0F5.versanet.de) (Ping timeout: 265 seconds)
2024-12-24 02:39:53 +0100ft(~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 +0100califax(~califax@user/califx) califx
2024-12-24 02:45:38 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 02:49:57 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2024-12-24 02:52:50 +0100dsrt^(~dsrt@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 260 seconds)
2024-12-24 03:00:01 +0100dsrt^(~dsrt@c-98-242-74-66.hsd1.ga.comcast.net)
2024-12-24 03:01:02 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 03:05:42 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-12-24 03:06:03 +0100Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
2024-12-24 03:10:04 +0100rekahsoft(~rekahsoft@bras-base-orllon1103w-grc-06-76-69-85-220.dsl.bell.ca) (Remote host closed the connection)
2024-12-24 03:11:59 +0100nadja(~dequbed@banana-new.kilobyte22.de) (Ping timeout: 265 seconds)
2024-12-24 03:12:12 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds)
2024-12-24 03:12:46 +0100nadja(~dequbed@banana-new.kilobyte22.de) dequbed
2024-12-24 03:13:36 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2024-12-24 03:16:24 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 03:17:20 +0100Feuermagier(~Feuermagi@user/feuermagier) (Remote host closed the connection)
2024-12-24 03:17:40 +0100Feuermagier(~Feuermagi@user/feuermagier) Feuermagier
2024-12-24 03:18:21 +0100rekahsoft(~rekahsoft@76.69.85.220) rekahsoft
2024-12-24 03:19:17 +0100emmanuelux_(~emmanuelu@user/emmanuelux) emmanuelux
2024-12-24 03:20:54 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
2024-12-24 03:22:35 +0100emmanuelux(~emmanuelu@user/emmanuelux) (Ping timeout: 260 seconds)
2024-12-24 03:31:47 +0100merijn(~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 +0100weary-traveler(~user@user/user363627) user363627
2024-12-24 03:36:08 +0100emmanuelux_(~emmanuelu@user/emmanuelux) (Ping timeout: 252 seconds)
2024-12-24 03:40:59 +0100merijn(~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 +0100merijn(~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 +0100Feuermagier(~Feuermagi@user/feuermagier) (Remote host closed the connection)
2024-12-24 03:55:32 +0100Feuermagier(~Feuermagi@user/feuermagier) Feuermagier
2024-12-24 03:56:27 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-12-24 03:59:06 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 04:00:57 +0100Feuermagier(~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 +0100merijn(~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 +0100dsrt^(~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 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 04:14:51 +0100dsrt^(~dsrt@c-98-242-74-66.hsd1.ga.comcast.net)
2024-12-24 04:19:10 +0100merijn(~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 +0100ski. 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 +0100machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod
2024-12-24 04:26:18 +0100CrunchyFlakes(~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 +0100CrunchyFlakes(~CrunchyFl@31.19.233.78)
2024-12-24 04:29:49 +0100merijn(~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 +0100merijn(~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
2024-12-24 04:41:21 +0100rekahsoft(~rekahsoft@76.69.85.220) (Remote host closed the connection)
2024-12-24 04:41:30 +0100td_(~td@i53870924.versanet.de) (Ping timeout: 252 seconds)
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:42:04 +0100 <haskellbridge> <thirdofmay18081814goya> uh sorry the right-hand-side term
2024-12-24 04:42:08 +0100terrorjack4(~terrorjac@2a01:4f8:c17:dc9f::) (Quit: The Lounge - https://thelounge.chat)
2024-12-24 04:43:08 +0100td_(~td@i53870930.versanet.de) td_
2024-12-24 04:43:10 +0100rekahsoft(~rekahsoft@bras-base-orllon1103w-grc-06-76-69-85-220.dsl.bell.ca) rekahsoft
2024-12-24 04:43:51 +0100terrorjack4(~terrorjac@2a01:4f8:c17:dc9f::) terrorjack
2024-12-24 04:45:34 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
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:49:59 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds)
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: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: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 05:00:28 +0100machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds)
2024-12-24 05:00:55 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 05:01:11 +0100tomboy64(~tomboy64@user/tomboy64) (Read error: Connection reset by peer)
2024-12-24 05:01:22 +0100tomboy64(~tomboy64@user/tomboy64) tomboy64
2024-12-24 05:02:30 +0100 <haskellbridge> <Bowuigi> Which logic is this one? It looks interesting
2024-12-24 05:03:37 +0100rekahsoft(~rekahsoft@bras-base-orllon1103w-grc-06-76-69-85-220.dsl.bell.ca) (Remote host closed the connection)
2024-12-24 05:05:34 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
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:09:02 +0100rekahsoft(~rekahsoft@bras-base-orllon1103w-grc-06-76-69-85-220.dsl.bell.ca) rekahsoft
2024-12-24 05:10:10 +0100 <haskellbridge> <thirdofmay18081814goya> maybe (probably not) "GADTs" and something something "[]"
2024-12-24 05:10:51 +0100tomboy64(~tomboy64@user/tomboy64) (Ping timeout: 272 seconds)
2024-12-24 05:16:18 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 05:23:12 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-12-24 05:24:17 +0100tomboy64(~tomboy64@user/tomboy64) tomboy64
2024-12-24 05:24:52 +0100aforemny(~aforemny@i59F4C727.versanet.de) aforemny
2024-12-24 05:25:54 +0100aforemny_(~aforemny@2001:9e8:6cf3:d200:ed4d:2a81:f273:8171) (Ping timeout: 276 seconds)
2024-12-24 05:28:43 +0100 <haskellbridge> <Bowuigi> What's this "[]" operator? I'd assume it isn't "List"
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:32:33 +0100 <haskellbridge> <thirdofmay18081814goya> ski helpfully suggests it can be interpreted generally as "necessity" or "it is necessary"
2024-12-24 05:34:21 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 05:35:48 +0100dsrt^(~dsrt@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 244 seconds)
2024-12-24 05:37:13 +0100 <EvanR> so [] is the square modality
2024-12-24 05:37:26 +0100 <EvanR> not brackets
2024-12-24 05:37:34 +0100 <haskellbridge> <thirdofmay18081814goya> yeah sorry
2024-12-24 05:39:24 +0100 <haskellbridge> <Bowuigi> Oh it's modal logic in sequent-ish syntax
2024-12-24 05:40:21 +0100 <haskellbridge> <Bowuigi> "Unordered sequence of past effects" seems interesting
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:41:54 +0100 <haskellbridge> <thirdofmay18081814goya> i am not sure of this I am trying to find an answer
2024-12-24 05:42:00 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
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:44:09 +0100invariadic(~invariadi@2405:201:5c16:894:60cf:104f:f572:3e41)
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:45:41 +0100rekahsoft(~rekahsoft@bras-base-orllon1103w-grc-06-76-69-85-220.dsl.bell.ca) (Ping timeout: 265 seconds)
2024-12-24 05:48:10 +0100invariadic(~invariadi@2405:201:5c16:894:60cf:104f:f572:3e41) (Client Quit)
2024-12-24 05:49:20 +0100invariadic(~invariadi@2405:201:5c16:894:60cf:104f:f572:3e41)
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: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:50:56 +0100 <haskellbridge> <thirdofmay18081814goya> or some variation of these themes
2024-12-24 05:51:36 +0100 <haskellbridge> <thirdofmay18081814goya> Bowuigi: interesting! I will read these articles
2024-12-24 05:51:40 +0100 <haskellbridge> <Bowuigi> That's pretty cool
2024-12-24 05:52:17 +0100 <haskellbridge> <Bowuigi> Never saw circuits as "possibly empty types depending on time"
2024-12-24 05:52:30 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
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:56:15 +0100 <haskellbridge> <Bowuigi> t is the time here, F is the possibly empty type
2024-12-24 05:56:53 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
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 06:05:14 +0100 <haskellbridge> <Bowuigi> Notions of "past" and "future" imply this anyways
2024-12-24 06:07:52 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 06:12:20 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-12-24 06:14:01 +0100robobub(uid248673@id-248673.uxbridge.irccloud.com) robobub
2024-12-24 06:17:41 +0100xff0x(~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp)
2024-12-24 06:23:14 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 06:27:27 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
2024-12-24 06:27:57 +0100dsrt^(dsrt@c-98-242-74-66.hsd1.ga.comcast.net)
2024-12-24 06:33:55 +0100gorignak(~gorignak@user/gorignak) (Quit: quit)
2024-12-24 06:38:20 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 06:42:58 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2024-12-24 06:43:43 +0100esph(~weechat@user/esph) esph
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:51:12 +0100 <haskellbridge> ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/PBvgtawxtXnBJKOpEuWithmU/8CDgsIaqPKY (4 lines)
2024-12-24 06:53:43 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 06:58:18 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds)
2024-12-24 07:07:03 +0100chexum(~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection)
2024-12-24 07:07:17 +0100chexum(~quassel@gateway/tor-sasl/chexum) chexum
2024-12-24 07:08:15 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2024-12-24 07:09:06 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 07:16:04 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-12-24 07:21:24 +0100takuan(~takuan@178-116-218-225.access.telenet.be)
2024-12-24 07:27:19 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 07:27:59 +0100 <haskellbridge> <thirdofmay18081814goya> messed up. need to distinguish the stream and circuit types (lhs of "data ... := ...") from their constructors (rhs of "data ... := ...")
2024-12-24 07:31:54 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-12-24 07:35:10 +0100 <haskellbridge> <thirdofmay18081814goya> Bowuigi: am trying to realize this
2024-12-24 07:39:21 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 07:39:48 +0100invariadic(~invariadi@2405:201:5c16:894:60cf:104f:f572:3e41) (Remote host closed the connection)
2024-12-24 07:44:06 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-12-24 07:45:33 +0100xff0x(~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp) (Ping timeout: 265 seconds)
2024-12-24 07:54:42 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 07:59:34 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-12-24 08:00:19 +0100Guest78(~Guest78@2a02:8084:1:6500::db)
2024-12-24 08:06:12 +0100xff0x(~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp)
2024-12-24 08:10:05 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 08:15:02 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-12-24 08:25:29 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 08:29:41 +0100Sgeo(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2024-12-24 08:29:59 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds)
2024-12-24 08:40:06 +0100l_k(~student@46.61.242.35) (Ping timeout: 246 seconds)
2024-12-24 08:40:20 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 08:41:16 +0100l_k(~student@85.172.110.180)
2024-12-24 08:47:01 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2024-12-24 08:49:01 +0100CiaoSen(~Jura@2a05:5800:2d3:c700:ca4b:d6ff:fec1:99da) CiaoSen
2024-12-24 08:56:24 +0100CiaoSen(~Jura@2a05:5800:2d3:c700:ca4b:d6ff:fec1:99da) (Quit: CiaoSen)
2024-12-24 08:58:22 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 08:59:31 +0100 <iqubic> Is there a good way to get the nth bit from an integer in Haskell?
2024-12-24 09:00:01 +0100caconym(~caconym@user/caconym) (Quit: bye)
2024-12-24 09:00:34 +0100CiaoSen(~Jura@2a05:5800:2d3:c700:ca4b:d6ff:fec1:99da) CiaoSen
2024-12-24 09:00:37 +0100caconym(~caconym@user/caconym) caconym
2024-12-24 09:03:22 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-12-24 09:05:28 +0100dsrt^(dsrt@c-98-242-74-66.hsd1.ga.comcast.net) (Remote host closed the connection)
2024-12-24 09:07:25 +0100irfan(~irfan@user/irfan) irfan
2024-12-24 09:13:45 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 09:15:17 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds)
2024-12-24 09:18:36 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds)
2024-12-24 09:22:52 +0100irfan(~irfan@user/irfan) (Quit: leaving)
2024-12-24 09:29:08 +0100housemate(~housemate@pa49-185-180-187.pa.vic.optusnet.com.au) housemate
2024-12-24 09:29:08 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 09:33:49 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-12-24 09:41:20 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 09:45:02 +0100 <davean> iqubic: Bits
2024-12-24 09:45:31 +0100 <davean> iqubic: https://hackage.haskell.org/package/base-4.21.0.0/docs/Data-Bits.html#v:testBit
2024-12-24 09:45:54 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-12-24 09:46:08 +0100 <iqubic> Yeah, I want something like that, but I want to have it return either a 1 or a 0 instead of a Bool.
2024-12-24 09:46:30 +0100 <davean> I mean then shift and mask.
2024-12-24 09:46:45 +0100 <iqubic> Is there a better way of doing it than just `\x n -> if testBit x n then 1 else 0`?
2024-12-24 09:47:07 +0100 <davean> depends on your definition of better, but shift and masking if you want it non-conditionally
2024-12-24 09:47:13 +0100 <iqubic> I see.
2024-12-24 09:47:21 +0100 <iqubic> Thanks for the help
2024-12-24 09:47:54 +0100 <davean> (a `shiftR` n) .&. 0x1
2024-12-24 09:48:12 +0100 <davean> *assuming* that represents 1 in your type
2024-12-24 09:48:26 +0100 <davean> Which there *is no reason to assume*
2024-12-24 09:49:06 +0100 <davean> shift and mask is likely faster though, depending on a ton of factors.
2024-12-24 09:49:58 +0100 <iqubic> Thanks!
2024-12-24 09:51:40 +0100Guest78(~Guest78@2a02:8084:1:6500::db) (Ping timeout: 240 seconds)
2024-12-24 09:56:43 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 09:59:41 +0100weary-traveler(~user@user/user363627) (Remote host closed the connection)
2024-12-24 10:01:14 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds)
2024-12-24 10:02:49 +0100xff0x(~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp) (Ping timeout: 265 seconds)
2024-12-24 10:04:24 +0100ChaiTRex(~ChaiTRex@user/chaitrex) (Ping timeout: 264 seconds)
2024-12-24 10:06:08 +0100ChaiTRex(~ChaiTRex@user/chaitrex) ChaiTRex
2024-12-24 10:12:04 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 10:16:04 +0100billchenchina(~billchenc@103.152.35.21) billchenchina
2024-12-24 10:16:09 +0100billchenchina(~billchenc@103.152.35.21) (Remote host closed the connection)
2024-12-24 10:16:32 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-12-24 10:20:03 +0100alexherbo2(~alexherbo@2a02-8440-3504-8ae4-a87d-f91c-a611-29c0.rev.sfr.net) alexherbo2
2024-12-24 10:26:21 +0100CiaoSen(~Jura@2a05:5800:2d3:c700:ca4b:d6ff:fec1:99da) (Ping timeout: 252 seconds)
2024-12-24 10:27:15 +0100housemate(~housemate@pa49-185-180-187.pa.vic.optusnet.com.au) (Ping timeout: 260 seconds)
2024-12-24 10:27:27 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 10:28:15 +0100alexherbo2(~alexherbo@2a02-8440-3504-8ae4-a87d-f91c-a611-29c0.rev.sfr.net) (Remote host closed the connection)
2024-12-24 10:29:40 +0100L29Ah(~L29Ah@wikipedia/L29Ah) (Ping timeout: 252 seconds)
2024-12-24 10:32:35 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
2024-12-24 10:42:20 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 10:46:50 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2024-12-24 10:52:01 +0100mari-estel(~mari-este@user/mari-estel) mari-estel
2024-12-24 10:54:34 +0100tnt2(~Thunderbi@user/tnt1) tnt1
2024-12-24 10:56:28 +0100tnt1(~Thunderbi@user/tnt1) (Ping timeout: 265 seconds)
2024-12-24 10:56:28 +0100tnt2tnt1
2024-12-24 11:00:38 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 11:04:56 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-12-24 11:05:13 +0100lxsameer(~lxsameer@Serene/lxsameer) lxsameer
2024-12-24 11:06:08 +0100Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla
2024-12-24 11:11:02 +0100ljdarj(~Thunderbi@user/ljdarj) ljdarj
2024-12-24 11:16:01 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 11:16:46 +0100ash3en(~Thunderbi@p200300ef0f04dc00f0cbb9f6013f5f8e.dip0.t-ipconnect.de) ash3en
2024-12-24 11:19:11 +0100gentauro(~gentauro@user/gentauro) (Read error: Connection reset by peer)
2024-12-24 11:19:47 +0100L29Ah(~L29Ah@wikipedia/L29Ah) L29Ah
2024-12-24 11:20:38 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-12-24 11:20:58 +0100ash3en(~Thunderbi@p200300ef0f04dc00f0cbb9f6013f5f8e.dip0.t-ipconnect.de) (Client Quit)
2024-12-24 11:23:53 +0100gentauro(~gentauro@user/gentauro) gentauro
2024-12-24 11:30:15 +0100gentauro(~gentauro@user/gentauro) (Ping timeout: 260 seconds)
2024-12-24 11:30:29 +0100xff0x(~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp)
2024-12-24 11:31:24 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 11:36:36 +0100gentauro(~gentauro@user/gentauro) gentauro
2024-12-24 11:38:11 +0100__monty__(~toonn@user/toonn) toonn
2024-12-24 11:38:31 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-12-24 11:41:37 +0100gentauro_(~gentauro@cgn-cgn11-185-107-12-141.static.kviknet.net)
2024-12-24 11:41:54 +0100gentauro(~gentauro@user/gentauro) (Ping timeout: 265 seconds)
2024-12-24 11:43:21 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 11:47:35 +0100sawilagar(~sawilagar@user/sawilagar) sawilagar
2024-12-24 11:47:54 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds)
2024-12-24 11:58:42 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 11:59:01 +0100econo_(uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity)
2024-12-24 12:03:39 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-12-24 12:12:02 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 12:15:51 +0100pavonia(~user@user/siracusa) (Quit: Bye!)
2024-12-24 12:16:44 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
2024-12-24 12:16:53 +0100kuribas(~user@ptr-17d51enqg53ahlm81u8.18120a2.ip6.access.telenet.be) kuribas
2024-12-24 12:17:31 +0100AlexZenon(~alzenon@5.139.233.146) (Ping timeout: 252 seconds)
2024-12-24 12:23:25 +0100kuribas(~user@ptr-17d51enqg53ahlm81u8.18120a2.ip6.access.telenet.be) (Remote host closed the connection)
2024-12-24 12:27:24 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 12:27:27 +0100AlexZenon(~alzenon@5.139.233.146)
2024-12-24 12:31:43 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2024-12-24 12:33:07 +0100ash3en(~Thunderbi@p200300ef0f04dc00f0cbb9f6013f5f8e.dip0.t-ipconnect.de) ash3en
2024-12-24 12:33:09 +0100ash3en(~Thunderbi@p200300ef0f04dc00f0cbb9f6013f5f8e.dip0.t-ipconnect.de) (Client Quit)
2024-12-24 12:42:48 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 12:48:49 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-12-24 12:48:58 +0100sprotte24(~sprotte24@p200300d16f32ae00e0f28665918683b3.dip0.t-ipconnect.de)
2024-12-24 12:59:30 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 13:00:05 +0100caconym(~caconym@user/caconym) (Quit: bye)
2024-12-24 13:03:55 +0100caconym(~caconym@user/caconym) caconym
2024-12-24 13:04:00 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
2024-12-24 13:14:53 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 13:18:11 +0100 <hellwolf> who is also using lsp in emacs; how can I enable hlint plugin properly
2024-12-24 13:18:28 +0100 <hellwolf> it doesn't seem to have code lens warnings coming from hlint
2024-12-24 13:20:39 +0100youthlic(~Thunderbi@user/youthlic) youthlic
2024-12-24 13:21:57 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-12-24 13:24:51 +0100ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
2024-12-24 13:28:21 +0100mari-estel(~mari-este@user/mari-estel) (Quit: nelli xmas)
2024-12-24 13:32:56 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 13:37:28 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-12-24 13:42:26 +0100tnt1(~Thunderbi@user/tnt1) (Remote host closed the connection)
2024-12-24 13:43:01 +0100eL_Bart0(eL_Bart0@dietunichtguten.org) (Ping timeout: 244 seconds)
2024-12-24 13:45:20 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 13:49:51 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-12-24 13:53:35 +0100CrunchyFlakes(~CrunchyFl@31.19.233.78) (Read error: Connection reset by peer)
2024-12-24 13:56:01 +0100CrunchyFlakes(~CrunchyFl@31.19.233.78)
2024-12-24 14:00:42 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 14:04:59 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds)
2024-12-24 14:05:47 +0100takuan(~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection)
2024-12-24 14:16:04 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 14:18:07 +0100ash3en(~Thunderbi@p200300ef0f04dc00f0cbb9f6013f5f8e.dip0.t-ipconnect.de) ash3en
2024-12-24 14:20:18 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
2024-12-24 14:20:35 +0100ash3en(~Thunderbi@p200300ef0f04dc00f0cbb9f6013f5f8e.dip0.t-ipconnect.de) (Client Quit)
2024-12-24 14:25:15 +0100Nixkernal(~Nixkernal@90.74.198.178.dynamic.cust.swisscom.net) Nixkernal
2024-12-24 14:31:27 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 14:32:43 +0100ljdarj(~Thunderbi@user/ljdarj) ljdarj
2024-12-24 14:35:46 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-12-24 14:35:48 +0100tnt1(~Thunderbi@user/tnt1) tnt1
2024-12-24 14:36:09 +0100gorignak(~gorignak@user/gorignak) gorignak
2024-12-24 14:36:32 +0100califax(~califax@user/califx) (Remote host closed the connection)
2024-12-24 14:36:50 +0100califax(~califax@user/califx) califx
2024-12-24 14:45:24 +0100korrykatti(~korrykatt@user/korrykatti) korrykatti
2024-12-24 14:45:26 +0100korrykatti(~korrykatt@user/korrykatti) (Remote host closed the connection)
2024-12-24 14:46:19 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 14:49:41 +0100itaipu(~itaipu@168.121.98.246) itaipu
2024-12-24 14:52:46 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2024-12-24 15:04:23 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 15:06:30 +0100ubert(~Thunderbi@p200300ecdf117cf78af43359d271b243.dip0.t-ipconnect.de) ubert
2024-12-24 15:09:03 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2024-12-24 15:19:44 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 15:21:04 +0100hseg(~gesh@46.120.21.36)
2024-12-24 15:24:34 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
2024-12-24 15:30:21 +0100youthlic(~Thunderbi@user/youthlic) (Quit: youthlic)
2024-12-24 15:35:08 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 15:37:24 +0100 <hseg> Weirdly enough, I'm getting a type error building chs-cabal, but only on non-windows systems and on ghc 8.10.7? https://0x0.st/8rJU.txt
2024-12-24 15:40:22 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
2024-12-24 15:40:48 +0100toch(toch@user/toch) (Ping timeout: 276 seconds)
2024-12-24 15:42:40 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 15:44:22 +0100 <int-e> Looks like Cabal-3.14 is too new for this.
2024-12-24 15:44:30 +0100toch(~toch@user/toch) toch
2024-12-24 15:44:48 +0100 <int-e> for reference, GHC 8.10.7 shipped with Cabal-3.2.1
2024-12-24 15:45:25 +0100 <int-e> (well, 3.2.1.0)
2024-12-24 15:48:08 +0100toch_(toch@user/toch) toch
2024-12-24 15:48:16 +0100 <hseg> Odd that cabal tried to build chs-cabal-0.1.1.2 with Cabal-3.14.0.0 -- that is specifically listed as out-of-range on hackage
2024-12-24 15:48:48 +0100 <int-e> it's not a library dependency though, it's a build tool dependency
2024-12-24 15:49:14 +0100toch(~toch@user/toch) (Ping timeout: 272 seconds)
2024-12-24 15:49:17 +0100 <hseg> https://hackage.haskell.org/package/chs-cabal-0.1.1.2/dependencies no? it _is_ a library dep
2024-12-24 15:49:46 +0100 <int-e> Oh, looking at the wrong package
2024-12-24 15:50:06 +0100 <hseg> this build run comes from https://github.com/haskell/ghcup-hs/pull/1182
2024-12-24 15:50:06 +0100 <int-e> but (evidently) that still doesn't prevent building Setup.{l}hs with Cabal>=3.14
2024-12-24 15:51:21 +0100 <int-e> And that generates a somethingPathsomething file that use that new SymbolicPath abstraction.
2024-12-24 15:51:47 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
2024-12-24 15:52:12 +0100 <int-e> IIUC
2024-12-24 15:52:35 +0100 <int-e> My reasoning is very much guided by actually having that error.
2024-12-24 15:52:45 +0100tomboy64(~tomboy64@user/tomboy64) (Ping timeout: 260 seconds)
2024-12-24 15:53:19 +0100 <hseg> hrm. who should I prod about this?
2024-12-24 15:53:24 +0100tomboy64(~tomboy64@user/tomboy64) tomboy64
2024-12-24 15:54:33 +0100 <hseg> also, why would this not cause trouble with windows?
2024-12-24 15:55:39 +0100 <hseg> ah, I see - for some reason, cabal there decided to build with Cabal-3.12.1.0
2024-12-24 15:56:09 +0100 <hseg> .. actually, I see multiple Cabals there?
2024-12-24 15:56:21 +0100 <hseg> it also builds Cabal-3.10.3.0
2024-12-24 15:56:28 +0100youthlic(~Thunderbi@user/youthlic) youthlic
2024-12-24 15:57:43 +0100 <hseg> hrm. it seems all the builds build Cabal-3.10.3.0, but windows/nonwindows differ on which newer cabal to build in addition -- 3.12.1.0 (windows, which works) or 3.14.0.0 (nonwindows, which breaks)
2024-12-24 16:02:02 +0100 <hseg> ahh -- the problem is the version of the cabal-install package these are built with, I think
2024-12-24 16:02:30 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 16:04:24 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds)
2024-12-24 16:05:10 +0100ubert(~Thunderbi@p200300ecdf117cf78af43359d271b243.dip0.t-ipconnect.de) (Ping timeout: 252 seconds)
2024-12-24 16:06:00 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2024-12-24 16:07:19 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds)
2024-12-24 16:09:11 +0100ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
2024-12-24 16:15:25 +0100 <int-e> I think what chs-cabal needs is an upper bound on its cabal-version field
2024-12-24 16:16:05 +0100 <int-e> well, for 0.1.1.2 at least
2024-12-24 16:16:51 +0100 <int-e> there's a 0.1.1.4 that works with Cabal-3.14?
2024-12-24 16:17:52 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 16:19:28 +0100 <hseg> https://hackage.haskell.org/package/chs-cabal-0.1.1.2/src/chs-cabal.cabal sets cabal-version to 1.18, so I don't _think_ that's the right place to blame?
2024-12-24 16:20:47 +0100 <hseg> indeed, https://hackage.haskell.org/package/chs-cabal-0.1.1.2/revisions/ seems to have deliberately introduced that upper bound?
2024-12-24 16:21:29 +0100 <int-e> hrm
2024-12-24 16:22:06 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
2024-12-24 16:22:15 +0100 <int-e> https://cabal.readthedocs.io/en/3.4/cabal-package.html#pkg-field-cabal-version ...okay I'm confused. There used to be a lower bound syntax here but that's discontinued.
2024-12-24 16:24:39 +0100 <int-e> I guess 3.14 should conservatively refuse to work with any package that doesn't specify cabal-version: 3.14 or later? ("refuse" - it can still build Setup executable with an older Cabal version)
2024-12-24 16:25:14 +0100 <int-e> Oh I hate the fact that DDG found docs for version 3.4.
2024-12-24 16:25:45 +0100Natch(~natch@c-92-34-7-158.bbcust.telenor.se) (Ping timeout: 252 seconds)
2024-12-24 16:26:39 +0100 <hseg> note that cabal-version is the version of the .cabal format
2024-12-24 16:26:43 +0100 <hseg> not of the build tool
2024-12-24 16:28:03 +0100 <int-e> Yes but my understanding is that the build tool semantics are not supposed to change either.
2024-12-24 16:28:30 +0100 <int-e> So if a generated file isn't backwards compatible... that's very murky.
2024-12-24 16:29:01 +0100 <int-e> Anyway, the real issue I have is that there's no way I can see to *express* that Cabal-3.14 is unfit for building that package.
2024-12-24 16:29:48 +0100 <int-e> I can live with a breaking change that only affects a few packages (using those Path modules is not too common)
2024-12-24 16:30:32 +0100 <hseg> should I perhaps post this to the cabal-install github?
2024-12-24 16:33:15 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 16:35:07 +0100Sgeo(~Sgeo@user/sgeo) Sgeo
2024-12-24 16:35:46 +0100xff0x(~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp) (Ping timeout: 265 seconds)
2024-12-24 16:40:07 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-12-24 16:45:58 +0100ljdarj(~Thunderbi@user/ljdarj) ljdarj
2024-12-24 16:48:20 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 16:52:50 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
2024-12-24 16:58:36 +0100sayurc(~sayurc@169.150.203.34) sayurc
2024-12-24 17:03:42 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 17:08:21 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2024-12-24 17:11:09 +0100JuanDaugherty(~juan@user/JuanDaugherty) JuanDaugherty
2024-12-24 17:19:05 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 17:19:59 +0100machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod
2024-12-24 17:22:46 +0100pavonia(~user@user/siracusa) siracusa
2024-12-24 17:23:34 +0100CrunchyFlakes(~CrunchyFl@31.19.233.78) (Read error: Connection reset by peer)
2024-12-24 17:23:37 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2024-12-24 17:26:01 +0100CrunchyFlakes(~CrunchyFl@31.19.233.78)
2024-12-24 17:30:52 +0100notzmv(~umar@user/notzmv) (Ping timeout: 265 seconds)
2024-12-24 17:31:54 +0100ubert(~Thunderbi@p200300ecdf117cf7bdcd23ba5c3b89f8.dip0.t-ipconnect.de) ubert
2024-12-24 17:34:28 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 17:37:34 +0100 <geekosaur> if you think you have a bug, yes. At worst someone will tell you how it's supposed to work
2024-12-24 17:37:48 +0100prasad(~Thunderbi@c-73-75-25-251.hsd1.in.comcast.net)
2024-12-24 17:38:45 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
2024-12-24 17:45:16 +0100machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds)
2024-12-24 17:49:20 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2024-12-24 17:52:43 +0100euphores(~SASL_euph@user/euphores) (Quit: Leaving.)
2024-12-24 17:53:36 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2024-12-24 17:58:42 +0100notzmv(~umar@user/notzmv) notzmv
2024-12-24 18:03:34 +0100ridcully(~ridcully@p57b52ec2.dip0.t-ipconnect.de) (Quit: WeeChat 4.4.2)
2024-12-24 18:03:52 +0100ridcully(~ridcully@p57b52ec2.dip0.t-ipconnect.de) ridcully
2024-12-24 18:04:42 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn