Newest at the top
| 2026-04-19 19:17:49 +0000 | karenw | (~karenw@user/karenw) karenw |
| 2026-04-19 19:13:52 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-04-19 19:09:19 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-19 19:09:00 +0000 | uli-fem | (~uli-fem@115.128.71.34) (Ping timeout: 246 seconds) |
| 2026-04-19 19:04:45 +0000 | uli-fem | (~uli-fem@115.128.71.34) |
| 2026-04-19 19:04:24 +0000 | <monochrom> | or rather s/reason/excuse/ haha |
| 2026-04-19 19:04:13 +0000 | <monochrom> | It is not every day that one finds a real-world reason to teach System F to undergrads! |
| 2026-04-19 19:03:38 +0000 | <monochrom> | OK I'm going to teach Dhall in my PL course!!! |
| 2026-04-19 19:02:06 +0000 | uli-fem | (~uli-fem@115.128.71.34) (Ping timeout: 256 seconds) |
| 2026-04-19 18:58:02 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-04-19 18:57:32 +0000 | uli-fem | (~uli-fem@115.128.71.34) |
| 2026-04-19 18:52:26 +0000 | gabriel_sevecek | (~gabriel@92-180-224-71.dynamic.orange.sk) gabriel_sevecek |
| 2026-04-19 18:51:31 +0000 | gabriel_sevecek | (~gabriel@92-180-224-71.dynamic.orange.sk) (Quit: WeeChat 4.9.0) |
| 2026-04-19 18:51:16 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-19 18:42:42 +0000 | puke | (~puke@user/puke) (Ping timeout: 250 seconds) |
| 2026-04-19 18:41:45 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2026-04-19 18:36:25 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-19 18:29:58 +0000 | <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:28:15 +0000 | <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:25:49 +0000 | uli-fem | (~uli-fem@115.128.71.34) (Ping timeout: 244 seconds) |
| 2026-04-19 18:25:43 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-04-19 18:24:03 +0000 | lol_ | jcarpenter2 |
| 2026-04-19 18:21:15 +0000 | uli-fem | (~uli-fem@115.128.71.34) |
| 2026-04-19 18:21:04 +0000 | machinedgod | (~machinedg@d172-219-48-230.abhsia.telus.net) machinedgod |
| 2026-04-19 18:21:03 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-19 18:17:34 +0000 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2026-04-19 18:16:09 +0000 | <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:14:31 +0000 | <monochrom> | https://docs.dhall-lang.org/howtos/How-to-translate-recursive-code-to-Dhall.html |
| 2026-04-19 18:14:22 +0000 | <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:13:14 +0000 | __monty__ | (~toonn@user/toonn) toonn |
| 2026-04-19 18:12:34 +0000 | peterbecich | (~Thunderbi@71.84.33.135) (Ping timeout: 248 seconds) |
| 2026-04-19 18:10:23 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2026-04-19 18:06:12 +0000 | peterbecich | (~Thunderbi@71.84.33.135) peterbecich |
| 2026-04-19 18:05:39 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-19 18:03:36 +0000 | peterbecich | (~Thunderbi@71.84.33.135) (Ping timeout: 244 seconds) |
| 2026-04-19 17:55:03 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-04-19 17:54:43 +0000 | Enrico63 | (~Enrico63@host-95-249-71-165.retail.telecomitalia.it) (Quit: Client closed) |
| 2026-04-19 17:50:25 +0000 | gmg | (~user@user/gehmehgeh) (Ping timeout: 265 seconds) |
| 2026-04-19 17:50:16 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-19 17:49:29 +0000 | uli-fem | (~uli-fem@115.128.71.34) (Ping timeout: 248 seconds) |
| 2026-04-19 17:45:29 +0000 | Enrico63 | (~Enrico63@host-95-249-71-165.retail.telecomitalia.it) Enrico63 |
| 2026-04-19 17:45:22 +0000 | tromp | (~textual@2001:1c00:340e:2700:bd40:ea59:f230:b9cd) |
| 2026-04-19 17:45:18 +0000 | uli-fem | (~uli-fem@115.128.71.34) |
| 2026-04-19 17:43:05 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2026-04-19 17:41:44 +0000 | bitdex_ | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2026-04-19 17:41:38 +0000 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 2026-04-19 17:39:44 +0000 | Square2 | (~Square@user/square) Square |
| 2026-04-19 17:38:46 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-19 17:34:50 +0000 | misterfish | (~misterfis@84.53.85.146) (Ping timeout: 256 seconds) |
| 2026-04-19 17:30:35 +0000 | troojg | (~troojg@user/troojg) (Ping timeout: 252 seconds) |