Newest at the top
| 2026-06-24 01:17:55 +0000 | <jreicher> | A type system that checked complexity would be really interesting. |
| 2026-06-24 01:17:43 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 01:13:02 +0000 | user363627 | (~user@user/user363627) user363627 |
| 2026-06-24 01:12:46 +0000 | user363627 | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2026-06-24 01:12:13 +0000 | <monochrom> | (It is not like you have a non-constructive proof of termination using the axiom of choice, is it? >:) ) |
| 2026-06-24 01:11:42 +0000 | <monochrom> | Almost every termination proof hides a time bound so it is counterproductive to throw the time bound away. |
| 2026-06-24 01:09:55 +0000 | ski | (~ski@90-224-14-130-no600.tbcn.telia.com) (Ping timeout: 264 seconds) |
| 2026-06-24 01:09:49 +0000 | <monochrom> | IMO totality is never going to be worthwhile because, for the same price, you should go for big-Theta complexity instead. I.e., don't bother proving termination; if anything, go straight for proving linear time or log time or whatever. Who cares about termination if it ends up being triple-expoenential time. |
| 2026-06-24 01:08:21 +0000 | <monochrom> | My answer to "why you accept static and strong typing but not totality, it sounds inconsistent" is that trade-offs and cost-vs-benefit considerations are consistent. Strong static typing gives me a lot of benefits with very little cost and/or inconvenience. Totality is a lot of cost for what it's worth. |
| 2026-06-24 01:06:56 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 271 seconds) |
| 2026-06-24 01:02:20 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 01:02:17 +0000 | prdak | (~Thunderbi@user/prdak) prdak |
| 2026-06-24 01:01:58 +0000 | prdak | (~Thunderbi@user/prdak) (Remote host closed the connection) |
| 2026-06-24 00:59:28 +0000 | acidjnk | (~acidjnk@p54ad50b4.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2026-06-24 00:58:58 +0000 | acidjnk_new | (~acidjnk@p200300d6e74def43ec2141b26299b177.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 2026-06-24 00:57:46 +0000 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2026-06-24 00:52:45 +0000 | xff0x | (~xff0x@2405:6580:b080:900:9353:b8c8:c41e:444d) (Ping timeout: 252 seconds) |
| 2026-06-24 00:51:19 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-06-24 00:44:17 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 00:33:05 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-24 00:28:56 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 00:19:23 +0000 | pavonia | (~user@user/siracusa) siracusa |
| 2026-06-24 00:17:56 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-06-24 00:14:15 +0000 | schuelermine | (~Thunderbi@user/schuelermine) schuelermine |
| 2026-06-24 00:13:33 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-24 00:02:49 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-06-23 23:58:10 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 23:47:32 +0000 | tromp | (~textual@2001:1c00:340e:2700:e1be:7d8f:de85:da97) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-06-23 23:47:27 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-06-23 23:42:48 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 23:41:07 +0000 | <dolio> | That is the 'productive' part of totality. |
| 2026-06-23 23:40:38 +0000 | <dolio> | Like, 'non-termination' is fine if your witness of the infinitude of primes is a stream of distinct prime numbers, as long as there's no point in the stream where it goes, "hold on a second," and then never comes back. |
| 2026-06-23 23:38:54 +0000 | <EvanR> | a term which can be used at any type |
| 2026-06-23 23:38:39 +0000 | <dolio> | That was my point. |
| 2026-06-23 23:38:32 +0000 | <dolio> | Not really non-termination, I guess, depending on what you mean. |
| 2026-06-23 23:37:16 +0000 | <dolio> | Non-termination allows vacuous proofs of false things, usually. |
| 2026-06-23 23:37:04 +0000 | <EvanR> | something on top of that would need to identify that you're talking about a turing machine |
| 2026-06-23 23:36:37 +0000 | <EvanR> | base haskell being not particularly expressive as a logic, you basically proved some stream exists |
| 2026-06-23 23:36:23 +0000 | <jreicher> | And how does that relate to termination? |
| 2026-06-23 23:35:58 +0000 | <dolio> | The type is what is being proved. |
| 2026-06-23 23:35:35 +0000 | <jreicher> | dolio: the analogy is not straightforward. You still have to be clear what is being proven by the program you are taking as a proof |
| 2026-06-23 23:35:01 +0000 | <dolio> | The connection is that proofs are analogous to Haskell programs, but saying that the text of a Haskell program is finite doesn't really tell you whether it stops or not, and some Haskell programs are not 'supposed' to stop, depending on what you mean by that. |
| 2026-06-23 23:33:52 +0000 | czan | (~czan@user/mange) czan |
| 2026-06-23 23:33:51 +0000 | <EvanR> | presumably, for this case |
| 2026-06-23 23:33:26 +0000 | <EvanR> | each WHNF step terminates |
| 2026-06-23 23:32:18 +0000 | <EvanR> | yeah the proof would be the program in this case, not the semantics value (the infinite stream) |
| 2026-06-23 23:31:02 +0000 | <jreicher> | How does that relate to what we're talking about? |
| 2026-06-23 23:30:59 +0000 | <dolio> | The ones that don't finish in pathological ways, too. |
| 2026-06-23 23:30:27 +0000 | <dolio> | All Haskell programs are finite, including the ones that don't finish. |
| 2026-06-23 23:30:24 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |