Newest at the top
| 2026-06-23 23:21:28 +0000 | <EvanR> | so you might ask why do we want proofs to terminate and confuse some people |
| 2026-06-23 23:20:55 +0000 | <EvanR> | so a vast subset of general programming |
| 2026-06-23 23:20:48 +0000 | <EvanR> | also I think the whole total thing really came out of theorem proving where proofs take the form of definitely terminating computations |
| 2026-06-23 23:20:06 +0000 | Digitteknohippie | Digit |
| 2026-06-23 23:19:41 +0000 | <EvanR> | or map over finite structure |
| 2026-06-23 23:19:17 +0000 | <EvanR> | but it's surprising how much easier it is to mentally verify when you move from e.g. explicit for loops to foreach over a (finite) array |
| 2026-06-23 23:18:28 +0000 | <dolio> | Lots of Haskell tricks are fine, but not allowed in any straight forward way. |
| 2026-06-23 23:18:22 +0000 | <EvanR> | many algorithms are total but the compiler can't just look at it and verify |
| 2026-06-23 23:17:59 +0000 | <EvanR> | yes |
| 2026-06-23 23:17:49 +0000 | <dolio> | I think the real issue with demanding totality is usually that a lot of things that are total aren't easy to show total, especially for corecursion. |
| 2026-06-23 23:17:34 +0000 | <EvanR> | but if it was () -> IO () then sure |
| 2026-06-23 23:17:13 +0000 | <EvanR> | in my premise, it's not even a function in the math sense but a procedure |
| 2026-06-23 23:16:37 +0000 | xff0x | (~xff0x@2405:6580:b080:900:9353:b8c8:c41e:444d) |
| 2026-06-23 23:16:22 +0000 | <dolio> | Why isn't it total? |
| 2026-06-23 23:16:06 +0000 | <EvanR> | in game engines you sometimes have 1 special function that implements an infinite loop, it's not total, and isn't even a pure function so you wouldn't test for that |
| 2026-06-23 23:15:31 +0000 | xff0x | (~xff0x@2405:6580:b080:900:e63a:b024:3b2a:a5eb) (Quit: xff0x) |
| 2026-06-23 23:15:21 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2026-06-23 23:15:12 +0000 | <EvanR> | but if you're in a module where you know all the functions are total then that's a thing you can test |
| 2026-06-23 23:15:06 +0000 | <jreicher> | Cool. We're on the same page. I can see where you're coming from. |
| 2026-06-23 23:14:49 +0000 | <EvanR> | of course not. In fact there are use cases for functions that mess up, like when doing LUB racing between threads |
| 2026-06-23 23:14:38 +0000 | <jreicher> | You want to know your function is correct. The fact that correctness implies totality is somewhat incidental, and won't be the case for other functions. |
| 2026-06-23 23:14:21 +0000 | peterbecich | (~Thunderbi@71.84.33.135) peterbecich |
| 2026-06-23 23:14:11 +0000 | <EvanR> | but I would find it useful to do the "easier" (hard) thing |
| 2026-06-23 23:14:04 +0000 | <jreicher> | So we aren't interested in totality for its own sake. |
| 2026-06-23 23:13:57 +0000 | <jreicher> | Exactly |
| 2026-06-23 23:13:51 +0000 | <EvanR> | compiler checking the actual requirements would be even harder |
| 2026-06-23 23:13:37 +0000 | <jreicher> | Now we're talking. So in the absence of being able to check the "more complete" properties of the function, you check totality. |
| 2026-06-23 23:13:36 +0000 | Digitteknohippie | (~user@user/digit) Digit |
| 2026-06-23 23:13:16 +0000 | marinelli | (~weechat@gateway/tor-sasl/marinelli) marinelli |
| 2026-06-23 23:13:00 +0000 | <EvanR> | it's a side effect of the requirements |
| 2026-06-23 23:12:50 +0000 | Digit | (~user@user/digit) (Ping timeout: 244 seconds) |
| 2026-06-23 23:12:40 +0000 | <jreicher> | Why is this the definition/requirement of that function? |
| 2026-06-23 23:12:38 +0000 | pounce | (8a023a9e4a@user/cute/pounce) pounce |
| 2026-06-23 23:12:31 +0000 | <jreicher> | Why? |
| 2026-06-23 23:12:24 +0000 | <EvanR> | for any shape you give it, it gaves some answer (also a specific answer, but that's another story) |
| 2026-06-23 23:12:21 +0000 | <jreicher> | I'm not saying you're wrong, I just want to understand why |
| 2026-06-23 23:12:12 +0000 | <jreicher> | Why? |
| 2026-06-23 23:12:07 +0000 | <EvanR> | I'm telling you it's supposed to be total |
| 2026-06-23 23:12:04 +0000 | <jreicher> | Why did you want it to be total in the first place? |
| 2026-06-23 23:11:56 +0000 | marinelli | (~weechat@gateway/tor-sasl/marinelli) (Ping timeout: 245 seconds) |
| 2026-06-23 23:11:48 +0000 | <jreicher> | What is "wrong" with a partial function? |
| 2026-06-23 23:11:48 +0000 | pounce | (8a023a9e4a@user/cute/pounce) (Ping timeout: 244 seconds) |
| 2026-06-23 23:11:43 +0000 | <EvanR> | if the compiler "merely" told me it wasn't total, I would have saved myself a lot of work |
| 2026-06-23 23:11:28 +0000 | <jreicher> | Why is it "supposed" to be total? Where is this "supposed" come from? God? |
| 2026-06-23 23:11:27 +0000 | <EvanR> | but when you pass in a certain polygon to it, it crashes badly |
| 2026-06-23 23:11:13 +0000 | <EvanR> | I have a function in C right now, like most functions, is supposed to be total |
| 2026-06-23 23:10:55 +0000 | apache2 | (apache2@anubis.0x90.dk) apache2 |
| 2026-06-23 23:10:44 +0000 | apache | (apache2@anubis.0x90.dk) (Remote host closed the connection) |
| 2026-06-23 23:10:26 +0000 | <EvanR> | but not bottom |
| 2026-06-23 23:10:24 +0000 | <jreicher> | OK. Why is that desirable? |