IRCBrowse

2025/01/18

2025-01-18 00:00:01 +0100 <EvanR> countable and constructible is certainly not the same thing
2025-01-18 00:00:19 +0100 <monochrom> And on second thought, I am not even sure I can take credit. My purpose was to make a newtype to allow the like of (\x -> x x), and the error message literally inspires that definition!
2025-01-18 00:00:41 +0100 <EvanR> formal languages come with grammar rules which limit you to a countable number of sentences
2025-01-18 00:00:45 +0100 <monochrom> "I thank GHC for suggesting this newtype."
2025-01-18 00:00:52 +0100 <EvanR> haskell being an example of one
2025-01-18 00:01:18 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 244 seconds)
2025-01-18 00:01:38 +0100 <haskellbridge> <thirdofmay18081814goya> right, e.g. a language with the judgment 'x is a value of type Real Number' does not have countably many statements I think
2025-01-18 00:02:04 +0100 <EvanR> that's mixing concepts
2025-01-18 00:02:23 +0100 <EvanR> jumping to another level of abstraction, beyond the syntax
2025-01-18 00:02:29 +0100paul_j(~user@8.190.187.81.in-addr.arpa) (Quit: Asta la vista)
2025-01-18 00:02:47 +0100 <monochrom> We know of at least two theories (aka models) of programming, and they disagree on countability as well as other things. The moral is that you choose a theory to suit a purpose, not for Platonic "absolute" "truth".
2025-01-18 00:02:56 +0100 <EvanR> as far as real numbers go it's a pretty nutty way to specify one xD
2025-01-18 00:03:02 +0100 <EvanR> usually you need a language for that
2025-01-18 00:03:19 +0100 <haskellbridge> <thirdofmay18081814goya> well if a theory is a set of axioms and derivable sentences, then we should admit such a language (the one having the judgment 'x is a value of type Real Number')
2025-01-18 00:04:06 +0100 <geekosaur> there are countably many values of IEEE float or double, though. you're limited to some form of "computable reals" on any physical computer
2025-01-18 00:04:12 +0100 <EvanR> is "x" there a metavariable or literally x
2025-01-18 00:04:26 +0100 <haskellbridge> <thirdofmay18081814goya> geekosaur: the computable reals are embeddable in the naturals!
2025-01-18 00:04:37 +0100 <geekosaur> yes
2025-01-18 00:04:38 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 00:04:42 +0100 <geekosaur> hence are countable
2025-01-18 00:04:43 +0100 <monochrom> And it is also related to the deal with real numbers, set theory, everything. There are countable models of ZFC, and yet there are also uncountable sets.
2025-01-18 00:04:59 +0100 <EvanR> also there's a difference between computable real and algorithmic real
2025-01-18 00:05:13 +0100 <EvanR> monochrom, yes that's what I was getting at
2025-01-18 00:05:15 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-18 00:05:34 +0100 <EvanR> uncountable is necessarily semantic
2025-01-18 00:05:55 +0100 <monochrom> You can choose a different level of abstraction (aka model) you get a different conclusion. This is supposed to be normal.
2025-01-18 00:08:12 +0100 <monochrom> I think both are necessarily semantic. But then that's a tautology. You need to choose a semantic (aka model again) before you can argue anything.
2025-01-18 00:08:49 +0100 <EvanR> sometimes something can be said about any possible semantics
2025-01-18 00:08:56 +0100 <EvanR> because you're really talking about the syntax
2025-01-18 00:09:12 +0100 <EvanR> or the logic of how you put the sentences together
2025-01-18 00:09:22 +0100 <EvanR> and never really refer to any meaning
2025-01-18 00:09:35 +0100 <EvanR> which happens in haskell sometimes
2025-01-18 00:09:43 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds)
2025-01-18 00:09:51 +0100 <monochrom> In particular if you think that you are using merely syntax trees for your argument, then you are choosing the Herbrand model, therefore it's a model, therefore it's also a semantics! There is no escape from arguing semantics
2025-01-18 00:09:59 +0100 <EvanR> when you're dealing with raw data, no IO
2025-01-18 00:10:24 +0100 <EvanR> Herbrand
2025-01-18 00:10:37 +0100 <EvanR> I'll have to look that up and hope it's not ridiculously trivial lol
2025-01-18 00:10:48 +0100 <monochrom> "It's semantics all the way down" >:)
2025-01-18 00:11:08 +0100 <monochrom> It is fairly trivial. It's literally the set of ASTs.
2025-01-18 00:11:52 +0100 <monochrom> So for example if you argue that programs are countable, you are just reminding us that the Herbrand model is countable.
2025-01-18 00:12:16 +0100 <monochrom> ... and I guess that's one way to see why there are countable models for ZFC!
2025-01-18 00:12:25 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-01-18 00:13:42 +0100 <haskellbridge> <thirdofmay18081814goya> i'll be back with a more rigorous statement
2025-01-18 00:13:57 +0100 <monochrom> And whatever you do in model theory, you must respect that Herbrand models are here to stay, even if it may be an annoying silly oddball.
2025-01-18 00:16:06 +0100agent314(~quassel@c-24-17-1-67.hsd1.wa.comcast.net) (Ping timeout: 252 seconds)
2025-01-18 00:16:30 +0100agent314(~quassel@37.19.210.25) agent314
2025-01-18 00:17:58 +0100 <monochrom> You may need more than spelling out a rigorous statement. You may end up also needing to spell out exactly which proof system you chose. Like I said, choosing a different one leads to the opposite result.
2025-01-18 00:18:48 +0100 <monochrom> And just around the same time in #haskell-offtopic we were talking about how programs come ship with their own C++ libs to avoid DLL hell.
2025-01-18 00:19:24 +0100 <monochrom> program : supporting libs :: true statement :: the proof system that proved it
2025-01-18 00:19:59 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 00:20:45 +0100tnt2(~Thunderbi@user/tnt1) tnt1
2025-01-18 00:21:20 +0100tnt1(~Thunderbi@user/tnt1) (Ping timeout: 272 seconds)
2025-01-18 00:21:20 +0100tnt2tnt1
2025-01-18 00:21:41 +0100 <monochrom> Oh and...
2025-01-18 00:21:50 +0100 <monochrom> @quote monochrom polymorphic
2025-01-18 00:21:50 +0100 <lambdabot> monochrom says: All pointless debates can be settled by going polymorphic.
2025-01-18 00:22:57 +0100 <c_wraith> does that also apply to pointfree debates?
2025-01-18 00:23:13 +0100 <monochrom> haha, I haven't thought of that.
2025-01-18 00:23:51 +0100igorantonow(~igor@user/igorantonow) igorantonow
2025-01-18 00:24:37 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2025-01-18 00:25:20 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 265 seconds)
2025-01-18 00:31:06 +0100igorantonow(~igor@user/igorantonow) (Remote host closed the connection)
2025-01-18 00:33:57 +0100__monty__(~toonn@user/toonn) (Quit: leaving)
2025-01-18 00:35:53 +0100ss4(~wootehfoo@user/wootehfoot) (Quit: Leaving)
2025-01-18 00:37:55 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 00:40:47 +0100Everything(~Everythin@195.138.86.118) (Quit: leaving)
2025-01-18 00:42:24 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
2025-01-18 00:42:44 +0100tallcatparade(~tallcatpa@99-171-182-203.lightspeed.sndgca.sbcglobal.net)
2025-01-18 00:43:44 +0100alecs(~alecs@61.pool85-58-154.dynamic.orange.es) alecs
2025-01-18 00:47:48 +0100alecs(~alecs@61.pool85-58-154.dynamic.orange.es) (Ping timeout: 244 seconds)
2025-01-18 00:53:18 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 00:57:47 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2025-01-18 00:57:47 +0100Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla
2025-01-18 00:58:09 +0100tallcatparade(~tallcatpa@99-171-182-203.lightspeed.sndgca.sbcglobal.net) (Ping timeout: 260 seconds)
2025-01-18 00:58:55 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-18 01:03:18 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 252 seconds)
2025-01-18 01:08:40 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 01:13:18 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2025-01-18 01:13:45 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-01-18 01:15:31 +0100tallcatparade(~tallcatpa@2600:8801:9801:d600::c83b)
2025-01-18 01:16:07 +0100machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds)
2025-01-18 01:18:30 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-18 01:24:02 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 01:24:21 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds)
2025-01-18 01:30:36 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
2025-01-18 01:33:57 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 01:38:29 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2025-01-18 01:42:38 +0100Sgeo(~Sgeo@user/sgeo) Sgeo
2025-01-18 01:48:49 +0100 <homo> trying to convert microhs's use of GHC.Types(Any) to Data.Dynamic(Dynamic) to make hugs happy is so hard that it seems impossible
2025-01-18 01:49:18 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 01:49:22 +0100TheCoffeMaker(~TheCoffeM@user/thecoffemaker) (Ping timeout: 248 seconds)
2025-01-18 01:51:49 +0100 <homo> the more I try the more I discover code that I have to rewrite
2025-01-18 01:53:42 +0100sprotte24(~sprotte24@p200300d16f42e000280df7176889acea.dip0.t-ipconnect.de) (Quit: Leaving)
2025-01-18 01:55:00 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2025-01-18 01:55:41 +0100Sgeo(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2025-01-18 02:03:57 +0100mixfix41(~tbmur@user/mixfix41) (Ping timeout: 265 seconds)
2025-01-18 02:05:46 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 02:10:43 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2025-01-18 02:13:09 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Remote host closed the connection)
2025-01-18 02:13:26 +0100euleritian(~euleritia@77.23.250.232)
2025-01-18 02:15:23 +0100acidjnk(~acidjnk@p200300d6e7283f5200259c07642d77ab.dip0.t-ipconnect.de) (Ping timeout: 245 seconds)
2025-01-18 02:16:37 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 248 seconds)
2025-01-18 02:19:34 +0100sawilagar(~sawilagar@user/sawilagar) (Ping timeout: 252 seconds)
2025-01-18 02:21:08 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 02:25:27 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2025-01-18 02:25:35 +0100Sgeo(~Sgeo@user/sgeo) Sgeo
2025-01-18 02:31:57 +0100otto_s(~user@p5b044128.dip0.t-ipconnect.de) (Ping timeout: 276 seconds)
2025-01-18 02:32:13 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 02:32:39 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 02:32:58 +0100otto_s(~user@p4ff27ba5.dip0.t-ipconnect.de)
2025-01-18 02:35:14 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-18 02:35:47 +0100Smiles(uid551636@id-551636.lymington.irccloud.com) Smiles
2025-01-18 02:36:30 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 02:39:29 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 248 seconds)
2025-01-18 02:39:45 +0100Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
2025-01-18 02:41:05 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2025-01-18 02:42:54 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 02:43:27 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 02:44:19 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 02:44:39 +0100euleritian(~euleritia@77.23.250.232) (Remote host closed the connection)
2025-01-18 02:44:51 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 02:45:31 +0100euleritian(~euleritia@77.23.250.232)
2025-01-18 02:49:04 +0100telser(~quassel@user/telser) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.)
2025-01-18 02:51:09 +0100ColinRobinson(~juan@user/JuanDaugherty) JuanDaugherty
2025-01-18 02:51:30 +0100weary-traveler(~user@user/user363627) (Remote host closed the connection)
2025-01-18 02:51:53 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 02:53:55 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-01-18 02:56:13 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2025-01-18 03:05:55 +0100ColinRobinsonJuanDaugherty
2025-01-18 03:07:14 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 03:11:38 +0100vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 252 seconds)
2025-01-18 03:13:31 +0100vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2025-01-18 03:14:12 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2025-01-18 03:15:18 +0100tnt1(~Thunderbi@user/tnt1) (Ping timeout: 252 seconds)
2025-01-18 03:15:18 +0100JuanDaughertyColinRobinson
2025-01-18 03:15:52 +0100tnt1(~Thunderbi@user/tnt1) tnt1
2025-01-18 03:17:14 +0100symdrome(~user@2804:1e78:2201:58b0::416) (ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.4))
2025-01-18 03:17:41 +0100jrm2(~jrm@user/jrm) jrm
2025-01-18 03:17:48 +0100jrm(~jrm@user/jrm) (Read error: Connection reset by peer)
2025-01-18 03:19:17 +0100jrm2jrm
2025-01-18 03:20:12 +0100Jeanne-Kamikaze(~Jeanne-Ka@79.127.217.40) Jeanne-Kamikaze
2025-01-18 03:24:20 +0100tnt2(~Thunderbi@user/tnt1) tnt1
2025-01-18 03:25:18 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 03:25:38 +0100tnt1(~Thunderbi@user/tnt1) (Ping timeout: 265 seconds)
2025-01-18 03:25:38 +0100tnt2tnt1
2025-01-18 03:27:07 +0100ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 264 seconds)
2025-01-18 03:27:56 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 03:28:24 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 03:29:31 +0100ColinRobinsonJuanDaugherty
2025-01-18 03:29:31 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2025-01-18 03:31:11 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-18 03:32:28 +0100tnt2(~Thunderbi@user/tnt1) tnt1
2025-01-18 03:32:53 +0100tnt1(~Thunderbi@user/tnt1) (Ping timeout: 265 seconds)
2025-01-18 03:32:53 +0100tnt2tnt1
2025-01-18 03:35:43 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 244 seconds)
2025-01-18 03:40:40 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 03:43:39 +0100JuanDaughertyColinRobinson
2025-01-18 03:45:01 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2025-01-18 03:50:44 +0100ColinRobinsonJuanDaugherty
2025-01-18 03:53:19 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-01-18 03:53:31 +0100alp(~alp@2001:861:8ca0:4940:efc9:d30b:fc5e:f0f7) (Ping timeout: 264 seconds)
2025-01-18 03:56:03 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 03:57:37 +0100tnt2(~Thunderbi@user/tnt1) tnt1
2025-01-18 03:57:56 +0100tnt1(~Thunderbi@user/tnt1) (Ping timeout: 244 seconds)
2025-01-18 03:57:56 +0100tnt2tnt1
2025-01-18 04:00:23 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds)
2025-01-18 04:01:10 +0100TheCoffeMaker(~TheCoffeM@user/thecoffemaker) TheCoffeMaker
2025-01-18 04:02:13 +0100tnt2(~Thunderbi@user/tnt1) tnt1
2025-01-18 04:02:29 +0100tnt1(~Thunderbi@user/tnt1) (Ping timeout: 260 seconds)
2025-01-18 04:02:29 +0100tnt2tnt1
2025-01-18 04:02:35 +0100JuanDaughertyColinRobinson
2025-01-18 04:10:50 +0100tnt2(~Thunderbi@user/tnt1) tnt1
2025-01-18 04:10:51 +0100tnt1(~Thunderbi@user/tnt1) (Ping timeout: 244 seconds)
2025-01-18 04:10:51 +0100tnt2tnt1
2025-01-18 04:11:25 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 04:11:59 +0100ColinRobinson(~juan@user/JuanDaugherty) (Quit: ColinRobinson)
2025-01-18 04:13:57 +0100pabs3(~pabs3@user/pabs3) (Ping timeout: 248 seconds)
2025-01-18 04:15:48 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2025-01-18 04:26:48 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 04:31:51 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2025-01-18 04:33:13 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-18 04:37:54 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 252 seconds)
2025-01-18 04:40:40 +0100Sgeo(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2025-01-18 04:42:25 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 04:44:54 +0100Smiles(uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity)
2025-01-18 04:46:48 +0100weary-traveler(~user@user/user363627) user363627
2025-01-18 04:47:42 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2025-01-18 04:55:11 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 04:55:40 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 04:56:14 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 04:56:40 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 04:56:46 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 04:57:52 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 04:57:55 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 04:58:29 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 04:59:18 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 04:59:26 +0100haskellbridge(~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection)
2025-01-18 05:00:09 +0100haskellbridge(~hackager@syn-024-093-192-219.res.spectrum.com) hackager
2025-01-18 05:00:09 +0100ChanServ+v haskellbridge
2025-01-18 05:00:12 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds)
2025-01-18 05:02:57 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2025-01-18 05:10:03 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
2025-01-18 05:10:40 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-01-18 05:13:39 +0100Sgeo(~Sgeo@user/sgeo) Sgeo
2025-01-18 05:13:51 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 05:18:19 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
2025-01-18 05:24:31 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 05:29:03 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2025-01-18 05:32:06 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-18 05:36:21 +0100Jeanne-Kamikaze(~Jeanne-Ka@79.127.217.40) (Quit: Leaving)
2025-01-18 05:36:37 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 244 seconds)
2025-01-18 05:45:14 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 05:50:03 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2025-01-18 05:50:25 +0100agent314(~quassel@37.19.210.25) (Ping timeout: 248 seconds)
2025-01-18 05:50:59 +0100xff0x(~xff0x@2405:6580:b080:900:d98:5c1a:a689:d0b8) (Ping timeout: 260 seconds)
2025-01-18 05:51:03 +0100szkl(uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity)
2025-01-18 05:54:27 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-01-18 05:59:13 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 06:00:35 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 06:05:58 +0100euleritian(~euleritia@77.23.250.232) (Remote host closed the connection)
2025-01-18 06:06:14 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
2025-01-18 06:07:34 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Remote host closed the connection)
2025-01-18 06:08:23 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
2025-01-18 06:12:23 +0100xff0x(~xff0x@2405:6580:b080:900:d98:5c1a:a689:d0b8)
2025-01-18 06:16:53 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 06:18:23 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 06:19:44 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 06:21:21 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2025-01-18 06:32:15 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 06:32:26 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-18 06:36:58 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 252 seconds)
2025-01-18 06:37:20 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2025-01-18 06:47:16 +0100sroso(~sroso@user/SrOso) SrOso
2025-01-18 06:48:11 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 06:55:24 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2025-01-18 07:07:34 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 07:12:09 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2025-01-18 07:15:59 +0100pabs3(~pabs3@user/pabs3) pabs3
2025-01-18 07:21:25 +0100greenflower(~greenflow@2409:4080:ceba:f2ae:f192:933c:3880:ac13) greenflower
2025-01-18 07:22:56 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 07:23:35 +0100greenflower(~greenflow@2409:4080:ceba:f2ae:f192:933c:3880:ac13) (Client Quit)
2025-01-18 07:23:55 +0100tessier(~tessier@ec2-184-72-149-67.compute-1.amazonaws.com) (Ping timeout: 265 seconds)
2025-01-18 07:24:15 +0100takuan(~takuan@178-116-218-225.access.telenet.be)
2025-01-18 07:25:24 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds)
2025-01-18 07:26:20 +0100pabs3(~pabs3@user/pabs3) (Remote host closed the connection)
2025-01-18 07:26:49 +0100vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 265 seconds)
2025-01-18 07:27:03 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-01-18 07:28:25 +0100vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2025-01-18 07:29:46 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2025-01-18 07:40:40 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 07:45:40 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2025-01-18 07:49:28 +0100tnt2(~Thunderbi@user/tnt1) tnt1
2025-01-18 07:50:30 +0100tnt1(~Thunderbi@user/tnt1) (Ping timeout: 265 seconds)
2025-01-18 07:50:30 +0100tnt2tnt1
2025-01-18 07:52:01 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-18 07:56:02 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 07:56:17 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 248 seconds)
2025-01-18 07:56:59 +0100pabs3(~pabs3@user/pabs3) pabs3
2025-01-18 07:59:36 +0100CiaoSen(~Jura@2a05:5800:220:2500:ca4b:d6ff:fec1:99da) CiaoSen
2025-01-18 08:00:15 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2025-01-18 08:00:27 +0100JamesMowery439(~JamesMowe@ip68-228-212-232.ph.ph.cox.net) (Quit: Goodbye)
2025-01-18 08:00:45 +0100JamesMowery4395(~JamesMowe@ip68-228-212-232.ph.ph.cox.net) JamesMowery
2025-01-18 08:02:57 +0100mikess(~mikess@user/mikess) mikess
2025-01-18 08:06:53 +0100mikess(~mikess@user/mikess) (Client Quit)
2025-01-18 08:11:25 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 08:13:28 +0100Square(~Square@user/square) Square
2025-01-18 08:16:07 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2025-01-18 08:23:05 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 08:24:22 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 08:24:29 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 08:25:55 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 08:26:32 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 08:31:32 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 08:32:49 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 08:33:18 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2025-01-18 08:33:36 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 08:34:53 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 08:35:24 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
2025-01-18 08:35:56 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 08:37:11 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 08:40:02 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 08:41:21 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 08:42:35 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 08:43:52 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 08:43:53 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 08:44:35 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 08:45:12 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 08:45:20 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 08:46:45 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 08:47:15 +0100harveypwca(~harveypwc@2601:246:d080:b40:1889:d9bf:2dd8:b288) HarveyPwca
2025-01-18 08:49:09 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2025-01-18 08:59:32 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2025-01-18 08:59:57 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 09:00:02 +0100caconym(~caconym@user/caconym) (Quit: bye)
2025-01-18 09:00:34 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-18 09:00:47 +0100caconym(~caconym@user/caconym) caconym
2025-01-18 09:01:58 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 09:03:16 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 09:03:25 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 09:04:50 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 244 seconds)
2025-01-18 09:04:55 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2025-01-18 09:05:57 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 09:06:43 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 09:11:56 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 09:12:02 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 09:12:45 +0100tnt2(~Thunderbi@user/tnt1) tnt1
2025-01-18 09:13:19 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 09:14:16 +0100tnt1(~Thunderbi@user/tnt1) (Ping timeout: 252 seconds)
2025-01-18 09:14:16 +0100tnt2tnt1
2025-01-18 09:14:21 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 09:15:18 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 09:15:37 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 09:20:18 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
2025-01-18 09:23:58 +0100harveypwca(~harveypwc@2601:246:d080:b40:1889:d9bf:2dd8:b288) (Quit: Leaving)
2025-01-18 09:26:03 +0100 <chiselfuse> [ x | x /=13, x <- [10..20], x /= 15, x /= 19]
2025-01-18 09:26:12 +0100 <chiselfuse> what happens here? why does it run forever?
2025-01-18 09:26:28 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 09:27:28 +0100 <tomsmeding> > [ x | x /=13, x <- [10..20], x /= 15, x /= 19]
2025-01-18 09:27:29 +0100 <lambdabot> [10,11,12,13,14,16,17,18,20]
2025-01-18 09:27:33 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 09:27:34 +0100 <tomsmeding> O.o
2025-01-18 09:27:36 +0100 <tomsmeding> % [ x | x /=13, x <- [10..20], x /= 15, x /= 19]
2025-01-18 09:27:36 +0100 <yahb2> <interactive>:5:7: error: [GHC-88464] Variable not in scope: x
2025-01-18 09:27:38 +0100 <tomsmeding> thank you
2025-01-18 09:27:44 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 09:27:44 +0100ljdarj(~Thunderbi@user/ljdarj) ljdarj
2025-01-18 09:27:53 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 09:27:57 +0100 <tomsmeding> chiselfuse: you can't require that x /= 13 before you have some x in the first place
2025-01-18 09:28:11 +0100 <tomsmeding> do you know python?
2025-01-18 09:28:43 +0100 <tomsmeding> > x
2025-01-18 09:28:44 +0100 <lambdabot> x
2025-01-18 09:28:49 +0100 <tomsmeding> (lambdabot being too clever)
2025-01-18 09:29:34 +0100homo(~homo@user/homo) (Read error: Connection reset by peer)
2025-01-18 09:30:02 +0100 <chiselfuse> tomsmeding: i know a little bit of python
2025-01-18 09:30:05 +0100 <chiselfuse> > :version
2025-01-18 09:30:06 +0100 <lambdabot> <hint>:1:1: error: parse error on input ‘:’
2025-01-18 09:30:17 +0100 <Angelz> python?
2025-01-18 09:30:19 +0100 <tomsmeding> chiselfuse: do you know python's list comprehension syntax?
2025-01-18 09:30:20 +0100 <chiselfuse> what's '>' and what is '%' here?
2025-01-18 09:30:24 +0100 <Angelz> i dunno
2025-01-18 09:30:27 +0100 <chiselfuse> tomsmeding: no
2025-01-18 09:30:29 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 09:30:44 +0100 <tomsmeding> it's rather like haskell's, so that would've been a shortcut for explaining what haskell does here :)
2025-01-18 09:30:56 +0100vanishingideal(~vanishing@user/vanishingideal) (Remote host closed the connection)
2025-01-18 09:30:59 +0100 <chiselfuse> what's '>' and what is '%' here?
2025-01-18 09:31:09 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 09:31:11 +0100 <tomsmeding> lambdabot and yahb2 are bothghci-ish; lambdabot responds to '>', yahb2 to '%'
2025-01-18 09:31:23 +0100 <tomsmeding> yahb2 is ghci, lambdabot is some magic over ghci
2025-01-18 09:31:27 +0100 <chiselfuse> how can we learn the ghci versions of othem?
2025-01-18 09:31:33 +0100 <tomsmeding> % :version
2025-01-18 09:31:33 +0100 <yahb2> 9.12.1
2025-01-18 09:31:38 +0100 <chiselfuse> > :version
2025-01-18 09:31:39 +0100 <lambdabot> <hint>:1:1: error: parse error on input ‘:’
2025-01-18 09:31:40 +0100 <tomsmeding> lambdabot doesn't support such querying
2025-01-18 09:32:01 +0100 <chiselfuse> mine is The Glorious Glasgow Haskell Compilation System, version 9.2.8
2025-01-18 09:32:03 +0100Angelz(Angelz@Angelz.oddprotocol.org) (Changing host)
2025-01-18 09:32:03 +0100Angelz(Angelz@user/angelz) angelz
2025-01-18 09:32:05 +0100 <chiselfuse> and it runs forever
2025-01-18 09:32:13 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2025-01-18 09:32:15 +0100 <tomsmeding> what is 'x'?
2025-01-18 09:32:25 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 09:32:29 +0100 <Angelz> cservice maybe.
2025-01-18 09:32:41 +0100 <tomsmeding> chiselfuse: because this particular bit of code should _not_ run forever.
2025-01-18 09:32:50 +0100 <chiselfuse> tomsmeding: but it evaluates fine on one of them. i want to know whether it's valid haskell or not (both semantically and syntactically) and how it gets evaluted on either of those
2025-01-18 09:33:01 +0100 <tomsmeding> it is not valid haskell
2025-01-18 09:33:06 +0100 <tomsmeding> because in the "x /= 13", x is out of scope
2025-01-18 09:33:17 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 09:33:17 +0100 <tomsmeding> lambdabot has pre-defined magic values for 'a' through 'z' for reasons
2025-01-18 09:33:24 +0100 <tomsmeding> so it doesn't quite raise an error here
2025-01-18 09:33:30 +0100 <chiselfuse> but it's just a definition, i thought those didn't matter in fp
2025-01-18 09:33:50 +0100acidjnk(~acidjnk@p200300d6e7283f4400259c07642d77ab.dip0.t-ipconnect.de) acidjnk
2025-01-18 09:33:53 +0100 <tomsmeding> in a list comprehension, the items to the right of the '|' get run "left-to-right"
2025-01-18 09:34:04 +0100 <chiselfuse> sorry, i meant i thought order of definitions didn't matter
2025-01-18 09:34:14 +0100 <chiselfuse> get run?
2025-01-18 09:34:18 +0100 <chiselfuse> procedurally?
2025-01-18 09:34:23 +0100 <chiselfuse> not so fp
2025-01-18 09:34:24 +0100 <tomsmeding> % [(x,y) | x <- [1..3], y <- ['a'..'c']]
2025-01-18 09:34:24 +0100 <yahb2> [(1,'a'),(1,'b'),(1,'c'),(2,'a'),(2,'b'),(2,'c'),(3,'a'),(3,'b'),(3,'c')]
2025-01-18 09:34:32 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 09:34:35 +0100it_(~quassel@v2202212189510211193.supersrv.de) (Quit: ,o>)
2025-01-18 09:34:38 +0100 <tomsmeding> % [(x,y) | x <- [1..3], x /= 2, y <- ['a'..'c']]
2025-01-18 09:34:38 +0100 <yahb2> [(1,'a'),(1,'b'),(1,'c'),(3,'a'),(3,'b'),(3,'c')]
2025-01-18 09:34:45 +0100 <tomsmeding> % [(x,y) | x <- [1..3], y <- ['a'..'c'], x /= 2]
2025-01-18 09:34:45 +0100 <yahb2> [(1,'a'),(1,'b'),(1,'c'),(3,'a'),(3,'b'),(3,'c')]
2025-01-18 09:34:51 +0100 <tomsmeding> % [(x,y) | x /= 2, x <- [1..3], y <- ['a'..'c']]
2025-01-18 09:34:51 +0100 <yahb2> <interactive>:15:10: error: [GHC-88464] Variable not in scope: x
2025-01-18 09:35:35 +0100 <tomsmeding> not quite procedurally, but you can think of it that way
2025-01-18 09:35:43 +0100 <tomsmeding> a '<-' clause is a "for loop", a bare condition is an "if"
2025-01-18 09:36:09 +0100 <tomsmeding> and at the bottom of the for/if nesting, the expression to the left of the '|' is generated
2025-01-18 09:36:14 +0100 <tomsmeding> the results are put in a list
2025-01-18 09:36:15 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 09:36:45 +0100 <Leary> @undo [ x | x /= 13, x <- [10..20], x /= 15 ]
2025-01-18 09:36:45 +0100 <lambdabot> if x /= 13 then concatMap (\ x -> if x /= 15 then [x] else []) [10 .. 20] else []
2025-01-18 09:37:10 +0100 <chiselfuse> what's @undo?
2025-01-18 09:37:27 +0100 <tomsmeding> converts a haskell expression into one using more basic syntax
2025-01-18 09:37:27 +0100 <Leary> It desugars the list comprehension so you can see what it means.
2025-01-18 09:37:30 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 09:37:41 +0100 <Leary> Here, you can see that `x` is used before it's brought into scope.
2025-01-18 09:38:10 +0100sawilagar(~sawilagar@user/sawilagar) sawilagar
2025-01-18 09:38:40 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 09:38:47 +0100 <chiselfuse> @undo [ x | x <- [10..20], x /=13, x /= 15 ]
2025-01-18 09:38:48 +0100 <lambdabot> concatMap (\ x -> if x /= 13 then if x /= 15 then [x] else [] else []) [10 .. 20]
2025-01-18 09:38:55 +0100 <chiselfuse> can i use @undo on my computer
2025-01-18 09:39:00 +0100it_(~quassel@game-crew.ch) K4su
2025-01-18 09:39:07 +0100 <tomsmeding> you can open a private chat with lambdabot
2025-01-18 09:39:22 +0100 <chiselfuse> @undo :version
2025-01-18 09:39:22 +0100 <lambdabot> <unknown>.hs:1:1:Parse error: :
2025-01-18 09:39:43 +0100 <chiselfuse> i want run code localloy
2025-01-18 09:39:56 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 09:40:13 +0100 <tomsmeding> '@undo' is a plugin in lambdabot, so it's rather hard to run locally
2025-01-18 09:40:34 +0100it_(~quassel@game-crew.ch) (Client Quit)
2025-01-18 09:40:49 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 09:40:51 +0100it_(~quassel@game-crew.ch) K4su
2025-01-18 09:42:08 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 09:42:55 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 09:43:08 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 09:44:20 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-01-18 09:44:31 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 09:44:51 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 09:46:08 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 09:48:51 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 09:50:17 +0100Guest9464(~v@anomalous.eu)
2025-01-18 09:51:01 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2025-01-18 09:51:05 +0100Guest9464(~v@anomalous.eu) (Remote host closed the connection)
2025-01-18 09:52:31 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 09:52:31 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 09:52:36 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2025-01-18 09:53:03 +0100 <haskellbridge> <Bowuigi> I guess you can just write the list comprehension in ghci and see if it works, along with the result
2025-01-18 09:53:35 +0100 <haskellbridge> <Bowuigi> You can't see what it desugars to, but you can build an intuition of what it does anyway
2025-01-18 09:53:53 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 09:54:21 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 09:55:45 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 09:55:57 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 09:57:14 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 09:57:24 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 09:58:50 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 09:59:02 +0100robobub(uid248673@id-248673.uxbridge.irccloud.com) robobub
2025-01-18 09:59:21 +0100it_(~quassel@game-crew.ch) (Quit: ,o>)
2025-01-18 09:59:29 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 09:59:54 +0100it_(~quassel@game-crew.ch) K4su
2025-01-18 10:00:59 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 10:01:03 +0100it_(~quassel@game-crew.ch) (Client Quit)
2025-01-18 10:01:35 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 10:02:05 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 10:03:02 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 10:03:43 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 10:03:45 +0100CiaoSen(~Jura@2a05:5800:220:2500:ca4b:d6ff:fec1:99da) (Ping timeout: 248 seconds)
2025-01-18 10:04:13 +0100it_(~quassel@game-crew.ch) K4su
2025-01-18 10:04:57 +0100alp(~alp@2001:861:8ca0:4940:a068:990b:3be7:3971)
2025-01-18 10:04:58 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 10:05:06 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 10:06:23 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 10:06:37 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 10:07:53 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 10:08:32 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 10:09:24 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
2025-01-18 10:09:34 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-18 10:09:48 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 10:10:35 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 10:11:51 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 10:12:43 +0100 <chiselfuse> are you sure that @undo is guaranteed to be correct in all cases?
2025-01-18 10:13:07 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 10:14:02 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 252 seconds)
2025-01-18 10:14:48 +0100 <tomsmeding> the author of lambdabot tried their best
2025-01-18 10:15:46 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 10:15:49 +0100 <tomsmeding> but in general that's what you're going to get from software -- even if you have formally proven software, that delegates the burden to the implementor of the proof tool, which is hopefully smaller and easier to check, but still to be checked manually
2025-01-18 10:15:54 +0100 <c_wraith> the desugaring is part of the spec. The only thing lambdabot doesn't necessarily have is the definition of all the relevant data types
2025-01-18 10:16:09 +0100 <c_wraith> So it doesn't know when a pattern match needs to introduce a fail case
2025-01-18 10:17:04 +0100 <c_wraith> (a pattern match on the LHS of a <-, specifically)
2025-01-18 10:17:56 +0100 <tomsmeding> @undo [x | Just x <- l]
2025-01-18 10:17:56 +0100 <lambdabot> concatMap (\ a -> case a of { Just x -> [x]; _ -> []}) l
2025-01-18 10:18:08 +0100 <tomsmeding> ah it just assumes there's other constructors
2025-01-18 10:20:08 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 10:20:19 +0100 <c_wraith> That's a case I'd expect to have hardcoded
2025-01-18 10:20:40 +0100 <c_wraith> @undo do { (a, b) <- foo ; pure $ a + b }
2025-01-18 10:20:40 +0100 <lambdabot> foo >>= \ (a, b) -> pure $ a + b
2025-01-18 10:20:56 +0100 <c_wraith> It knows that one only has one constructor
2025-01-18 10:21:10 +0100it_(~quassel@game-crew.ch) (Quit: ,o>)
2025-01-18 10:21:33 +0100 <c_wraith> I'd assume the @undo plugin has definitions for all the common types
2025-01-18 10:22:09 +0100it_(~quassel@game-crew.ch) K4su
2025-01-18 10:22:36 +0100 <c_wraith> @undo do { Foo a b <- foo ; pure $ a + b }
2025-01-18 10:22:36 +0100 <lambdabot> foo >>= \ c -> case c of { Foo a b -> pure $ a + b; _ -> fail ""}
2025-01-18 10:22:53 +0100 <c_wraith> and just assumes that things it doesn't know about have more constructors.
2025-01-18 10:23:12 +0100 <c_wraith> whereas ghc knows if there are more constructors or not
2025-01-18 10:24:40 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2025-01-18 10:28:38 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 10:29:33 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 10:30:56 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 10:30:57 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 10:32:14 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 10:32:16 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 10:32:18 +0100acidjnk(~acidjnk@p200300d6e7283f4400259c07642d77ab.dip0.t-ipconnect.de) (Ping timeout: 276 seconds)
2025-01-18 10:33:23 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2025-01-18 10:33:38 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 10:35:15 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 10:36:43 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 10:38:01 +0100euandreh1(~Thunderbi@191-217-172-66.user3p.v-tal.net.br) euandreh
2025-01-18 10:39:24 +0100tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
2025-01-18 10:39:28 +0100euandreh1(~Thunderbi@191-217-172-66.user3p.v-tal.net.br) (Client Quit)
2025-01-18 10:39:38 +0100ljdarj(~Thunderbi@user/ljdarj) (Quit: ljdarj)
2025-01-18 10:39:57 +0100ljdarj(~Thunderbi@user/ljdarj) ljdarj
2025-01-18 10:40:21 +0100ljdarj(~Thunderbi@user/ljdarj) (Client Quit)
2025-01-18 10:40:43 +0100ljdarj(~Thunderbi@user/ljdarj) ljdarj
2025-01-18 10:40:54 +0100euandreh(~Thunderbi@189.6.105.228) (Ping timeout: 260 seconds)
2025-01-18 10:42:30 +0100euandreh(~Thunderbi@191-217-172-66.user3p.v-tal.net.br) euandreh
2025-01-18 10:44:54 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 10:46:09 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 10:46:10 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 10:46:35 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 10:47:26 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 10:47:27 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 10:48:43 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 10:49:41 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 10:51:17 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2025-01-18 10:52:17 +0100Guest8686(~v@anomalous.eu)
2025-01-18 10:52:49 +0100ubert(~Thunderbi@p200300ecdf3b1a6b3fb62acbaa32cd66.dip0.t-ipconnect.de) ubert
2025-01-18 10:52:56 +0100todi(~todi@p57803331.dip0.t-ipconnect.de) todi
2025-01-18 10:57:46 +0100Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla
2025-01-18 10:59:13 +0100it_(~quassel@game-crew.ch) (Read error: Connection reset by peer)
2025-01-18 11:00:00 +0100Guest8686(~v@anomalous.eu) (Remote host closed the connection)
2025-01-18 11:01:21 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 11:01:28 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 11:01:58 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 11:02:41 +0100Guest3889(~v@anomalous.eu)
2025-01-18 11:03:15 +0100Guest3889(~v@anomalous.eu) (Remote host closed the connection)
2025-01-18 11:04:03 +0100ubert1(~Thunderbi@p200300ecdf3b1a6b88ad1acf189eaf58.dip0.t-ipconnect.de) ubert
2025-01-18 11:05:59 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 11:06:03 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 11:06:15 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2025-01-18 11:07:23 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 11:07:25 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 11:07:53 +0100ubert(~Thunderbi@p200300ecdf3b1a6b3fb62acbaa32cd66.dip0.t-ipconnect.de) (Ping timeout: 245 seconds)
2025-01-18 11:08:17 +0100ubert1(~Thunderbi@p200300ecdf3b1a6b88ad1acf189eaf58.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
2025-01-18 11:08:43 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 11:09:53 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 11:11:10 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 11:11:56 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 11:13:12 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 11:13:19 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 11:14:35 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 11:14:41 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 11:14:44 +0100 <chiselfuse> c_wraith: can you link me the spec for desugaring please?
2025-01-18 11:15:49 +0100 <Leary> chiselfuse: https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-420003.11
2025-01-18 11:16:13 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 11:16:34 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 11:17:22 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 11:17:51 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 11:17:58 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 11:19:29 +0100target_i(~target_i@user/target-i/x-6023099) target_i
2025-01-18 11:22:19 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
2025-01-18 11:27:30 +0100ubert(~Thunderbi@p200300ecdf3b1a6ba5e76ac014a2fe38.dip0.t-ipconnect.de) ubert
2025-01-18 11:29:30 +0100euandreh(~Thunderbi@191-217-172-66.user3p.v-tal.net.br) (Ping timeout: 276 seconds)
2025-01-18 11:29:32 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 11:30:12 +0100euandreh(~Thunderbi@189.6.105.228) euandreh
2025-01-18 11:32:36 +0100euandreh(~Thunderbi@189.6.105.228) (Client Quit)
2025-01-18 11:34:00 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
2025-01-18 11:36:30 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-18 11:37:46 +0100ByronJohnson(~bairyn@50.250.232.19) (Ping timeout: 244 seconds)
2025-01-18 11:38:01 +0100ByronJohnson(~bairyn@MAIL.DIGITALKINGDOM.ORG) ByronJohnson
2025-01-18 11:40:59 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 260 seconds)
2025-01-18 11:44:19 +0100rvalue(~rvalue@user/rvalue) (Read error: Connection reset by peer)
2025-01-18 11:44:51 +0100rvalue(~rvalue@user/rvalue) rvalue
2025-01-18 11:44:55 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 11:49:25 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2025-01-18 11:50:18 +0100ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 276 seconds)
2025-01-18 12:00:17 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 12:07:01 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2025-01-18 12:07:03 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds)
2025-01-18 12:07:19 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
2025-01-18 12:09:44 +0100remedan(~remedan@ip-62-245-108-153.bb.vodafone.cz) (Quit: Bye!)
2025-01-18 12:14:23 +0100pavonia(~user@user/siracusa) (Quit: Bye!)
2025-01-18 12:14:57 +0100Sgeo(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2025-01-18 12:18:04 +0100remedan(~remedan@ip-62-245-108-153.bb.vodafone.cz) remedan
2025-01-18 12:18:20 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 12:18:51 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-18 12:23:01 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2025-01-18 12:23:29 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 248 seconds)
2025-01-18 12:25:13 +0100__monty__(~toonn@user/toonn) toonn
2025-01-18 12:25:49 +0100acidjnk(~acidjnk@p200300d6e7283f4440b553cdf075f952.dip0.t-ipconnect.de) acidjnk
2025-01-18 12:26:56 +0100remedan(~remedan@ip-62-245-108-153.bb.vodafone.cz) (Quit: Bye!)
2025-01-18 12:28:03 +0100CiaoSen(~Jura@2a05:5800:220:2500:ca4b:d6ff:fec1:99da) CiaoSen
2025-01-18 12:29:10 +0100alecs(~alecs@61.pool85-58-154.dynamic.orange.es) alecs
2025-01-18 12:30:31 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 12:30:46 +0100remedan(~remedan@ip-62-245-108-153.bb.vodafone.cz) remedan
2025-01-18 12:32:31 +0100alp(~alp@2001:861:8ca0:4940:a068:990b:3be7:3971) (Ping timeout: 264 seconds)
2025-01-18 12:33:30 +0100alecs(~alecs@61.pool85-58-154.dynamic.orange.es) (Ping timeout: 246 seconds)
2025-01-18 12:34:54 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
2025-01-18 12:45:53 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 12:50:34 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
2025-01-18 12:50:59 +0100dtman34(~dtman34@c-174-53-203-90.hsd1.mn.comcast.net) (Ping timeout: 260 seconds)
2025-01-18 13:00:05 +0100caconym(~caconym@user/caconym) (Quit: bye)
2025-01-18 13:01:18 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 13:02:40 +0100caconym(~caconym@user/caconym) caconym
2025-01-18 13:04:44 +0100ljdarj(~Thunderbi@user/ljdarj) ljdarj
2025-01-18 13:04:57 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-18 13:06:21 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds)
2025-01-18 13:08:49 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-01-18 13:09:36 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 276 seconds)
2025-01-18 13:13:38 +0100sroso(~sroso@user/SrOso) (Quit: Leaving :))
2025-01-18 13:14:16 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2025-01-18 13:15:00 +0100Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
2025-01-18 13:16:39 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 13:20:48 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 245 seconds)
2025-01-18 13:21:09 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2025-01-18 13:21:34 +0100euleritian(~euleritia@dynamic-176-006-137-212.176.6.pool.telefonica.de)
2025-01-18 13:22:33 +0100ensyde(~ensyde@2601:5c6:c200:6dc0::3cb6) (Ping timeout: 265 seconds)
2025-01-18 13:22:43 +0100dtman34(~dtman34@c-174-53-203-90.hsd1.mn.comcast.net) dtman34
2025-01-18 13:27:24 +0100CiaoSen(~Jura@2a05:5800:220:2500:ca4b:d6ff:fec1:99da) (Ping timeout: 246 seconds)
2025-01-18 13:29:28 +0100lxsameer(~lxsameer@Serene/lxsameer) lxsameer
2025-01-18 13:31:32 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 13:33:51 +0100Digitteknohippie(~user@user/digit) Digit
2025-01-18 13:35:19 +0100Digit(~user@user/digit) (Ping timeout: 260 seconds)
2025-01-18 13:36:39 +0100Midjak(~MarciZ@82.66.147.146) (Quit: This computer has gone to sleep)
2025-01-18 13:38:15 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2025-01-18 13:40:58 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-18 13:45:13 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 252 seconds)
2025-01-18 13:49:35 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 13:50:06 +0100acidjnk(~acidjnk@p200300d6e7283f4440b553cdf075f952.dip0.t-ipconnect.de) (Ping timeout: 252 seconds)
2025-01-18 13:54:02 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2025-01-18 14:04:41 +0100euleritian(~euleritia@dynamic-176-006-137-212.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2025-01-18 14:04:56 +0100sprotte24(~sprotte24@p200300d16f495900c540e25e648a3a4c.dip0.t-ipconnect.de)
2025-01-18 14:04:57 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 14:05:22 +0100euleritian(~euleritia@dynamic-176-006-137-212.176.6.pool.telefonica.de)
2025-01-18 14:05:45 +0100euleritian(~euleritia@dynamic-176-006-137-212.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2025-01-18 14:06:02 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
2025-01-18 14:08:29 +0100alp(~alp@2001:861:8ca0:4940:88c9:4a0c:8072:846f)
2025-01-18 14:13:36 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
2025-01-18 14:14:50 +0100rvalue-(~rvalue@user/rvalue) rvalue
2025-01-18 14:15:33 +0100rvalue(~rvalue@user/rvalue) (Ping timeout: 248 seconds)
2025-01-18 14:17:08 +0100acidjnk(~acidjnk@p200300d6e7283f4440b553cdf075f952.dip0.t-ipconnect.de) acidjnk
2025-01-18 14:18:40 +0100ash3en(~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en
2025-01-18 14:18:43 +0100ash3en(~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Client Quit)
2025-01-18 14:21:24 +0100rvalue-rvalue
2025-01-18 14:23:29 +0100Digitteknohippie(~user@user/digit) (Ping timeout: 248 seconds)
2025-01-18 14:24:51 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 14:24:58 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 245 seconds)
2025-01-18 14:25:33 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
2025-01-18 14:26:12 +0100weary-traveler(~user@user/user363627) (Remote host closed the connection)
2025-01-18 14:26:30 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-01-18 14:28:44 +0100ubert(~Thunderbi@p200300ecdf3b1a6ba5e76ac014a2fe38.dip0.t-ipconnect.de) (Ping timeout: 272 seconds)
2025-01-18 14:29:14 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2025-01-18 14:30:20 +0100robobub(uid248673@id-248673.uxbridge.irccloud.com) (Quit: Connection closed for inactivity)
2025-01-18 14:31:06 +0100alecs(~alecs@61.pool85-58-154.dynamic.orange.es) alecs
2025-01-18 14:32:39 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 14:35:41 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-18 14:36:03 +0100alecs(~alecs@61.pool85-58-154.dynamic.orange.es) (Ping timeout: 276 seconds)
2025-01-18 14:36:56 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2025-01-18 14:40:36 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 276 seconds)
2025-01-18 14:45:52 +0100ubert(~Thunderbi@p200300ecdf3b1a6b33f8a008550b561a.dip0.t-ipconnect.de) ubert
2025-01-18 14:47:58 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 14:49:43 +0100CiaoSen(~Jura@2a05:5800:220:2500:ca4b:d6ff:fec1:99da) CiaoSen
2025-01-18 14:53:21 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2025-01-18 15:04:25 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 15:04:57 +0100nrs(~nrs@190.16.167.62)
2025-01-18 15:05:15 +0100nrs(~nrs@190.16.167.62) (Client Quit)
2025-01-18 15:06:11 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2025-01-18 15:08:31 +0100acidjnk(~acidjnk@p200300d6e7283f4440b553cdf075f952.dip0.t-ipconnect.de) (Ping timeout: 264 seconds)
2025-01-18 15:08:53 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2025-01-18 15:19:49 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 15:20:27 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-18 15:20:37 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 15:20:42 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 15:20:51 +0100CiaoSen(~Jura@2a05:5800:220:2500:ca4b:d6ff:fec1:99da) (Ping timeout: 252 seconds)
2025-01-18 15:25:18 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 265 seconds)
2025-01-18 15:26:46 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2025-01-18 15:30:31 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 15:30:34 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 15:31:12 +0100m5zs7k(aquares@web10.mydevil.net) (Ping timeout: 252 seconds)
2025-01-18 15:32:31 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 15:32:34 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 15:33:32 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 15:33:53 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 15:33:53 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 15:35:15 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 15:35:22 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 15:35:29 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds)
2025-01-18 15:35:39 +0100euleritian(~euleritia@dynamic-176-006-137-212.176.6.pool.telefonica.de)
2025-01-18 15:35:49 +0100m5zs7k(aquares@web10.mydevil.net) m5zs7k
2025-01-18 15:36:47 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 15:36:49 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 15:38:06 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 15:38:09 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 15:38:24 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
2025-01-18 15:42:41 +0100vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2025-01-18 15:45:53 +0100CiaoSen(~Jura@2a05:5800:220:2500:ca4b:d6ff:fec1:99da) CiaoSen
2025-01-18 15:48:55 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 15:49:55 +0100 <lxsameer> hey folks, is there a shorter syntatx for this pattern? https://dpaste.com/D2KZVHSBY
2025-01-18 15:51:21 +0100CiaoSen(~Jura@2a05:5800:220:2500:ca4b:d6ff:fec1:99da) (Ping timeout: 252 seconds)
2025-01-18 15:51:48 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-18 15:51:50 +0100V(~v@ircpuzzles/2022/april/winner/V) (Remote host closed the connection)
2025-01-18 15:52:36 +0100 <Leary> lxsameer: `foo <|> ....`
2025-01-18 15:52:45 +0100sprotte24(~sprotte24@p200300d16f495900c540e25e648a3a4c.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
2025-01-18 15:54:33 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2025-01-18 15:55:10 +0100 <lxsameer> Leary: cool, thank you
2025-01-18 15:55:21 +0100gmg(~user@user/gehmehgeh) (Remote host closed the connection)
2025-01-18 15:58:15 +0100gmg(~user@user/gehmehgeh) gehmehgeh
2025-01-18 16:03:39 +0100Digit(~user@user/digit) Digit
2025-01-18 16:03:53 +0100sprotte24(~sprotte24@p200300d16f495900c82cb8d65a41923f.dip0.t-ipconnect.de)
2025-01-18 16:05:43 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 16:06:46 +0100euleritian(~euleritia@dynamic-176-006-137-212.176.6.pool.telefonica.de) (Ping timeout: 252 seconds)
2025-01-18 16:06:54 +0100weary-traveler(~user@user/user363627) user363627
2025-01-18 16:08:06 +0100euleritian(~euleritia@dynamic-176-003-077-005.176.3.pool.telefonica.de)
2025-01-18 16:10:04 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2025-01-18 16:21:06 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 16:27:33 +0100CiaoSen(~Jura@2a05:5800:220:2500:ca4b:d6ff:fec1:99da) CiaoSen
2025-01-18 16:27:36 +0100euleritian(~euleritia@dynamic-176-003-077-005.176.3.pool.telefonica.de) (Read error: Connection reset by peer)
2025-01-18 16:28:07 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
2025-01-18 16:28:49 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2025-01-18 16:32:34 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 248 seconds)
2025-01-18 16:33:56 +0100euleritian(~euleritia@dynamic-176-003-077-005.176.3.pool.telefonica.de)
2025-01-18 16:34:33 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 16:38:59 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2025-01-18 16:42:34 +0100euleritian(~euleritia@dynamic-176-003-077-005.176.3.pool.telefonica.de) (Read error: Connection reset by peer)
2025-01-18 16:42:52 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
2025-01-18 16:49:55 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 16:53:17 +0100sprotte24(~sprotte24@p200300d16f495900c82cb8d65a41923f.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
2025-01-18 16:54:11 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-01-18 16:54:26 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2025-01-18 17:00:22 +0100vanishingideal(~vanishing@user/vanishingideal) (Remote host closed the connection)
2025-01-18 17:01:34 +0100Fijxu(~Fijxu@user/fijxu) (Quit: XD!!)
2025-01-18 17:06:16 +0100Fijxu(~Fijxu@user/fijxu) fijxu
2025-01-18 17:10:13 +0100sprotte24(~sprotte24@p200300d16f495900956dd031c8d9206e.dip0.t-ipconnect.de)
2025-01-18 17:10:31 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 17:10:36 +0100weary-traveler(~user@user/user363627) (Remote host closed the connection)
2025-01-18 17:16:01 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-01-18 17:17:27 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2025-01-18 17:21:52 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 244 seconds)
2025-01-18 17:22:28 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2025-01-18 17:25:49 +0100euleritian(~euleritia@dynamic-176-003-077-005.176.3.pool.telefonica.de)
2025-01-18 17:27:03 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
2025-01-18 17:28:34 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 17:32:42 +0100vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2025-01-18 17:33:07 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds)
2025-01-18 17:34:12 +0100alecs(~alecs@61.pool85-58-154.dynamic.orange.es) alecs
2025-01-18 17:34:30 +0100tallcatparade(~tallcatpa@2600:8801:9801:d600::c83b) (Ping timeout: 246 seconds)
2025-01-18 17:35:35 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 17:37:22 +0100euleritian(~euleritia@dynamic-176-003-077-005.176.3.pool.telefonica.de) (Ping timeout: 244 seconds)
2025-01-18 17:37:32 +0100euleritian(~euleritia@dynamic-176-003-039-171.176.3.pool.telefonica.de)
2025-01-18 17:38:24 +0100alecs(~alecs@61.pool85-58-154.dynamic.orange.es) (Ping timeout: 244 seconds)
2025-01-18 17:40:10 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
2025-01-18 17:47:09 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-18 17:51:25 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 17:51:57 +0100sprotte24(~sprotte24@p200300d16f495900956dd031c8d9206e.dip0.t-ipconnect.de) (Quit: Leaving)
2025-01-18 17:52:21 +0100euleritian(~euleritia@dynamic-176-003-039-171.176.3.pool.telefonica.de) (Read error: Connection reset by peer)
2025-01-18 17:53:04 +0100euleritian(~euleritia@dynamic-176-003-039-171.176.3.pool.telefonica.de)
2025-01-18 17:54:11 +0100ggggg(~ggggg@146-241-40-105.dyn.eolo.it)
2025-01-18 17:55:48 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds)
2025-01-18 17:57:36 +0100euleritian(~euleritia@dynamic-176-003-039-171.176.3.pool.telefonica.de) (Ping timeout: 252 seconds)
2025-01-18 17:59:55 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 18:00:35 +0100acidjnk(~acidjnk@p200300d6e7283f4440b553cdf075f952.dip0.t-ipconnect.de) acidjnk
2025-01-18 18:01:24 +0100ggggg(~ggggg@146-241-40-105.dyn.eolo.it) (Remote host closed the connection)
2025-01-18 18:02:18 +0100hueso(~root@user/hueso) (Read error: Connection reset by peer)
2025-01-18 18:03:25 +0100hueso(~root@user/hueso) hueso
2025-01-18 18:04:03 +0100hueso(~root@user/hueso) (Read error: Connection reset by peer)
2025-01-18 18:04:12 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
2025-01-18 18:06:37 +0100hueso(~root@user/hueso) hueso
2025-01-18 18:07:26 +0100hueso(~root@user/hueso) (Read error: Connection reset by peer)
2025-01-18 18:08:35 +0100hueso(~root@user/hueso) hueso
2025-01-18 18:09:05 +0100CiaoSen(~Jura@2a05:5800:220:2500:ca4b:d6ff:fec1:99da) (Ping timeout: 248 seconds)
2025-01-18 18:12:08 +0100hueso(~root@user/hueso) (Read error: Connection reset by peer)
2025-01-18 18:12:21 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 248 seconds)
2025-01-18 18:13:33 +0100hueso(~root@user/hueso) hueso
2025-01-18 18:13:42 +0100euleritian(~euleritia@dynamic-176-002-007-012.176.2.pool.telefonica.de)
2025-01-18 18:14:09 +0100euleritian(~euleritia@dynamic-176-002-007-012.176.2.pool.telefonica.de) (Read error: Connection reset by peer)
2025-01-18 18:14:27 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
2025-01-18 18:15:18 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 18:17:07 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-01-18 18:20:17 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
2025-01-18 18:21:14 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 265 seconds)
2025-01-18 18:29:55 +0100euleritian(~euleritia@dynamic-176-001-132-019.176.1.pool.telefonica.de)
2025-01-18 18:30:40 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 18:32:39 +0100vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 244 seconds)
2025-01-18 18:34:26 +0100vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2025-01-18 18:35:03 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
2025-01-18 18:36:45 +0100euleritian(~euleritia@dynamic-176-001-132-019.176.1.pool.telefonica.de) (Read error: Connection reset by peer)
2025-01-18 18:37:03 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
2025-01-18 18:38:44 +0100Midjak(~MarciZ@82.66.147.146) Midjak
2025-01-18 18:38:47 +0100 <lxsameer> https://dpaste.com/ARK8BLHC9 is it possible to limit the type T in the signature of the Foo function to only the B contructor?
2025-01-18 18:42:29 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2025-01-18 18:48:19 +0100 <geekosaur> no, constructors are not types (unless promoted, which doesn't do what you want)
2025-01-18 18:51:23 +0100 <EvanR> you can define T using GADTs which makes T's constructed from B identifiable at the type level
2025-01-18 18:51:34 +0100 <EvanR> then foo can use that in the type signature
2025-01-18 18:51:42 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 18:51:47 +0100 <EvanR> whether this is worth it I cannot say
2025-01-18 18:52:16 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-01-18 18:52:27 +0100 <EvanR> it also leads to an awkward definition of foo which will need to put something for the A case even though it would be impossible
2025-01-18 18:52:55 +0100 <EvanR> if you have an answer to "what are you really trying to do" someone might have a more elegant way to say it in haskell
2025-01-18 18:55:53 +0100 <lxsameer> EvanR: I'm trying to learn more about Gadts and dependent types in haskell
2025-01-18 18:59:01 +0100 <lxsameer> EvanR: I tried to do what I did in Agda in haskell but didn't work obviously
2025-01-18 18:59:10 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
2025-01-18 18:59:45 +0100 <geekosaur> haskell doesn't have dependent types. it has a horrible hack (`singletons`) which simulates them to some extent
2025-01-18 18:59:46 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2025-01-18 19:00:21 +0100 <lxsameer> geekosaur: ahhh got it.
2025-01-18 19:04:15 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-18 19:04:23 +0100tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net) tzh
2025-01-18 19:08:43 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 245 seconds)
2025-01-18 19:09:45 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 19:11:59 +0100Square(~Square@user/square) (Remote host closed the connection)
2025-01-18 19:13:54 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds)
2025-01-18 19:14:18 +0100euleritian(~euleritia@dynamic-176-001-132-019.176.1.pool.telefonica.de)
2025-01-18 19:14:54 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds)
2025-01-18 19:15:52 +0100Square(~Square@user/square) Square
2025-01-18 19:17:37 +0100wootehfoot(~wootehfoo@user/wootehfoot) wootehfoot
2025-01-18 19:17:42 +0100 <EvanR> you don't technically need singletons to do what I was saying, but it's more organized if you use dedicated singletons for that
2025-01-18 19:18:47 +0100 <EvanR> haskell not having dependent types means accomplishing a similar thing is usually klunkier. But there might be a more haskelly way to do it
2025-01-18 19:19:26 +0100Fijxu(~Fijxu@user/fijxu) (Quit: XD!!)
2025-01-18 19:23:21 +0100 <EvanR> for example the foo function could just take a Text instead of a T, and at the call site would need to unpack the T to get a Text, else no dice
2025-01-18 19:23:54 +0100 <EvanR> the a type variable can't be used for anything in this example since it will be unknown to the foo function and doesn't appear as part of the Foo return type
2025-01-18 19:24:25 +0100 <EvanR> so can be omitted entirely
2025-01-18 19:25:07 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 19:25:21 +0100 <monochrom> ISTR if you go the GADT way, foo won't need a case for A, and even -Wall will not generate a warning.
2025-01-18 19:25:28 +0100pavonia(~user@user/siracusa) siracusa
2025-01-18 19:25:48 +0100 <monochrom> I'm too lazy to test that, but it is easy to test.
2025-01-18 19:27:44 +0100 <EvanR> that's snazzy
2025-01-18 19:28:01 +0100rvalue(~rvalue@user/rvalue) (Read error: Connection reset by peer)
2025-01-18 19:28:32 +0100rvalue(~rvalue@user/rvalue) rvalue
2025-01-18 19:28:42 +0100 <lxsameer> monochrom: but is that type safe?
2025-01-18 19:28:58 +0100euleritian(~euleritia@dynamic-176-001-132-019.176.1.pool.telefonica.de) (Ping timeout: 244 seconds)
2025-01-18 19:28:59 +0100 <EvanR> the A case would be impossible at runtime
2025-01-18 19:29:30 +0100euleritian(~euleritia@dynamic-176-006-138-171.176.6.pool.telefonica.de)
2025-01-18 19:29:31 +0100 <EvanR> because the types could not have checked
2025-01-18 19:29:39 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
2025-01-18 19:30:30 +0100Fijxu(~Fijxu@user/fijxu) fijxu
2025-01-18 19:30:32 +0100Fijxu(~Fijxu@user/fijxu) (Remote host closed the connection)
2025-01-18 19:30:44 +0100 <EvanR> I am walking out the door so I can't type up the GADT version of the example
2025-01-18 19:30:58 +0100 <EvanR> the margin is too small for the proof!
2025-01-18 19:33:18 +0100Feuermagier_(~Feuermagi@user/feuermagier) Feuermagier
2025-01-18 19:33:18 +0100Feuermagier(~Feuermagi@user/feuermagier) (Killed (silver.libera.chat (Nickname regained by services)))
2025-01-18 19:33:18 +0100Feuermagier_Feuermagier
2025-01-18 19:33:30 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 19:38:08 +0100Feuermagier(~Feuermagi@user/feuermagier) (Client Quit)
2025-01-18 19:38:22 +0100ColinRobinson(~juan@user/JuanDaugherty) JuanDaugherty
2025-01-18 19:39:06 +0100szkl(uid110435@id-110435.uxbridge.irccloud.com) szkl
2025-01-18 19:41:37 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds)
2025-01-18 19:41:40 +0100Lord_of_Life_(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2025-01-18 19:42:14 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
2025-01-18 19:44:40 +0100Lord_of_Life_Lord_of_Life
2025-01-18 19:45:57 +0100cheater_(~Username@user/cheater) cheater
2025-01-18 19:46:01 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-01-18 19:48:35 +0100cheater(~Username@user/cheater) (Ping timeout: 252 seconds)
2025-01-18 19:48:44 +0100cheater_cheater
2025-01-18 19:52:28 +0100acidjnk(~acidjnk@p200300d6e7283f4440b553cdf075f952.dip0.t-ipconnect.de) (Ping timeout: 245 seconds)
2025-01-18 19:52:43 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn
2025-01-18 19:57:25 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
2025-01-18 20:02:31 +0100 <monochrom> You will have "data G a b where A :: a -> Int -> G a Int; B :: a -> Text -> G a Text". b is a phantom type param that is sync'ed with whether your ctor is A or B.
2025-01-18 20:03:33 +0100 <monochrom> Then we can argue all day long whether "foo :: G a Text -> Foo" needs a line for the A case or not, how many warnings must the compiler give, etc. etc. But that's beside the point.
2025-01-18 20:04:02 +0100 <monochrom> The point is with "foo :: G a Text -> Foo", the user will be banned from trying "foo (A ...)".
2025-01-18 20:04:13 +0100 <monochrom> In that sense, it is 100% type-safe.
2025-01-18 20:04:38 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-18 20:08:04 +0100merijn(~merijn@128-137-045-062.dynamic.caiway.nl) merijn