Logs: liberachat/#haskell
| 2026-04-19 15:52:28 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-19 15:56:02 | × | misterfish quits (~misterfis@84.53.85.146) (Ping timeout: 248 seconds) |
| 2026-04-19 15:57:22 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2026-04-19 15:58:34 | <janus> | i talked about iso-inductive types a few days back |
| 2026-04-19 15:58:53 | <janus> | and now i found solomon did a chain of interpreters https://github.com/solomon-b/lambda-calculus-hs/blob/main/main/09b-IsoInductiveTypes.hs |
| 2026-04-19 15:58:59 | × | arandombit quits (~arandombi@user/arandombit) (Ping timeout: 244 seconds) |
| 2026-04-19 15:59:26 | <janus> | it seems like the main concern was about whether the fold-unfolding would retain the right laziness |
| 2026-04-19 16:00:06 | <janus> | but i didn't actually understand why it wouldn't |
| 2026-04-19 16:00:12 | → | arandombit joins (~arandombi@2a02:2455:8656:7100:19a4:6d16:82eb:d1) |
| 2026-04-19 16:00:12 | × | arandombit quits (~arandombi@2a02:2455:8656:7100:19a4:6d16:82eb:d1) (Changing host) |
| 2026-04-19 16:00:12 | → | arandombit joins (~arandombi@user/arandombit) |
| 2026-04-19 16:02:15 | × | jmcantrell_ quits (~weechat@user/jmcantrell) (Ping timeout: 245 seconds) |
| 2026-04-19 16:07:51 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-19 16:08:38 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2026-04-19 16:09:23 | → | gmg joins (~user@user/gehmehgeh) |
| 2026-04-19 16:12:37 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-04-19 16:14:24 | → | uli-fem joins (~uli-fem@115.128.71.34) |
| 2026-04-19 16:16:39 | × | ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 244 seconds) |
| 2026-04-19 16:18:26 | → | ezzieyguywuf joins (~Unknown@user/ezzieyguywuf) |
| 2026-04-19 16:19:33 | × | uli-fem quits (~uli-fem@115.128.71.34) (Ping timeout: 272 seconds) |
| 2026-04-19 16:19:39 | × | pabs3 quits (~pabs3@user/pabs3) (Ping timeout: 255 seconds) |
| 2026-04-19 16:23:15 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-19 16:24:45 | → | pabs3 joins (~pabs3@user/pabs3) |
| 2026-04-19 16:25:22 | × | arandombit quits (~arandombi@user/arandombit) (Ping timeout: 248 seconds) |
| 2026-04-19 16:25:49 | → | arandombit joins (~arandombi@user/arandombit) |
| 2026-04-19 16:26:22 | → | alhazrod joins (uid662262@user/alhazrod) |
| 2026-04-19 16:27:58 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-04-19 16:38:38 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-19 16:39:28 | → | troojg joins (~troojg@user/troojg) |
| 2026-04-19 16:43:03 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-04-19 16:48:21 | → | uli-fem joins (~uli-fem@115.128.71.34) |
| 2026-04-19 16:49:16 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-19 16:52:49 | × | uli-fem quits (~uli-fem@115.128.71.34) (Ping timeout: 245 seconds) |
| 2026-04-19 16:53:30 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-04-19 16:54:53 | × | tusko quits (~uwu@user/tusko) (Remote host closed the connection) |
| 2026-04-19 16:55:08 | → | tusko joins (~uwu@user/tusko) |
| 2026-04-19 17:04:39 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-19 17:07:48 | × | skum quits (~skum@user/skum) (Ping timeout: 255 seconds) |
| 2026-04-19 17:09:52 | → | skum joins (~skum@user/skum) |
| 2026-04-19 17:11:19 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-04-19 17:11:40 | → | peterbecich joins (~Thunderbi@71.84.33.135) |
| 2026-04-19 17:14:36 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2026-04-19 17:22:21 | → | uli-fem joins (~uli-fem@115.128.71.34) |
| 2026-04-19 17:22:42 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-19 17:25:48 | → | misterfish joins (~misterfis@84.53.85.146) |
| 2026-04-19 17:26:02 | × | tromp quits (~textual@2001:1c00:340e:2700:bd40:ea59:f230:b9cd) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-04-19 17:27:09 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-04-19 17:28:56 | × | tristanC quits (~tristanC@2602:4b:ac7b:500:701e:9a24:a355:5957) (Ping timeout: 252 seconds) |
| 2026-04-19 17:29:22 | × | uli-fem quits (~uli-fem@115.128.71.34) (Ping timeout: 248 seconds) |
| 2026-04-19 17:30:35 | × | troojg quits (~troojg@user/troojg) (Ping timeout: 252 seconds) |
| 2026-04-19 17:34:50 | × | misterfish quits (~misterfis@84.53.85.146) (Ping timeout: 256 seconds) |
| 2026-04-19 17:38:46 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-19 17:39:44 | → | Square2 joins (~Square@user/square) |
| 2026-04-19 17:41:38 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 2026-04-19 17:41:44 | → | bitdex_ joins (~bitdex@gateway/tor-sasl/bitdex) |
| 2026-04-19 17:43:05 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2026-04-19 17:45:18 | → | uli-fem joins (~uli-fem@115.128.71.34) |
| 2026-04-19 17:45:22 | → | tromp joins (~textual@2001:1c00:340e:2700:bd40:ea59:f230:b9cd) |
| 2026-04-19 17:45:29 | → | Enrico63 joins (~Enrico63@host-95-249-71-165.retail.telecomitalia.it) |
| 2026-04-19 17:49:29 | × | uli-fem quits (~uli-fem@115.128.71.34) (Ping timeout: 248 seconds) |
| 2026-04-19 17:50:16 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-19 17:50:25 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 265 seconds) |
| 2026-04-19 17:54:43 | × | Enrico63 quits (~Enrico63@host-95-249-71-165.retail.telecomitalia.it) (Quit: Client closed) |
| 2026-04-19 17:55:03 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-04-19 18:03:36 | × | peterbecich quits (~Thunderbi@71.84.33.135) (Ping timeout: 244 seconds) |
| 2026-04-19 18:05:39 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-19 18:06:12 | → | peterbecich joins (~Thunderbi@71.84.33.135) |
| 2026-04-19 18:10:23 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2026-04-19 18:12:34 | × | peterbecich quits (~Thunderbi@71.84.33.135) (Ping timeout: 248 seconds) |
| 2026-04-19 18:13:14 | → | __monty__ joins (~toonn@user/toonn) |
| 2026-04-19 18:14:22 | <monochrom> | \∩/ I guessed right about why Dhall mandates handwritten types for functions (e.g. \(x:Natural) -> x+x). Last time I saw that requirement was System F. So I thought "is it just because Dhall is System F? and if so, can I do the usual System F trick to sneak in any positively recursive ADT?" The answer is yes and yes! In fact they have a howto for that! |
| 2026-04-19 18:14:31 | <monochrom> | https://docs.dhall-lang.org/howtos/How-to-translate-recursive-code-to-Dhall.html |
| 2026-04-19 18:16:09 | <monochrom> | So the language doesn't directly allow recursive ADT but they tell you that the backdoor is rank-n polymorphic church encoding. |
| 2026-04-19 18:17:34 | → | gmg joins (~user@user/gehmehgeh) |
| 2026-04-19 18:21:03 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-19 18:21:04 | → | machinedgod joins (~machinedg@d172-219-48-230.abhsia.telus.net) |
| 2026-04-19 18:21:15 | → | uli-fem joins (~uli-fem@115.128.71.34) |
| 2026-04-19 18:24:03 | lol_ | is now known as jcarpenter2 |
| 2026-04-19 18:25:43 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-04-19 18:25:49 | × | uli-fem quits (~uli-fem@115.128.71.34) (Ping timeout: 244 seconds) |
| 2026-04-19 18:28:15 | <monochrom> | More completely (pun!), handwritten types for lambdas and explicity type applications when calling polymorphic functions. So a better example is: Haskell's "map (\x -> x>0)" becomes Dhall's "map Natural Bool (\(x:Natural -> x>0))". That really looks like System F. |
| 2026-04-19 18:29:58 | <monochrom> | plus the meta-clue that Gabriella is very PLT well-informed (unlike the makers of Perl, Python, PHP) so if she chose this there must be a PLT reason. |
| 2026-04-19 18:36:25 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-19 18:41:45 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2026-04-19 18:42:42 | × | puke quits (~puke@user/puke) (Ping timeout: 250 seconds) |
| 2026-04-19 18:51:16 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-19 18:51:31 | × | gabriel_sevecek quits (~gabriel@92-180-224-71.dynamic.orange.sk) (Quit: WeeChat 4.9.0) |
| 2026-04-19 18:52:26 | → | gabriel_sevecek joins (~gabriel@92-180-224-71.dynamic.orange.sk) |
| 2026-04-19 18:57:32 | → | uli-fem joins (~uli-fem@115.128.71.34) |
| 2026-04-19 18:58:02 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-04-19 19:02:06 | × | uli-fem quits (~uli-fem@115.128.71.34) (Ping timeout: 256 seconds) |
| 2026-04-19 19:03:38 | <monochrom> | OK I'm going to teach Dhall in my PL course!!! |
| 2026-04-19 19:04:13 | <monochrom> | It is not every day that one finds a real-world reason to teach System F to undergrads! |
| 2026-04-19 19:04:24 | <monochrom> | or rather s/reason/excuse/ haha |
| 2026-04-19 19:04:45 | → | uli-fem joins (~uli-fem@115.128.71.34) |
| 2026-04-19 19:09:00 | × | uli-fem quits (~uli-fem@115.128.71.34) (Ping timeout: 246 seconds) |
| 2026-04-19 19:09:19 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-19 19:13:52 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-04-19 19:17:49 | → | karenw joins (~karenw@user/karenw) |
| 2026-04-19 19:24:35 | → | tristanC joins (~tristanC@2602:61:712f:b700:a215:c067:33c4:f43e) |
All times are in UTC.