Newest at the top
| 2026-04-22 20:27:56 +0000 | slomp | (~slomp@47-158-199-90.lsan.ca.frontiernet.net) |
| 2026-04-22 20:27:26 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-22 20:23:05 +0000 | Googulator | (~Googulato@84-236-65-56.pool.digikabel.hu) |
| 2026-04-22 20:22:47 +0000 | Googulator | (~Googulato@84-236-65-56.pool.digikabel.hu) (Quit: Client closed) |
| 2026-04-22 20:20:16 +0000 | slomp | (~slomp@47-158-199-90.lsan.ca.frontiernet.net) (Ping timeout: 244 seconds) |
| 2026-04-22 20:16:54 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 2026-04-22 20:14:09 +0000 | jmcantrell_ | (~weechat@user/jmcantrell) jmcantrell |
| 2026-04-22 20:11:39 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-22 20:10:43 +0000 | ouilemur | (~jgmerritt@user/ouilemur) (Quit: WeeChat 4.9.0) |
| 2026-04-22 20:09:42 +0000 | lewisbrown | (~user@user/lewisbrown) (ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.2)) |
| 2026-04-22 20:01:14 +0000 | Lord_of_Life_ | Lord_of_Life |
| 2026-04-22 20:00:59 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-04-22 19:58:42 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 248 seconds) |
| 2026-04-22 19:58:24 +0000 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-04-22 19:55:57 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-22 19:44:43 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-04-22 19:44:13 +0000 | Square2 | (~Square@user/square) (Ping timeout: 268 seconds) |
| 2026-04-22 19:37:50 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-22 19:32:42 +0000 | lewisbrown | (~user@user/lewisbrown) lewisbrown |
| 2026-04-22 19:32:42 +0000 | lewisbrown | (~user@15.218.2.231) (Changing host) |
| 2026-04-22 19:27:13 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2026-04-22 19:22:13 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-22 19:03:52 +0000 | vgtw | (~vgtw@user/vgtw) (Quit: ZNC - https://znc.in) |
| 2026-04-22 19:03:03 +0000 | lewisbrown | (~user@15.218.2.231) |
| 2026-04-22 18:52:53 +0000 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-04-22 18:52:53 +0000 | arandombit | (~arandombi@2a02:2455:8656:7100:a809:4899:76b6:a7ce) (Changing host) |
| 2026-04-22 18:52:53 +0000 | arandombit | (~arandombi@2a02:2455:8656:7100:a809:4899:76b6:a7ce) |
| 2026-04-22 18:43:47 +0000 | kupi | (uid212005@id-212005.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 2026-04-22 18:41:25 +0000 | <monochrom> | Personally I just fight bottom mistakes with test cases. This is more powerful in Haskell than in many other languages. Due to parametricity, if a sufficiently polymorphic function terminates for one test, then it terminates for a large generality. |
| 2026-04-22 18:38:44 +0000 | <gentauro> | must try again I guess |
| 2026-04-22 18:38:38 +0000 | <gentauro> | I tried to use it, couldn't make it build (nightly though) |
| 2026-04-22 18:36:32 +0000 | <monochrom> | But I have a feeling that Liquid Haskell is even less widely used than Lean. |
| 2026-04-22 18:36:03 +0000 | <monochrom> | I guess yes. |
| 2026-04-22 18:35:39 +0000 | <gentauro> | monochrom: can you ban `bottom` with Liquid Haskell comments? |
| 2026-04-22 18:34:34 +0000 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2026-04-22 18:30:03 +0000 | ski | . o O ( "Higher-Order Recursion Abstraction: How to Make Ackermann, Knuth and Conway Look Like a Bunch of Primitives, Figuratively Speaking" by Baltasar Trancón y Widemann in 2018-09-17 at <https://arxiv.org/abs/1602.05010> ) |
| 2026-04-22 18:29:24 +0000 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2026-04-22 18:25:09 +0000 | Digit | (~user@user/digit) (Ping timeout: 244 seconds) |
| 2026-04-22 18:20:46 +0000 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2026-04-22 18:02:35 +0000 | <monochrom> | (When I took a compiler course and submitted its toy compiler project) |
| 2026-04-22 18:01:22 +0000 | <monochrom> | When I took a compiler course, I submitted as a test case the Ackermann function! (The prof gave bonus marks for supporting recursion.) |
| 2026-04-22 17:56:07 +0000 | ft | (~ft@p508db287.dip0.t-ipconnect.de) ft |
| 2026-04-22 17:54:23 +0000 | <monochrom> | Yeah my thesis supervisor is like "termination is uninformative" because of that. |
| 2026-04-22 17:53:51 +0000 | <int-e> | monochrom: if it can implement the Ackermann function, is it really terminating ;) |
| 2026-04-22 17:52:49 +0000 | <monochrom> | (unless the talker actually advocates going all out for those two) |
| 2026-04-22 17:52:06 +0000 | <monochrom> | For now, IMO banning bottoms is just a lot of high-horse unpragmatic talk. |
| 2026-04-22 17:51:32 +0000 | <monochrom> | To be sure, I would be happy if someone found a third way much more ergonomic than those two. |
| 2026-04-22 17:50:50 +0000 | <monochrom> | (Belated) If one wants to ban bottoms, the only two currently widely deployed ways are System F (eg Dhall) and dependent type theory (eg Agda, Lean). |
| 2026-04-22 17:50:25 +0000 | ec | (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 2026-04-22 17:44:17 +0000 | rabbull | (~rabbull@user/rabbull) rabbull |