Logs: liberachat/#haskell
| 2025-10-15 19:28:58 | × | lieven quits (~mal@ns2.wyrd.be) (Ping timeout: 244 seconds) |
| 2025-10-15 19:28:58 | × | pmk quits (6afe4476a1@2a03:6000:1812:100::26d) (Ping timeout: 244 seconds) |
| 2025-10-15 19:28:58 | × | geekosaur quits (sid609282@xmonad/geekosaur) (Ping timeout: 244 seconds) |
| 2025-10-15 19:28:58 | × | fn_lumi quits (3d621153a5@2a03:6000:1812:100::df7) (Ping timeout: 244 seconds) |
| 2025-10-15 19:28:58 | × | b0o quits (0e4a0bf4c9@2a03:6000:1812:100::1bf) (Ping timeout: 244 seconds) |
| 2025-10-15 19:28:58 | × | nshepperd2 quits (~nshepperd@2a01:4f9:3b:4cc9::2) (Ping timeout: 244 seconds) |
| 2025-10-15 19:28:58 | × | bggd__ quits (~bgg@2a01:e0a:819:1510:a422:7a58:5231:4299) (Ping timeout: 244 seconds) |
| 2025-10-15 19:28:58 | × | cheater quits (~fuck@84-115-208-145.cable.dynamic.surfer.at) (Read error: Connection reset by peer) |
| 2025-10-15 19:28:58 | × | annamalai quits (~annamalai@157.32.214.152) (Ping timeout: 244 seconds) |
| 2025-10-15 19:28:58 | ggb_ | is now known as ggb |
| 2025-10-15 19:28:59 | fn_lumi_ | is now known as fn_lumi |
| 2025-10-15 19:28:59 | geekosaur_ | is now known as geekosaur |
| 2025-10-15 19:28:59 | rubin55_ | is now known as rubin55 |
| 2025-10-15 19:28:59 | b0o_ | is now known as b0o |
| 2025-10-15 19:28:59 | nshepperd21 | is now known as nshepperd2 |
| 2025-10-15 19:29:25 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-10-15 19:30:39 | × | tromp quits (~textual@2001:1c00:3487:1b00:cdf:654a:2a7f:261) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-10-15 19:31:11 | → | yahb2 joins (~yahb2@user/tomsmeding/bot/yahb2) |
| 2025-10-15 19:31:11 | ChanServ | sets mode +v yahb2 |
| 2025-10-15 19:31:55 | → | arandombit joins (~arandombi@user/arandombit) |
| 2025-10-15 19:32:03 | × | FANTOM quits (~fantom@90.244.183.5) (Ping timeout: 256 seconds) |
| 2025-10-15 19:32:20 | × | qqe quits (~qqq@185.54.23.200) (Quit: Lost terminal) |
| 2025-10-15 19:34:02 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-10-15 19:35:19 | → | FANTOM joins (~fantom@90.244.183.5) |
| 2025-10-15 19:36:57 | → | op_4 joins (~tslil@user/op-4/x-9116473) |
| 2025-10-15 19:37:34 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 2025-10-15 19:38:11 | → | ProofTechnique_ joins (sid79547@id-79547.ilkley.irccloud.com) |
| 2025-10-15 19:39:31 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 2025-10-15 19:43:00 | → | ft joins (~ft@p4fc2a207.dip0.t-ipconnect.de) |
| 2025-10-15 19:43:38 | fgarcia | is now known as fgidim |
| 2025-10-15 19:44:32 | → | tromp joins (~textual@2001:1c00:3487:1b00:d983:2af2:5deb:9bbb) |
| 2025-10-15 19:48:46 | → | CiaoSen joins (~Jura@ipservice-092-210-206-067.092.210.pools.vodafone-ip.de) |
| 2025-10-15 19:51:44 | → | Tuplanolla joins (~Tuplanoll@91-159-187-167.elisa-laajakaista.fi) |
| 2025-10-15 19:55:35 | → | Googulator joins (~Googulato@2a01-036d-0106-03fa-648b-10cf-62d2-2877.pool6.digikabel.hu) |
| 2025-10-15 19:58:17 | × | Maeda quits (~Maeda@91-161-10-149.subs.proxad.net) (Quit: leaving) |
| 2025-10-15 19:58:46 | × | tromp quits (~textual@2001:1c00:3487:1b00:d983:2af2:5deb:9bbb) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-10-15 20:05:05 | × | chexum_ quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2025-10-15 20:05:52 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 2025-10-15 20:08:39 | <tomsmeding> | % data Fix f = In (f (Fix f)) ; deriving instance (forall a. Show a => Show (f a)) => Show (Fix f) |
| 2025-10-15 20:08:39 | <yahb2> | <no output> |
| 2025-10-15 20:08:47 | <tomsmeding> | % let x = In [x] in x |
| 2025-10-15 20:08:47 | <yahb2> | In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [I... |
| 2025-10-15 20:09:12 | → | tromp joins (~textual@2001:1c00:3487:1b00:d983:2af2:5deb:9bbb) |
| 2025-10-15 20:09:33 | <monochrom> | Would you like to s/data/newtype/ ? :) |
| 2025-10-15 20:09:57 | → | gustrb joins (~gustrb@191.243.134.87) |
| 2025-10-15 20:10:16 | <tomsmeding> | % newtype Fix f = In (f (Fix f)) ; deriving instance (forall a. Show a => Show (f a)) => Show (Fix f) |
| 2025-10-15 20:10:16 | <yahb2> | <no output> |
| 2025-10-15 20:10:18 | <tomsmeding> | % let x = In [x] in x |
| 2025-10-15 20:10:18 | <yahb2> | In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [In [I... |
| 2025-10-15 20:10:34 | <tomsmeding> | more efficient pointlessness! |
| 2025-10-15 20:10:57 | <mreh> | looks pointless to me :P |
| 2025-10-15 20:11:01 | <monochrom> | Infinite types lead to Infinity Wars. >:) |
| 2025-10-15 20:12:01 | → | haltsolver joins (~cmo@2604:3d09:207f:8000::d1dc) |
| 2025-10-15 20:15:39 | → | karenw joins (~karenw@user/karenw) |
| 2025-10-15 20:16:06 | <mreh> | I think I just made a new pb. Three day refactor, compiles, two runtime errors, and then everything just works. |
| 2025-10-15 20:16:14 | <tomsmeding> | hm, perhaps I should have written `repeat x` instead of `[x]`, for more recursion. :) |
| 2025-10-15 20:16:25 | <tomsmeding> | mreh: congrats! |
| 2025-10-15 20:18:44 | → | pavonia joins (~user@user/siracusa) |
| 2025-10-15 20:23:37 | × | tromp quits (~textual@2001:1c00:3487:1b00:d983:2af2:5deb:9bbb) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-10-15 20:25:36 | × | Googulator quits (~Googulato@2a01-036d-0106-03fa-648b-10cf-62d2-2877.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-10-15 20:25:38 | → | Googulator63 joins (~Googulato@2a01-036d-0106-03fa-648b-10cf-62d2-2877.pool6.digikabel.hu) |
| 2025-10-15 20:26:40 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Ping timeout: 272 seconds) |
| 2025-10-15 20:30:30 | → | inline joins (~inline@2a02:8071:57a1:1260:590e:ee4d:f63f:13ad) |
| 2025-10-15 20:36:35 | × | michalz_ quits (~michalz@185.246.207.222) (Remote host closed the connection) |
| 2025-10-15 20:36:49 | → | Vajb joins (~Vajb@n7o35ytoa19a9fdq6h6-1.v6.elisa-mobile.fi) |
| 2025-10-15 20:40:42 | → | tromp joins (~textual@2001:1c00:3487:1b00:d983:2af2:5deb:9bbb) |
| 2025-10-15 20:41:12 | × | trickard_ quits (~trickard@cpe-62-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-10-15 20:41:26 | → | trickard_ joins (~trickard@cpe-62-98-47-163.wireline.com.au) |
| 2025-10-15 20:42:43 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 2025-10-15 20:44:00 | → | jmcantrell joins (~weechat@user/jmcantrell) |
| 2025-10-15 20:44:15 | → | xmyth joins (~xmyth@user/xmyth) |
| 2025-10-15 20:46:12 | × | inline quits (~inline@2a02:8071:57a1:1260:590e:ee4d:f63f:13ad) (Ping timeout: 260 seconds) |
| 2025-10-15 20:47:22 | → | inline joins (~inline@ip-178-202-059-161.um47.pools.vodafone-ip.de) |
| 2025-10-15 20:50:28 | × | inline quits (~inline@ip-178-202-059-161.um47.pools.vodafone-ip.de) (Remote host closed the connection) |
| 2025-10-15 20:51:36 | → | inline joins (~inline@2a02:8071:57a1:1260:1c9a:31b4:1f4:c0dc) |
| 2025-10-15 20:53:27 | <monochrom> | Hot take: Lean/Agda programming is type tetris, Haskell dependent type programming is Proxy tetris. :) |
| 2025-10-15 20:53:56 | <geekosaur> | I'd say singleton tetris |
| 2025-10-15 20:54:40 | <tomsmeding> | I concur with singleton tetris |
| 2025-10-15 20:54:45 | <monochrom> | (I have been doing that for type-assured modulus arithmetic, e.g., a+b `mod` m, where m is determined by a phantom type.) |
| 2025-10-15 20:54:54 | <tomsmeding> | if you can suffice with Proxy then you aren't doing enough tetris |
| 2025-10-15 20:55:50 | <monochrom> | OK, I have also been doing withDict tetris. Is that OK? :) |
| 2025-10-15 20:56:05 | <monochrom> | (It's the only reason why Proxy suffices.) |
| 2025-10-15 20:56:07 | × | inline quits (~inline@2a02:8071:57a1:1260:1c9a:31b4:1f4:c0dc) (Ping timeout: 260 seconds) |
| 2025-10-15 20:56:11 | <tomsmeding> | oh you're taking the typeclasses approach to type-level haskell masochism |
| 2025-10-15 20:56:24 | <int-e> | monochrom: you need to be carefule when doing that; if things fit too well, your code disappears. |
| 2025-10-15 20:56:34 | <monochrom> | haha |
| 2025-10-15 20:57:01 | <EvanR> | GHC deletes your code if it type checks |
| 2025-10-15 20:57:09 | <EvanR> | in the modern version of that bug |
| 2025-10-15 20:57:21 | <tomsmeding> | I find singletons more verbose but also more powerful; my experience (doing type tetris) is that if the inference system is not clever enough to do what you want, you're suddenly in a bind, whereas with singletons it's limited by your programming (and tetris) skills only |
| 2025-10-15 20:57:34 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-10-15 20:58:07 | <EvanR> | there are ways to trick the type class system into "inferring" things right |
| 2025-10-15 20:58:26 | <EvanR> | which is where it gets dicey to understand |
| 2025-10-15 21:00:39 | → | Googulator8 joins (~Googulato@2a01-036d-0106-03fa-648b-10cf-62d2-2877.pool6.digikabel.hu) |
| 2025-10-15 21:00:39 | × | Googulator63 quits (~Googulato@2a01-036d-0106-03fa-648b-10cf-62d2-2877.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-10-15 21:01:20 | <tomsmeding> | suppose you have two type-level naturals that you want to add. If they're peano SNats and there's no library function for that, you just do the stupid peano addition |
| 2025-10-15 21:01:37 | <tomsmeding> | if they're type-level Nats with KnownNat constraints around, how are you going to conjure up a KnownNat (a + b)? |
| 2025-10-15 21:01:43 | <tomsmeding> | you... don't |
| 2025-10-15 21:01:45 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2025-10-15 21:01:51 | <tomsmeding> | unless you bring in a GHC plugin that does it for you |
| 2025-10-15 21:02:06 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
All times are in UTC.