2025/12/03

2025-12-03 00:00:07 +0100__monty__(~toonn@user/toonn) (Quit: leaving)
2025-12-03 00:00:29 +0100lambda_gibbon(~lambda_gi@2603:7080:ee00:37d8:11e:138e:d914:c117) (Ping timeout: 260 seconds)
2025-12-03 00:03:23 +0100gorignak(~gorignak@user/gorignak) gorignak
2025-12-03 00:04:30 +0100vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 245 seconds)
2025-12-03 00:06:19 +0100vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2025-12-03 00:07:03 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 00:10:33 +0100trickard_trickard
2025-12-03 00:11:44 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-12-03 00:12:02 +0100target_i(~target_i@user/target-i/x-6023099) (Quit: leaving)
2025-12-03 00:19:44 +0100Miroboru(~myrvoll@84.215.250.50) Miroboru
2025-12-03 00:22:50 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 00:24:46 +0100trickard(~trickard@cpe-85-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
2025-12-03 00:24:59 +0100trickard_(~trickard@cpe-85-98-47-163.wireline.com.au)
2025-12-03 00:26:56 +0100tromp(~textual@2001:1c00:3487:1b00:40c9:191b:e4f:324a) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-12-03 00:27:51 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-12-03 00:38:38 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 00:41:14 +0100 <iqubic> Is there a list of Haskell code style things I should know about, like how many spaces to indent things and what have you?
2025-12-03 00:43:04 +0100humasect(~humasect@dyn-192-249-132-90.nexicom.net) humasect
2025-12-03 00:43:20 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
2025-12-03 00:43:44 +0100trickard_trickard
2025-12-03 00:43:57 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-12-03 00:44:30 +0100jmcantrell_(~weechat@user/jmcantrell) (Ping timeout: 245 seconds)
2025-12-03 00:47:58 +0100peterbecich(~Thunderbi@172.222.148.214) peterbecich
2025-12-03 00:48:13 +0100humasect(~humasect@dyn-192-249-132-90.nexicom.net) (Ping timeout: 255 seconds)
2025-12-03 00:50:22 +0100 <geekosaur> in terms of style, the closest thing to a standard is what various code formatters do — but ormolu, fourmolu, stylish-haskell, brittany (now defunct, I think), etc. all have different opinions
2025-12-03 00:52:27 +0100 <iqubic> Is there anywhere I can go to see what they all do? Is there a comparison anywhere?
2025-12-03 00:54:22 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 00:58:57 +0100 <EvanR> I looked at ormolu's output and it didn't match my expectations of style
2025-12-03 00:59:01 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2025-12-03 00:59:14 +0100 <iqubic> EvanR: What do you use?
2025-12-03 00:59:31 +0100 <EvanR> nothing
2025-12-03 00:59:55 +0100 <iqubic> I see.
2025-12-03 01:00:26 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection)
2025-12-03 01:00:48 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-12-03 01:01:24 +0100Anarchos(~Anarchos@91-161-254-16.subs.proxad.net) ()
2025-12-03 01:05:44 +0100Googulator11(~Googulato@2a01-036d-0106-479c-d9ec-010d-f188-ffcb.pool6.digikabel.hu)
2025-12-03 01:05:46 +0100Googulator95(~Googulato@85-238-68-117.pool.digikabel.hu) (Quit: Client closed)
2025-12-03 01:06:22 +0100Tuplanolla(~Tuplanoll@91-152-225-194.elisa-laajakaista.fi) Tuplanolla
2025-12-03 01:06:22 +0100 <geekosaur> likewise fwiw. I think I'd prefer stylish-haskell if someone held a gun to my head and forced me to use a formatter
2025-12-03 01:09:30 +0100 <jackdk> ormolu's choices are mostly well-argued but somehow it manages to emit the least aesthetic code I've seen. this is not just an ormulu problem, btw - it seems that each new nix language formatter discovers new frontiers in uglifying code =(. Regardless, I still use autoformatters in a lot of projects just to avoid having style discussions. If I had the time and inclination, I'd look at twiddling the knobs on fourmolu to do more of what i wanted.
2025-12-03 01:10:10 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 01:11:11 +0100 <ski> iqubic : <https://github.com/tibbe/haskell-style-guide/blob/master/haskell-style.md> is one resource, that might be useful to check and ponder
2025-12-03 01:11:18 +0100 <ski> (re tabs vs. spaces, "Yet Another Tabs v. Spaces Debate - I mix tabs and spaces" by dmwit at <http://dmwit.com/tabs/> (also <https://3.bp.blogspot.com/-kX7Gs0lFG_0/V9GIDlF59cI/AAAAAAAAG9E/8OXtloszZRMwd0_NjkWGk6qYedy_0m6jgCL…>) is another opinion)
2025-12-03 01:11:20 +0100 <EvanR> autoformatter fans I've talked to would say if there are configuration options it's defeating the purpose (to have everyone use the same format)
2025-12-03 01:11:57 +0100 <int-e> but if you don't have options then you're defeating adaptation :-P
2025-12-03 01:11:59 +0100 <ski> i would not trust an autoformatter, without closely checking out its opinions
2025-12-03 01:12:15 +0100 <int-e> I meant adoptation, though both work
2025-12-03 01:12:19 +0100 <jackdk> EvanR: I disagree, because you can still maintain consistency within a codebase, which is where I feel it's most important.
2025-12-03 01:12:27 +0100 <jackdk> (with autoformatter fans, not with you)
2025-12-03 01:12:49 +0100 <EvanR> really
2025-12-03 01:13:11 +0100 <EvanR> so like project1 is somehow set up with config 1, project 2 config 2 and everyone can actually keep it straight
2025-12-03 01:13:44 +0100skiindents by two spaces (including the whole module body, from the `where')
2025-12-03 01:13:44 +0100xff0x(~xff0x@2405:6580:b080:900:b577:52ee:470:5943) (Ping timeout: 244 seconds)
2025-12-03 01:14:23 +0100 <iqubic> Wait... are you serieous?
2025-12-03 01:15:24 +0100lambda_gibbon(~lambda_gi@2603:7080:ee00:37d8:11e:138e:d914:c117)
2025-12-03 01:15:29 +0100 <ski> of course
2025-12-03 01:16:04 +0100 <ski> (exception is if there's no `module ... where' part)
2025-12-03 01:16:54 +0100 <geekosaur> my response to said autoformatter fans is that as soon as there's more than one such the purpose is already defeated
2025-12-03 01:17:06 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds)
2025-12-03 01:17:09 +0100 <jackdk> EvanR: Yes, the configurable formatters I'm aware of can store the project config in version control next to the source.
2025-12-03 01:17:18 +0100 <geekosaur> and you will not convince everyone in the Haskell community to use One True Formatter
2025-12-03 01:17:47 +0100 <haskellbridge> <loonycyborg> if there was one true way then compiler would enforce it :P
2025-12-03 01:18:09 +0100 <geekosaur> (case in point, brittany's origins — and its demise)
2025-12-03 01:18:27 +0100 <haskellbridge> <loonycyborg> I think it emits warning if you stick "\t" somewhere already
2025-12-03 01:18:38 +0100 <haskellbridge> <loonycyborg> while in YAML they're illegal altogether
2025-12-03 01:18:49 +0100peterbecich(~Thunderbi@172.222.148.214) (Ping timeout: 255 seconds)
2025-12-03 01:19:57 +0100 <ski> i also not that seldom divide the source into pages (separated by form feeds) of size between thirtythree and sixtysix lines (c.f. "Riastradh's Lisp Style Rules" <https://mumble.net/~campbell/scheme/style.txt>)
2025-12-03 01:20:07 +0100lambda_gibbon(~lambda_gi@2603:7080:ee00:37d8:11e:138e:d914:c117) (Ping timeout: 264 seconds)
2025-12-03 01:20:42 +0100 <geekosaur> now I'm being reminded of C source code formatted with formfeeds in comments between functions, thanks
2025-12-03 01:28:13 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 01:33:29 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
2025-12-03 01:35:44 +0100Googulator88(~Googulato@85-238-68-117.pool.digikabel.hu)
2025-12-03 01:35:45 +0100Googulator11(~Googulato@2a01-036d-0106-479c-d9ec-010d-f188-ffcb.pool6.digikabel.hu) (Quit: Client closed)
2025-12-03 01:41:44 +0100CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 244 seconds)
2025-12-03 01:44:00 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 01:49:12 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-12-03 01:52:54 +0100DetourNetworkUK(DetourNetw@user/DetourNetworkUK) (Read error: Connection reset by peer)
2025-12-03 01:54:12 +0100DetourNetworkUK(~DetourNet@user/DetourNetworkUK) DetourNetworkUK
2025-12-03 01:56:20 +0100lambda_gibbon(~lambda_gi@2603:7080:ee00:37d8:11e:138e:d914:c117)
2025-12-03 02:01:14 +0100lambda_gibbon(~lambda_gi@2603:7080:ee00:37d8:11e:138e:d914:c117) (Ping timeout: 260 seconds)
2025-12-03 02:09:59 +0100xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
2025-12-03 02:13:58 +0100 <iqubic> I can't tell if my LSP is configured incorrectly or if weird things are happening here.
2025-12-03 02:14:25 +0100 <iqubic> By default, is hlint supposed to give a warning for unused function inputs?
2025-12-03 02:14:31 +0100 <iqubic> part1 :: String -> Int
2025-12-03 02:14:39 +0100 <iqubic> part1 i = undefined
2025-12-03 02:15:10 +0100 <iqubic> It's not telling me anything about the parameter i being unused.
2025-12-03 02:15:11 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 02:16:30 +0100acidjnk(~acidjnk@p200300d6e71719443da791614ae70cbb.dip0.t-ipconnect.de) (Ping timeout: 265 seconds)
2025-12-03 02:16:45 +0100 <davean> I'm at a loss why people care about style. It takes real work to make a style so bad it actually matters.
2025-12-03 02:18:18 +0100 <davean> You can do it, but I've not seen it outside of obfuscation contests.
2025-12-03 02:19:41 +0100omidmash5(~omidmash@user/omidmash) omidmash
2025-12-03 02:19:52 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2025-12-03 02:21:25 +0100omidmash(~omidmash@user/omidmash) (Ping timeout: 244 seconds)
2025-12-03 02:21:25 +0100omidmash5omidmash
2025-12-03 02:22:28 +0100 <probie> davean: Broken window theory. If the style is inconsistent, it'll encourage other bad behaviours that actually have consequences
2025-12-03 02:24:45 +0100 <davean> That doesn't follow the structure of the broken window theory to me
2025-12-03 02:24:55 +0100X-Scale(~ARM@6.67.114.89.rev.vodafone.pt) (Ping timeout: 240 seconds)
2025-12-03 02:25:00 +0100 <davean> The same "therefor" doesn't hold or apply
2025-12-03 02:25:48 +0100X-Scale(~ARM@50.65.114.89.rev.vodafone.pt) X-Scale
2025-12-03 02:26:37 +0100mehbark(~mehbark@joey.luug.ece.vt.edu)
2025-12-03 02:26:58 +0100mehbark(~mehbark@joey.luug.ece.vt.edu) (Changing host)
2025-12-03 02:26:58 +0100mehbark(~mehbark@user/mehbark) mehbark
2025-12-03 02:27:19 +0100sindu(~sindu@2.148.32.207.tmi.telenormobil.no) (Ping timeout: 240 seconds)
2025-12-03 02:30:43 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 02:31:56 +0100img(~img@user/img) (Quit: ZNC 1.10.1 - https://znc.in)
2025-12-03 02:32:46 +0100trickard(~trickard@cpe-85-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
2025-12-03 02:33:00 +0100trickard_(~trickard@cpe-85-98-47-163.wireline.com.au)
2025-12-03 02:33:15 +0100img(~img@user/img) img
2025-12-03 02:33:28 +0100 <davean> "I don't like their style" is different from "this isn't maintained. The equivilence for the broken window theory would be coming across a place with gothic arches
2025-12-03 02:34:07 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection)
2025-12-03 02:35:22 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-12-03 02:36:24 +0100divya(divya@140.238.251.170) (Ping timeout: 244 seconds)
2025-12-03 02:44:24 +0100lambda_gibbon(~lambda_gi@2603:7080:ee00:37d8:11e:138e:d914:c117)
2025-12-03 02:46:31 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 02:48:34 +0100lambda_gibbon(~lambda_gi@2603:7080:ee00:37d8:11e:138e:d914:c117) (Ping timeout: 246 seconds)
2025-12-03 02:52:55 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
2025-12-03 02:55:51 +0100 <geekosaur> the usual argument I hear for forcing formatting in projects is they usually enforce a style that minimizes diffs
2025-12-03 03:02:04 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-12-03 03:02:08 +0100lambda_gibbon(~lambda_gi@2603:7080:ee00:37d8:11e:138e:d914:c117)
2025-12-03 03:04:34 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 03:06:46 +0100lambda_gibbon(~lambda_gi@2603:7080:ee00:37d8:11e:138e:d914:c117) (Ping timeout: 265 seconds)
2025-12-03 03:07:33 +0100peterbecich(~Thunderbi@172.222.148.214) peterbecich
2025-12-03 03:09:38 +0100ttybitnik(~ttybitnik@user/wolper) (Remote host closed the connection)
2025-12-03 03:09:40 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
2025-12-03 03:20:18 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 03:24:56 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
2025-12-03 03:33:34 +0100Tuplanolla(~Tuplanoll@91-152-225-194.elisa-laajakaista.fi) (Quit: Leaving.)
2025-12-03 03:34:24 +0100finsternis(~X@23.226.237.192) finsternis
2025-12-03 03:36:05 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 03:36:56 +0100machinedgod(~machinedg@d75-159-126-101.abhsia.telus.net) (Ping timeout: 240 seconds)
2025-12-03 03:40:43 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2025-12-03 03:49:35 +0100wbooze(~wbooze@2001-4dd7-9813-0-4568-5322-9334-ddaa.ipv6dyn.netcologne.de) Inline
2025-12-03 03:51:52 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 03:52:15 +0100trickard_trickard
2025-12-03 03:56:20 +0100AlexNoo_(~AlexNoo@85.174.183.177)
2025-12-03 03:56:35 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-12-03 03:57:50 +0100AlexZenon(~alzenon@85.174.183.216) (Ping timeout: 245 seconds)
2025-12-03 03:59:35 +0100AlexNoo(~AlexNoo@85.174.183.216) (Ping timeout: 240 seconds)
2025-12-03 04:01:57 +0100AlexZenon(~alzenon@85.174.183.177)
2025-12-03 04:04:41 +0100 <EvanR> that would be a good argument
2025-12-03 04:04:43 +0100 <EvanR> if it were true
2025-12-03 04:05:01 +0100 <EvanR> auto formatting after a code change may have collateral damage when hit with the autoformatter
2025-12-03 04:05:05 +0100humasect(~humasect@dyn-192-249-132-90.nexicom.net) humasect
2025-12-03 04:07:41 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 04:08:28 +0100mesaoptimizer(~user@user/PapuaHardyNet) (Remote host closed the connection)
2025-12-03 04:12:08 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
2025-12-03 04:20:27 +0100 <geekosaur> theoretically you only get that when initially applying formatting
2025-12-03 04:21:20 +0100vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 240 seconds)
2025-12-03 04:23:04 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 04:23:16 +0100vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2025-12-03 04:25:54 +0100 <EvanR> with a properly designed algorithm?
2025-12-03 04:26:07 +0100 <EvanR> is there a no collateral damage theorem
2025-12-03 04:28:42 +0100td_(~td@i53870902.versanet.de) (Ping timeout: 252 seconds)
2025-12-03 04:29:35 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
2025-12-03 04:30:20 +0100td_(~td@i5387093E.versanet.de)
2025-12-03 04:31:59 +0100peterbecich(~Thunderbi@172.222.148.214) (Ping timeout: 250 seconds)
2025-12-03 04:35:28 +0100humasect(~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection)
2025-12-03 04:37:28 +0100inline__(~wbooze@cgn-195-14-219-152.nc.de) Inline
2025-12-03 04:40:30 +0100wbooze(~wbooze@2001-4dd7-9813-0-4568-5322-9334-ddaa.ipv6dyn.netcologne.de) (Ping timeout: 244 seconds)
2025-12-03 04:41:06 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 04:45:40 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-12-03 04:56:50 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 05:01:34 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds)
2025-12-03 05:07:56 +0100oppili-oppili
2025-12-03 05:07:56 +0100oppili(~oppili@lewi-27-b2-v4wan-165682-cust505.vm4.cable.virginm.net) (Changing host)
2025-12-03 05:07:56 +0100oppili(~oppili@user/nerdypepper) nerdy
2025-12-03 05:11:58 +0100Square(~Square@user/square) Square
2025-12-03 05:12:37 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 05:13:54 +0100peterbecich(~Thunderbi@172.222.148.214) peterbecich
2025-12-03 05:15:53 +0100Googulator45(~Googulato@2a01-036d-0106-479c-d9ec-010d-f188-ffcb.pool6.digikabel.hu)
2025-12-03 05:15:53 +0100Googulator88(~Googulato@85-238-68-117.pool.digikabel.hu) (Quit: Client closed)
2025-12-03 05:16:09 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Remote host closed the connection)
2025-12-03 05:17:49 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-12-03 05:18:09 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2025-12-03 05:28:26 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 05:32:55 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
2025-12-03 05:44:13 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 05:48:31 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
2025-12-03 05:50:01 +0100 <haskellbridge> <zoil> i cant beleive i went to all the trouble of putting together an example just to discover the advice was corrupt
2025-12-03 05:52:12 +0100 <haskellbridge> <zoil> Leary
2025-12-03 05:52:13 +0100 <haskellbridge> ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/meQNVtzNxaPzTuQoVMpGePld/Wmc2FsApiyo (7 lines)
2025-12-03 05:52:42 +0100 <haskellbridge> <zoil> i didnt read the bit where it was "and then you get these new constraints instead"
2025-12-03 05:52:45 +0100 <haskellbridge> <zoil> ...
2025-12-03 05:52:56 +0100 <haskellbridge> <zoil> _thats the whole point_
2025-12-03 05:53:26 +0100 <haskellbridge> <zoil> it wasnt a question about "how do i refactor these dumb constraints so i can carry around a more effecient expression"
2025-12-03 05:53:36 +0100 <haskellbridge> <zoil> it was, whats up with having to carry around these constraints
2025-12-03 05:54:00 +0100 <haskellbridge> <zoil> why cant I _assert to the compiler_ that the exhaustiveness is something i have ensured I have taken care of
2025-12-03 05:54:16 +0100 <haskellbridge> <zoil> if i have to tell it that Bool has an Eq instance, then its fine
2025-12-03 05:54:35 +0100 <haskellbridge> <zoil> but if its, that the head and tail of a hetroginous container both have a recursive instance
2025-12-03 05:54:39 +0100 <EvanR> a type level trust me
2025-12-03 05:54:43 +0100 <EvanR> sounds dangerous
2025-12-03 05:54:57 +0100 <haskellbridge> <zoil> but we have exhaustiveness elsewhere
2025-12-03 05:55:03 +0100 <haskellbridge> <zoil> maybe not that the user can specify it
2025-12-03 05:55:20 +0100 <haskellbridge> <zoil> we have had this whole dependant types singletons debate for years
2025-12-03 05:55:25 +0100 <haskellbridge> <zoil> isnt this the whole point!?
2025-12-03 05:55:43 +0100 <haskellbridge> <zoil> these damn eta constraints or whatever they are
2025-12-03 05:56:06 +0100 <EvanR> every time I disable the type system in e.g. C it usually results in a segfault xD
2025-12-03 05:56:06 +0100 <EvanR> it's crazy
2025-12-03 05:56:06 +0100 <EvanR> how good humans are at messing up logic
2025-12-03 05:56:15 +0100 <haskellbridge> <zoil> if its an exhaustiveness issue, thats at least an expression of the problem in a way, that, at least personally, i have never heard it phrased
2025-12-03 05:56:51 +0100 <haskellbridge> <zoil> EvanR: sure, i dont want some unknown way to break the compiler
2025-12-03 05:56:57 +0100 <haskellbridge> <zoil> we wouldnt know how to give reasonable errors
2025-12-03 05:57:07 +0100 <haskellbridge> <zoil> "you aserted something wrong!"
2025-12-03 05:57:24 +0100 <haskellbridge> <zoil> but still. languages like lean have this whole business dedicated to assertion proving
2025-12-03 05:57:44 +0100 <EvanR> does lean let you explicitly deal with or disable exhaustiveness
2025-12-03 05:57:47 +0100 <haskellbridge> <zoil> its like. iv even had situations where i pick up a constraint like 1 + n ~ n + 1
2025-12-03 05:58:15 +0100 <haskellbridge> <zoil> EvanR: idk how lean works. i think its more like a hackage for assertions
2025-12-03 05:58:23 +0100marinelli(~weechat@gateway/tor-sasl/marinelli) (Quit: marinelli)
2025-12-03 05:58:40 +0100 <haskellbridge> <zoil> like, there is some transistivity axiom that allows you to prove something and it does everything like that in a rigerous derived way
2025-12-03 05:58:57 +0100 <glguy> zoil: the thing you were asking about earlier wasn't about exhaustiveness, it's about not knowing what instance to use at runtime
2025-12-03 05:59:20 +0100 <haskellbridge> <zoil> there was some confusion, which iiuc, is because it requires 2 instances
2025-12-03 05:59:30 +0100 <haskellbridge> <zoil> iiuc thats a problem because its not exhaustive
2025-12-03 05:59:43 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 06:00:14 +0100 <EvanR> exhaustive sounds like something to do with a closed world assumption. type classes are open world and can never be exhaustive
2025-12-03 06:00:32 +0100 <EvanR> for all types there either is or not an instance
2025-12-03 06:00:49 +0100 <haskellbridge> <zoil> its saying (f :: [Type] -> Constraint) (xs :: [Type]) instance does not exist. and im saying "but i gave you a f [], and a f (x:xs) case, foolish compiler"
2025-12-03 06:00:49 +0100 <EvanR> (yet)
2025-12-03 06:01:17 +0100 <haskellbridge> <zoil> its exhaustive in the sum GADT cases
2025-12-03 06:01:21 +0100 <haskellbridge> <zoil> its not an open datatype
2025-12-03 06:01:35 +0100 <haskellbridge> <zoil> if it was a data family i would agree
2025-12-03 06:01:45 +0100 <haskellbridge> <zoil> but its not, so i have something that can be exhaustive
2025-12-03 06:02:35 +0100 <haskellbridge> <zoil> it seems to be like "what!? more than one instance, im confused"
2025-12-03 06:02:38 +0100 <haskellbridge> <zoil> which doesnt seem right at all!!
2025-12-03 06:03:07 +0100 <haskellbridge> <zoil> its like "where is the xs case, i only see [] and (x:xs), this is not xs"
2025-12-03 06:03:19 +0100peterbecich(~Thunderbi@172.222.148.214) (Ping timeout: 260 seconds)
2025-12-03 06:03:26 +0100 <haskellbridge> <zoil> and the user is like "but it is!! its exhaustive!!"
2025-12-03 06:04:07 +0100marinelli(~weechat@gateway/tor-sasl/marinelli) marinelli
2025-12-03 06:04:26 +0100marinelli(~weechat@gateway/tor-sasl/marinelli) (Remote host closed the connection)
2025-12-03 06:04:45 +0100marinelli(~weechat@gateway/tor-sasl/marinelli) marinelli
2025-12-03 06:04:56 +0100 <haskellbridge> <zoil> then someone said, "so just put it in one instance, and like, match the cases by a type family"
2025-12-03 06:05:19 +0100 <haskellbridge> <zoil> and then someone else said "but this needs a type witness, use singletons"
2025-12-03 06:05:51 +0100 <haskellbridge> <zoil> and then there was this KnownNonempty thing where head and tail could be given value level case matching that would bring the type into scope
2025-12-03 06:06:20 +0100 <haskellbridge> <zoil> and then i picked up this KnownNonempty constraint, and this still indicates the compiler is not happy that the assertion is satisfied
2025-12-03 06:06:31 +0100 <haskellbridge> <zoil> it says. "no. idk this instance exists, put it in a constraint"
2025-12-03 06:06:34 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
2025-12-03 06:07:02 +0100 <haskellbridge> <zoil> because the instances for KnownNonempty have the same problem. idk if this can be solved by the same typefamily idea or something
2025-12-03 06:07:11 +0100 <haskellbridge> <zoil> or if its that GHC is not advanced, or what
2025-12-03 06:07:15 +0100 <EvanR> either you missed the simple way to do what you're doing, the only way to do it in haskell is so arcane that it's probably not worth it, or it's just impossible
2025-12-03 06:07:16 +0100 <haskellbridge> <zoil> so i need some expert input
2025-12-03 06:08:08 +0100 <EvanR> sophisticated stuff at the type level is just easily overcomplicated here
2025-12-03 06:08:39 +0100 <haskellbridge> <zoil> iiuc the "singletons idea" requires these exhastive instances are provided. and these have to be done in one class, and there was another idea to use type families to do this, but im totally confused.
2025-12-03 06:09:07 +0100 <haskellbridge> <zoil> i just want to be able to describe the situation so people can understand the issue and maybe help produce a working example
2025-12-03 06:10:11 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 06:10:21 +0100 <haskellbridge> <zoil> i had this example to work with so far; https://play.haskell.org/saved/GwyPOlmo
2025-12-03 06:11:06 +0100 <EvanR> cool
2025-12-03 06:11:34 +0100 <haskellbridge> <zoil> also, glguy suggested that the name singleton should not apply to the recursive KnownNE situation, but im not sure why
2025-12-03 06:11:40 +0100 <haskellbridge> <zoil> im not sure it matters
2025-12-03 06:12:04 +0100 <haskellbridge> <zoil> its like, a recursively defined case that covers many situations, as opposed to (an infinite number) of explicit assertions
2025-12-03 06:12:29 +0100 <EvanR> because KnownNE isn't even a type
2025-12-03 06:13:06 +0100 <EvanR> and you're making two instances of it, so what's "single" about that
2025-12-03 06:13:33 +0100 <haskellbridge> <zoil> sorry, WhichNE
2025-12-03 06:13:44 +0100 <haskellbridge> <zoil> data WhichNE xs where
2025-12-03 06:13:44 +0100 <haskellbridge> ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/QHgkurBjvEckITCLYEHUHCfc/FL5KnP9OiZg (3 lines)
2025-12-03 06:14:09 +0100 <haskellbridge> <zoil> its the singletons idea of having this type witness that is matchable upon values to bring the corresponding type into scope
2025-12-03 06:14:19 +0100 <haskellbridge> <zoil> if thats not what a singleston is, idk, what this is
2025-12-03 06:14:43 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2025-12-03 06:15:26 +0100 <haskellbridge> <zoil> here was glguys paste about how to use the type family to condense the two instances into one
2025-12-03 06:15:30 +0100 <haskellbridge> <zoil> https://paste.tomsmeding.com/UEfrQUiN
2025-12-03 06:15:46 +0100 <EvanR> anyway your code compiles so
2025-12-03 06:16:02 +0100 <haskellbridge> <zoil> you dont understand the issue!?
2025-12-03 06:16:07 +0100 <haskellbridge> <zoil> its picking up these constraints!
2025-12-03 06:16:08 +0100 <EvanR> absolutely not
2025-12-03 06:16:28 +0100 <haskellbridge> <zoil> the compiler will forever ask for a constraint to an instance that exists at top level
2025-12-03 06:16:38 +0100 <haskellbridge> <zoil> simply because it exists in a distributed way
2025-12-03 06:17:29 +0100 <haskellbridge> <zoil> it would be like if i wrote a function matching the [] and (x:xs) cases in different function cases, and it was like "the function is not defined"
2025-12-03 06:17:41 +0100 <haskellbridge> <zoil> just because it cant tell if its exhaustive in these cases
2025-12-03 06:18:52 +0100 <haskellbridge> <zoil> as long as its "i insist that the KnownNE constraint is explicity specified", then its failing to appreciate the instance has been written at top level
2025-12-03 06:19:06 +0100 <haskellbridge> <zoil> now, if theres a "special way" of doing this, like, ensuring everything is written in just one instance
2025-12-03 06:19:12 +0100 <haskellbridge> <zoil> then at least there is a workaround
2025-12-03 06:19:33 +0100 <haskellbridge> <zoil> which should be pretty clearly indicated! since otherwise this insane behaviour from the compiler is commonly encountered
2025-12-03 06:19:42 +0100 <haskellbridge> <zoil> or it indicates a compiler fix is required
2025-12-03 06:20:39 +0100 <haskellbridge> <zoil> "compiler is nolonger blind to instances defined over several cases"
2025-12-03 06:20:59 +0100 <haskellbridge> <zoil> but then, i could just give the basecase instance. and then it would be like "wtf, this doesnt match"
2025-12-03 06:21:35 +0100 <haskellbridge> <zoil> "nonexhaustive instance encountered in this code you were trying to write on line 11"
2025-12-03 06:22:13 +0100 <haskellbridge> <zoil> which it _currently always says_
2025-12-03 06:22:33 +0100 <haskellbridge> <zoil> except in the case where no pattern matching takes place
2025-12-03 06:23:15 +0100 <haskellbridge> <zoil> then it is like "i see the instance exists, i will not require the constraint is explicitly specified, i cannot forsee an instance where the instance does not exist where then i would require it as a constraint"
2025-12-03 06:25:40 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 06:25:43 +0100EvanRlooks at line 11
2025-12-03 06:25:57 +0100 <EvanR> there's nothing there
2025-12-03 06:26:38 +0100 <haskellbridge> <zoil> > :-(
2025-12-03 06:27:11 +0100 <haskellbridge> <zoil> > :-|
2025-12-03 06:27:19 +0100 <haskellbridge> <zoil> ... >:-(
2025-12-03 06:28:01 +0100 <haskellbridge> <zoil> i dont know why this type witness idea was even suggested
2025-12-03 06:28:12 +0100 <haskellbridge> <zoil> there was apparently something different about show and read
2025-12-03 06:28:16 +0100 <EvanR> what are you trying to do
2025-12-03 06:28:33 +0100 <haskellbridge> <zoil> like, show could resolve the type, but read would require something like an instance version of allowambiguous types
2025-12-03 06:28:50 +0100 <haskellbridge> <zoil> EvanR: im sorry mate, im not enjoying you just talking past everything iv written
2025-12-03 06:29:21 +0100 <haskellbridge> <zoil> i think "what im trying to do" is very much inferable from the discussion so far.
2025-12-03 06:29:22 +0100 <EvanR> I guess you can keep spamming the channel with nonsense
2025-12-03 06:29:32 +0100 <haskellbridge> <zoil> THANKS!
2025-12-03 06:29:39 +0100 <EvanR> without being rudely interrupted
2025-12-03 06:29:48 +0100 <haskellbridge> <zoil> ill guess you can just keep using a time machine to write a compiler without any focus grouping from the future
2025-12-03 06:30:01 +0100 <haskellbridge> <zoil> im not trying to be rude
2025-12-03 06:30:15 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
2025-12-03 06:30:28 +0100 <haskellbridge> <zoil> if you could maybe not just, stonewall me, and then, as soon as this is noticed, start accusing me of not talking to you in the prescribed manner
2025-12-03 06:30:41 +0100 <haskellbridge> <zoil> what specifically is it that you dont understand
2025-12-03 06:31:05 +0100 <haskellbridge> <zoil> instead of just this most vague assertion that you cannot seem to convey any degree of understanding at all of the situation described
2025-12-03 06:31:07 +0100 <haskellbridge> <zoil> its vexating
2025-12-03 06:31:59 +0100 <haskellbridge> <zoil> "its a burden of proof, i insist i dont understand the users query and by virtue of this its nonesense"
2025-12-03 06:32:18 +0100 <haskellbridge> <zoil> its an awful precedent and it makes our community inpenetrable and unfrinedly
2025-12-03 06:36:23 +0100michalz(~michalz@185.246.207.205)
2025-12-03 06:41:29 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 06:45:54 +0100Googulator45(~Googulato@2a01-036d-0106-479c-d9ec-010d-f188-ffcb.pool6.digikabel.hu) (Quit: Client closed)
2025-12-03 06:45:56 +0100Googulator88(~Googulato@2a01-036d-0106-479c-d9ec-010d-f188-ffcb.pool6.digikabel.hu)
2025-12-03 06:46:29 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-12-03 06:48:27 +0100takuan(~takuan@d8D86B9E9.access.telenet.be)
2025-12-03 06:48:55 +0100trickard(~trickard@cpe-85-98-47-163.wireline.com.au) (Read error: Connection reset by peer)
2025-12-03 06:49:08 +0100trickard_(~trickard@cpe-85-98-47-163.wireline.com.au)
2025-12-03 06:54:08 +0100 <probie> +1 for could not infer what you're trying to do. There's no need to be mean about it. You're obviously frustrated by something, type families are involved, you did something with singletons but it was the wrong path(?)
2025-12-03 06:55:00 +0100 <probie> Since your problem seems to be at the type level, can you give an expression you want to type check, or not type check as appropriate?
2025-12-03 06:55:35 +0100Fijxu(~Fijxu@user/fijxu) (Quit: XD!!)
2025-12-03 06:56:10 +0100Square2(~Square4@user/square) Square
2025-12-03 06:57:02 +0100Fijxu(~Fijxu@user/fijxu) fijxu
2025-12-03 06:57:16 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 06:57:41 +0100Fijxu(~Fijxu@user/fijxu) (Remote host closed the connection)
2025-12-03 06:59:01 +0100Fijxu(~Fijxu@user/fijxu) fijxu
2025-12-03 06:59:15 +0100Square(~Square@user/square) (Ping timeout: 240 seconds)
2025-12-03 07:02:08 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
2025-12-03 07:02:55 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 07:05:30 +0100poscat(~poscat@user/poscat) poscat
2025-12-03 07:06:26 +0100trickard_trickard
2025-12-03 07:07:08 +0100poscat0x04(~poscat@user/poscat) (Ping timeout: 244 seconds)
2025-12-03 07:07:20 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
2025-12-03 07:14:27 +0100 <haskellbridge> <zoil> thanks, im sorry i rage quit
2025-12-03 07:16:19 +0100 <haskellbridge> <zoil> so far i have this;
2025-12-03 07:16:19 +0100 <haskellbridge> https://play.haskell.org/saved/GwyPOlmo
2025-12-03 07:16:40 +0100 <haskellbridge> <zoil> er, sorry, that was the previous version, now i have this
2025-12-03 07:16:41 +0100 <haskellbridge> <zoil> https://play.haskell.org/saved/GJqAvv67
2025-12-03 07:17:30 +0100 <haskellbridge> <zoil> its saying the injectivity condition here is not accepted
2025-12-03 07:17:30 +0100 <haskellbridge> <zoil> type family StatefulTransfers (xs :: Nonempty Type) i o = (c :: Constraint) | c -> xs i o where
2025-12-03 07:18:04 +0100 <haskellbridge> <zoil> like, i cant get the fundeps to go through the injective type family properly
2025-12-03 07:18:32 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 07:21:39 +0100 <haskellbridge> <zoil> so, whatever this apparent workaround was supposed to acheive, it cant
2025-12-03 07:21:57 +0100 <haskellbridge> <zoil> because the injective type family fails to impart the same data as the fundep
2025-12-03 07:22:24 +0100 <haskellbridge> <zoil> i have concluded that the compiler hates me, and i was wrong not to have rage quit.
2025-12-03 07:23:15 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
2025-12-03 07:23:27 +0100 <Leary> Let's kill all the cruft so others can follow along; the core issue is this: https://play.haskell.org/saved/BeYSIaVz
2025-12-03 07:24:15 +0100 <Leary> There are two instances, and GHC won't let you pretend they're the same as `Read (Two b)`, because that implies you have a way to choose which instance you want to use **at runtime** from type information alone.
2025-12-03 07:26:16 +0100peterbecich(~Thunderbi@172.222.148.214) peterbecich
2025-12-03 07:26:49 +0100 <EvanR> thanks
2025-12-03 07:34:02 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine)
2025-12-03 07:34:18 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-12-03 07:36:12 +0100lambda_gibbon(~lambda_gi@2603:7080:ee00:37d8:11e:138e:d914:c117)
2025-12-03 07:39:11 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 250 seconds)
2025-12-03 07:40:44 +0100lambda_gibbon(~lambda_gi@2603:7080:ee00:37d8:11e:138e:d914:c117) (Ping timeout: 260 seconds)
2025-12-03 07:42:21 +0100haritz(~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in)
2025-12-03 07:45:10 +0100chenjf(~chenjf@68.64.178.54)
2025-12-03 07:49:19 +0100chenjf(~chenjf@68.64.178.54) (Client Quit)
2025-12-03 07:51:13 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn