Newest at the top
| 2026-04-23 19:31:23 +0000 | <Comstar> | is there a generalized proof on peano-like recursion? like you have your base case essentially f_0 and some recursive step that takes you from an f_n to an f_{n-1} |
| 2026-04-23 19:31:10 +0000 | <monochrom> | Data.List.group is my last excuse for using head for non-toys (e.g., map head . group). I'm actually happy that Data.List.NonEmpty has a modernized group that produces [NonEmpty a] so I don't have to use head. |
| 2026-04-23 19:27:17 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-23 19:27:08 +0000 | accountant | (~accountan@2600:1702:5b61:8b40:955:b655:442f:e301) |
| 2026-04-23 19:25:15 +0000 | <monochrom> | Did you see the ">:)"? >:) |
| 2026-04-23 19:24:49 +0000 | <haskellbridge> | <ijouw> Maybe don't put it in the first homework? |
| 2026-04-23 19:23:59 +0000 | <haskellbridge> | <ijouw> I had to for theorem proof (and make a valid termination argument). |
| 2026-04-23 19:22:53 +0000 | <monochrom> | Speaking of which, and crossovering the Dhall/System-F conversation yesterday or two days ago: If I teach Dhall, it will be "fun" to put Ackermann on homework. >:) |
| 2026-04-23 19:21:58 +0000 | <EvanR> | the world ended because we didn't do the ideology and make sure all functions are total |
| 2026-04-23 19:21:25 +0000 | <EvanR> | you crashed |
| 2026-04-23 19:21:19 +0000 | <EvanR> | that *is* bottom |
| 2026-04-23 19:21:17 +0000 | <dminuoso> | And personally I think it improves awareness of where your code is brittle |
| 2026-04-23 19:20:48 +0000 | Square3 | (~Square@user/square) (Ping timeout: 244 seconds) |
| 2026-04-23 19:20:22 +0000 | <dminuoso> | Since bottom does not come with stack traces... |
| 2026-04-23 19:20:17 +0000 | jmcantrell_ | jmcantrell |
| 2026-04-23 19:20:17 +0000 | jmcantrell_ | (~weechat@user/jmcantrell) jmcantrell |
| 2026-04-23 19:20:16 +0000 | <EvanR> | rather you don't have to do much more than mention them |
| 2026-04-23 19:20:15 +0000 | <dminuoso> | EvanR: An explicit pattern match allows/nudges you into conjuring up an `error`. It saves downstream users a lot of time when they can search for your error string |
| 2026-04-23 19:19:33 +0000 | <EvanR> | you also don't have to mention impossible cases, it's built in |
| 2026-04-23 19:19:19 +0000 | <EvanR> | you don't have to prove this every time since it's built in |
| 2026-04-23 19:19:10 +0000 | <EvanR> | monochrom, for simple algorithms, the termination is guaranteed by recursion on a smaller argument |
| 2026-04-23 19:18:50 +0000 | <monochrom> | For automating finding a proof, you will have to look into satisfiability modulo theories (SMT), e.g., Z3. |
| 2026-04-23 19:18:49 +0000 | <EvanR> | similar to safeFromJust |
| 2026-04-23 19:18:15 +0000 | <EvanR> | if for some reason you have a list that is definitely not empty (and we didn't / can't use NonEmpty to get there), then a pattern match leaves you with no good options |
| 2026-04-23 19:18:10 +0000 | <dminuoso> | Since you can snuff a `error "lib:foo - cannot be empty"` in there, which serves as a primitive assertion whose provenance a downstream user can easily figure out |
| 2026-04-23 19:17:44 +0000 | <EvanR> | that's not true in general no |
| 2026-04-23 19:17:29 +0000 | <EvanR> | they can both go wrong, and a novice might actually end up doing that |
| 2026-04-23 19:17:25 +0000 | <dminuoso> | Even if you make an assumption of non-emptiness, an explicit pattern match is going to be vastly better. |
| 2026-04-23 19:17:13 +0000 | <EvanR> | for the same reason that every use of general recursion is bad? |
| 2026-04-23 19:17:05 +0000 | asd | (~asd@2a02:587:4550:b400:874e:c79f:8e8f:2a67) |
| 2026-04-23 19:16:52 +0000 | <EvanR> | ... |
| 2026-04-23 19:16:47 +0000 | <dminuoso> | EvanR: Id argue that every use of head/tail is bad. *shrugs* |
| 2026-04-23 19:16:31 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-04-23 19:16:24 +0000 | <monochrom> | Oh they require you to write the proof. Then they sit back and say "no". |
| 2026-04-23 19:15:55 +0000 | peterbecich | (~Thunderbi@71.84.33.135) (Ping timeout: 264 seconds) |
| 2026-04-23 19:15:43 +0000 | <EvanR> | it's built into the language / logic |
| 2026-04-23 19:15:28 +0000 | <monochrom> | But Agda and Lean don't automate the proofs. |
| 2026-04-23 19:14:56 +0000 | <EvanR> | but if we were then you can scroll up to the suggestion to use another language (agda or lean theorem prover or something) |
| 2026-04-23 19:14:27 +0000 | <EvanR> | Comstar, yes this is neither here nor there because we're not talking about automation to prove haltingness |
| 2026-04-23 19:14:26 +0000 | <haskellbridge> | <ijouw> I doubt it is, but rather that you use it more often than manual recursion. |
| 2026-04-23 19:13:42 +0000 | <EvanR> | how is a bad use of head or tail harder to detect in a test vs non termination |
| 2026-04-23 19:10:46 +0000 | Alex_delenda_est | (~al_test@85.174.181.200) |
| 2026-04-23 19:10:10 +0000 | <dminuoso> | But it is usually very possible to decide for a specific program. |
| 2026-04-23 19:10:04 +0000 | <monochrom> | EvanR, the way (IMO) to reject ideologies is to ask about actual quantities of damage in practice. And if it turns out that two kinds of mistakes, even though logically equivalent, are far from being on par in actual damage, then that's entirely possible because mistakes are made by humans and humans are weird. |
| 2026-04-23 19:09:39 +0000 | <Comstar> | yeah true, I pulled a demorgans oopsie |
| 2026-04-23 19:09:38 +0000 | <dminuoso> | It is impossible to write an algorithm that will decide whether or not an arbitrary input program will terminate |
| 2026-04-23 19:09:17 +0000 | <dminuoso> | Comstar: Id rephase "whether *any* arbitrary computation sequence will terminate" |
| 2026-04-23 19:09:14 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-23 19:08:53 +0000 | <dminuoso> | Comstar: Only in the generalized form. |
| 2026-04-23 19:08:43 +0000 | Googulator72 | (~Googulato@78-131-16-66.pool.digikabel.hu) |