Logs: liberachat/#haskell
| 2026-04-23 19:00:48 | <EvanR> | meanwhile recursive algorithms could easily bottom if the poor user doesn't know how to prove it doesn't |
| 2026-04-23 19:01:07 | <EvanR> | not a great reason to remove recursion |
| 2026-04-23 19:01:44 | <Comstar> | kind of a halting problem in abstract, no? |
| 2026-04-23 19:02:13 | <monochrom> | Is there hard data on how much damage head and tail have done in the real world? |
| 2026-04-23 19:02:23 | → | layline_ joins (~layline@149.154.26.56) |
| 2026-04-23 19:02:39 | <EvanR> | or how much damage recursion has done xD |
| 2026-04-23 19:03:06 | <EvanR> | e.g. a js script controlling a machine crashes after too much recursion |
| 2026-04-23 19:03:19 | <Comstar> | bun has tail recursion now, no? |
| 2026-04-23 19:03:50 | <EvanR> | (or freezes up) |
| 2026-04-23 19:04:00 | <dminuoso> | EvanR: In my experience, algorithms that never terminate caused 0% of upstream library bugs. |
| 2026-04-23 19:04:16 | <dminuoso> | Partial code however... |
| 2026-04-23 19:04:27 | <haskellbridge> | <ijouw> I think having 'headMaybe :: [a] -> Maybe a' and similar in Prelude is good. If you hide head and tail behind an import, a small but easily overcome hurdle could make you re-think whether you actually want partial head and tail. |
| 2026-04-23 19:04:39 | <EvanR> | your statement doesn't convince me of anything |
| 2026-04-23 19:04:55 | <EvanR> | they're both partial, and infinite loops are much harder to debug |
| 2026-04-23 19:04:57 | <monochrom> | poor user doesn't know how to prove <--- you know what, great reason to remove unproved code altogether! I'm all for it! But I'm clearly biased, formal methods is my favourite research area... |
| 2026-04-23 19:05:04 | <dminuoso> | EvanR: They just never occur in practice in libraries. |
| 2026-04-23 19:05:17 | <EvanR> | why not? |
| 2026-04-23 19:05:30 | <dminuoso> | That is a good question *shrugs* |
| 2026-04-23 19:05:42 | <EvanR> | whatever they did to avoid non termination |
| 2026-04-23 19:05:49 | <EvanR> | do that for bad usage of head and tail |
| 2026-04-23 19:05:56 | <monochrom> | @quote monochrom safeFromJust |
| 2026-04-23 19:05:56 | <lambdabot> | monochrom says: I use safeFromJust :: Maybe a -> Maybe a |
| 2026-04-23 19:06:17 | <monochrom> | "now you have two problems" >:) |
| 2026-04-23 19:06:47 | <dminuoso> | EvanR: Id say that non-termination is something that rather creeps up during development but will be caught by simple tests - but it seems really rare to have infinite recursion happen in edge cases. |
| 2026-04-23 19:08:26 | <Comstar> | theorem-wise whether or not a program terminates is an incompleteness thing right? like you can know if specific things will terminate, but not whether all abstract computation sequences will terminate? |
| 2026-04-23 19:08:28 | × | Googulator72 quits (~Googulato@78-131-16-66.pool.digikabel.hu) (Quit: Client closed) |
| 2026-04-23 19:08:43 | → | Googulator72 joins (~Googulato@78-131-16-66.pool.digikabel.hu) |
| 2026-04-23 19:08:53 | <dminuoso> | Comstar: Only in the generalized form. |
| 2026-04-23 19:09:14 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-23 19:09:17 | <dminuoso> | Comstar: Id rephase "whether *any* arbitrary computation sequence will terminate" |
| 2026-04-23 19:09:38 | <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:39 | <Comstar> | yeah true, I pulled a demorgans oopsie |
| 2026-04-23 19:10:04 | <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:10:10 | <dminuoso> | But it is usually very possible to decide for a specific program. |
| 2026-04-23 19:10:46 | → | Alex_delenda_est joins (~al_test@85.174.181.200) |
| 2026-04-23 19:13:42 | <EvanR> | how is a bad use of head or tail harder to detect in a test vs non termination |
| 2026-04-23 19:14:26 | <haskellbridge> | <ijouw> I doubt it is, but rather that you use it more often than manual recursion. |
| 2026-04-23 19:14:27 | <EvanR> | Comstar, yes this is neither here nor there because we're not talking about automation to prove haltingness |
| 2026-04-23 19:14:56 | <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:15:28 | <monochrom> | But Agda and Lean don't automate the proofs. |
| 2026-04-23 19:15:43 | <EvanR> | it's built into the language / logic |
| 2026-04-23 19:15:55 | × | peterbecich quits (~Thunderbi@71.84.33.135) (Ping timeout: 264 seconds) |
| 2026-04-23 19:16:24 | <monochrom> | Oh they require you to write the proof. Then they sit back and say "no". |
| 2026-04-23 19:16:31 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-04-23 19:16:47 | <dminuoso> | EvanR: Id argue that every use of head/tail is bad. *shrugs* |
| 2026-04-23 19:16:52 | <EvanR> | ... |
| 2026-04-23 19:17:05 | → | asd joins (~asd@2a02:587:4550:b400:874e:c79f:8e8f:2a67) |
| 2026-04-23 19:17:13 | <EvanR> | for the same reason that every use of general recursion is bad? |
| 2026-04-23 19:17:25 | <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:29 | <EvanR> | they can both go wrong, and a novice might actually end up doing that |
| 2026-04-23 19:17:44 | <EvanR> | that's not true in general no |
| 2026-04-23 19:18:10 | <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:18:15 | <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:49 | <EvanR> | similar to safeFromJust |
| 2026-04-23 19:18:50 | <monochrom> | For automating finding a proof, you will have to look into satisfiability modulo theories (SMT), e.g., Z3. |
| 2026-04-23 19:19:10 | <EvanR> | monochrom, for simple algorithms, the termination is guaranteed by recursion on a smaller argument |
| 2026-04-23 19:19:19 | <EvanR> | you don't have to prove this every time since it's built in |
| 2026-04-23 19:19:33 | <EvanR> | you also don't have to mention impossible cases, it's built in |
| 2026-04-23 19:20:15 | <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:20:16 | <EvanR> | rather you don't have to do much more than mention them |
| 2026-04-23 19:20:17 | → | jmcantrell_ joins (~weechat@user/jmcantrell) |
| 2026-04-23 19:20:17 | jmcantrell_ | is now known as jmcantrell |
| 2026-04-23 19:20:22 | <dminuoso> | Since bottom does not come with stack traces... |
| 2026-04-23 19:20:48 | × | Square3 quits (~Square@user/square) (Ping timeout: 244 seconds) |
| 2026-04-23 19:21:17 | <dminuoso> | And personally I think it improves awareness of where your code is brittle |
| 2026-04-23 19:21:19 | <EvanR> | that *is* bottom |
| 2026-04-23 19:21:25 | <EvanR> | you crashed |
| 2026-04-23 19:21:58 | <EvanR> | the world ended because we didn't do the ideology and make sure all functions are total |
| 2026-04-23 19:22:53 | <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:23:59 | <haskellbridge> | <ijouw> I had to for theorem proof (and make a valid termination argument). |
| 2026-04-23 19:24:49 | <haskellbridge> | <ijouw> Maybe don't put it in the first homework? |
| 2026-04-23 19:25:15 | <monochrom> | Did you see the ">:)"? >:) |
| 2026-04-23 19:27:08 | → | accountant joins (~accountan@2600:1702:5b61:8b40:955:b655:442f:e301) |
| 2026-04-23 19:27:17 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-23 19:31:10 | <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:31:23 | <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:40 | <Comstar> | where n \in \mathbb{N} |
| 2026-04-23 19:31:59 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-04-23 19:32:25 | <monochrom> | Look for "catamorphism". What you have in mind may be catamorphisms for "data N = Z | S N". |
| 2026-04-23 19:33:39 | <Comstar> | yeah I could see that |
| 2026-04-23 19:34:54 | <monochrom> | List's foldr is catamorphisms for cons lists. |
| 2026-04-23 19:35:11 | <Comstar> | oh that's where I heard it before then |
| 2026-04-23 19:35:42 | <Comstar> | folds/foldable and stuff |
| 2026-04-23 19:36:10 | <monochrom> | More precisely, for each type T, [T]'s foldr is catamorphisms for [T]. Now let T=() for Peano naturals. :) |
| 2026-04-23 19:36:35 | <monochrom> | which brings me to... |
| 2026-04-23 19:37:34 | ← | layline_ parts (~layline@149.154.26.56) (Textual IRC Client: www.textualapp.com) |
| 2026-04-23 19:37:37 | <haskellbridge> | <ijouw> generalizing peano numbers: instance (Monoid a) => Num [a] |
| 2026-04-23 19:37:38 | <monochrom> | A math prof was teaching an intro number theory course. I heard from students that he began with monoids. I asked him why, he said "because I don't like the Peano axioms". |
| 2026-04-23 19:38:19 | <monochrom> | One hour later I realized "oh so you're going to define N as the free monoid on the singleton set". |
| 2026-04-23 19:40:27 | <Comstar> | no magmas? |
| 2026-04-23 19:43:04 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-23 19:48:19 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-04-23 19:52:40 | × | aniketd quits (32aa4844cd@2a03:6000:1812:100::dcb) (Ping timeout: 245 seconds) |
| 2026-04-23 19:52:40 | × | bheesham quits (3aa22d8375@2a03:6000:1812:100::e40) (Ping timeout: 245 seconds) |
| 2026-04-23 19:52:56 | × | alethkit quits (23bd17ddc6@sourcehut/user/alethkit) (Ping timeout: 244 seconds) |
| 2026-04-23 19:52:56 | × | jkoshy quits (99b9359beb@user/jkoshy) (Ping timeout: 244 seconds) |
| 2026-04-23 19:53:05 | × | smiesner quits (b0cf5acf8c@user/smiesner) (Ping timeout: 245 seconds) |
| 2026-04-23 19:53:05 | × | caz quits (866183745f@2a03:6000:1812:100::15d4) (Ping timeout: 245 seconds) |
| 2026-04-23 19:53:05 | × | pmk quits (6afe4476a1@2a03:6000:1812:100::26d) (Ping timeout: 245 seconds) |
| 2026-04-23 19:53:05 | × | probie quits (cc0b34050a@user/probie) (Ping timeout: 245 seconds) |
All times are in UTC.