Newest at the top
| 2025-03-12 21:18:03 +0100 | <EvanR> | I don't see why my DOOM implementation in haskell doesn't just run at compile time! This long time joke apparently has become real in typescript recently |
| 2025-03-12 21:17:44 +0100 | <tomsmeding> | I have never had to use something like that yet. :) |
| 2025-03-12 21:17:30 +0100 | tomsmeding | had to look up "solvable" |
| 2025-03-12 21:16:11 +0100 | <c_wraith> | ah, I see. |
| 2025-03-12 21:16:03 +0100 | <int-e> | So there's some theoretical interest in HNFs. |
| 2025-03-12 21:15:51 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 2025-03-12 21:15:51 +0100 | <int-e> | A pure lambda term is solvable iff it has a HNF. |
| 2025-03-12 21:15:41 +0100 | <c_wraith> | or even Integer, for the really bold |
| 2025-03-12 21:15:39 +0100 | <EvanR> | wouldn't that be nice |
| 2025-03-12 21:15:24 +0100 | <tomsmeding> | 'Just (1 + 2 :: Int)' then |
| 2025-03-12 21:15:20 +0100 | tomsmeding | grumbles |
| 2025-03-12 21:15:11 +0100 | <EvanR> | in haskell |
| 2025-03-12 21:15:06 +0100 | <EvanR> | though Just (1 + 2) in isolation can't be simplified |
| 2025-03-12 21:13:10 +0100 | <tomsmeding> | heh |
| 2025-03-12 21:13:06 +0100 | <c_wraith> | so textbooks include it |
| 2025-03-12 21:13:04 +0100 | <tomsmeding> | surely if I write 'Just (1 + 2)', a compiler should optimise that to Just 3? But as far as I understand, 'Just (1 + 2)' is in HNF |
| 2025-03-12 21:12:59 +0100 | <c_wraith> | I think it mostly makes for a really nice exercise to say "implement this optimization" |
| 2025-03-12 21:12:28 +0100 | <tomsmeding> | only the one at the left seems awfully arbitrary |
| 2025-03-12 21:12:21 +0100 | <c_wraith> | That's not quite the same, but the idea is related |
| 2025-03-12 21:12:18 +0100 | <tomsmeding> | c_wraith: but then why would it not reduce _all_ redexes? |
| 2025-03-12 21:11:55 +0100 | <c_wraith> | tomsmeding: HNF seems related to like... compiler optimizations. Find reducible expressions anywhere in the graph and reduce them at compile time, for instance. |
| 2025-03-12 21:11:30 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-03-12 21:09:32 +0100 | <tomsmeding> | EvanR: it makes sense if you consider a lambda to be the "constructor" of the (->) type |
| 2025-03-12 21:08:53 +0100 | <EvanR> | so lambda is WHNF, regardless of what's in it |
| 2025-03-12 21:08:43 +0100 | <tomsmeding> | I get WHNF and NF, but is HNF useful for anything? |
| 2025-03-12 21:07:55 +0100 | <c_wraith> | IIRC, that's the main difference from HNF |
| 2025-03-12 21:07:35 +0100 | a_fantom | (~fantom@2.219.56.221) (Ping timeout: 244 seconds) |
| 2025-03-12 21:07:35 +0100 | <c_wraith> | whnf doesn't reduce under a lambda, though, so (\_ -> 1 + 2) is in WHNF |
| 2025-03-12 21:07:21 +0100 | pavonia | (~user@user/siracusa) siracusa |
| 2025-03-12 21:04:37 +0100 | infinity0 | (~infinity0@pwned.gg) infinity0 |
| 2025-03-12 21:00:00 +0100 | hiecaq | (~hiecaq@user/hiecaq) (ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.0.92)) |
| 2025-03-12 20:48:04 +0100 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-03-12 20:45:01 +0100 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-03-12 20:44:41 +0100 | <EvanR> | that's an application |
| 2025-03-12 20:44:34 +0100 | <EvanR> | WHNFs aren't applications |
| 2025-03-12 20:43:49 +0100 | infinity0 | (~infinity0@pwned.gg) (Ping timeout: 248 seconds) |
| 2025-03-12 20:39:32 +0100 | zungi | (~tory@user/andrewchawk) andrewchawk |
| 2025-03-12 20:37:49 +0100 | <Inst> | this is annoying, (+1) 2 isn't in WHNF, right? |
| 2025-03-12 20:29:27 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 246 seconds) |
| 2025-03-12 20:25:06 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-03-12 20:22:24 +0100 | zungi | (~tory@user/andrewchawk) (Ping timeout: 264 seconds) |
| 2025-03-12 20:20:30 +0100 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2025-03-12 20:20:23 +0100 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-03-12 20:16:26 +0100 | weary-traveler | (~user@user/user363627) (Ping timeout: 244 seconds) |
| 2025-03-12 20:16:09 +0100 | j1n37- | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-03-12 20:14:34 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-03-12 20:12:09 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-03-12 20:10:41 +0100 | notdabs | (~Owner@2600:1700:69cf:9000:91e8:307c:455b:5f65) (Read error: Connection reset by peer) |
| 2025-03-12 20:10:16 +0100 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
| 2025-03-12 20:04:14 +0100 | jespada | (~jespada@2800:a4:22b4:9a00:f994:da25:97cf:4452) jespada |