Newest at the top
| 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) |
| 2026-04-23 19:08:28 +0000 | Googulator72 | (~Googulato@78-131-16-66.pool.digikabel.hu) (Quit: Client closed) |
| 2026-04-23 19:08:26 +0000 | <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:06:47 +0000 | <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:06:17 +0000 | <monochrom> | "now you have two problems" >:) |
| 2026-04-23 19:05:56 +0000 | <lambdabot> | monochrom says: I use safeFromJust :: Maybe a -> Maybe a |
| 2026-04-23 19:05:56 +0000 | <monochrom> | @quote monochrom safeFromJust |
| 2026-04-23 19:05:49 +0000 | <EvanR> | do that for bad usage of head and tail |
| 2026-04-23 19:05:42 +0000 | <EvanR> | whatever they did to avoid non termination |
| 2026-04-23 19:05:30 +0000 | <dminuoso> | That is a good question *shrugs* |
| 2026-04-23 19:05:17 +0000 | <EvanR> | why not? |
| 2026-04-23 19:05:04 +0000 | <dminuoso> | EvanR: They just never occur in practice in libraries. |
| 2026-04-23 19:04:57 +0000 | <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:04:55 +0000 | <EvanR> | they're both partial, and infinite loops are much harder to debug |
| 2026-04-23 19:04:39 +0000 | <EvanR> | your statement doesn't convince me of anything |
| 2026-04-23 19:04:27 +0000 | <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:16 +0000 | <dminuoso> | Partial code however... |
| 2026-04-23 19:04:00 +0000 | <dminuoso> | EvanR: In my experience, algorithms that never terminate caused 0% of upstream library bugs. |
| 2026-04-23 19:03:50 +0000 | <EvanR> | (or freezes up) |
| 2026-04-23 19:03:19 +0000 | <Comstar> | bun has tail recursion now, no? |
| 2026-04-23 19:03:06 +0000 | <EvanR> | e.g. a js script controlling a machine crashes after too much recursion |
| 2026-04-23 19:02:39 +0000 | <EvanR> | or how much damage recursion has done xD |
| 2026-04-23 19:02:23 +0000 | layline_ | (~layline@149.154.26.56) layline |
| 2026-04-23 19:02:13 +0000 | <monochrom> | Is there hard data on how much damage head and tail have done in the real world? |
| 2026-04-23 19:01:44 +0000 | <Comstar> | kind of a halting problem in abstract, no? |
| 2026-04-23 19:01:07 +0000 | <EvanR> | not a great reason to remove recursion |
| 2026-04-23 19:00:48 +0000 | <EvanR> | meanwhile recursive algorithms could easily bottom if the poor user doesn't know how to prove it doesn't |
| 2026-04-23 19:00:47 +0000 | ouilemur | (~jgmerritt@user/ouilemur) ouilemur |
| 2026-04-23 18:58:46 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-04-23 18:58:26 +0000 | <EvanR> | by deleting head and tail from prelude, you'd force reasonable people to rewrite their correct code for the sake of ideology |
| 2026-04-23 18:56:47 +0000 | peterbecich | (~Thunderbi@71.84.33.135) peterbecich |
| 2026-04-23 18:54:18 +0000 | <monochrom> | :) |
| 2026-04-23 18:54:01 +0000 | <dminuoso> | I've done it. |
| 2026-04-23 18:53:57 +0000 | <dminuoso> | geekosaur: Fun story, for aliasing mutable buffers unsafePerformIO is enough! |
| 2026-04-23 18:53:52 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-23 18:53:44 +0000 | <geekosaur> | which is why there's an ever-growing list of GHC "bug" reports associated with it |
| 2026-04-23 18:53:27 +0000 | <dminuoso> | Which reminds me, IEEE 754 exceptions should be a thing. |
| 2026-04-23 18:53:25 +0000 | <geekosaur> | but people keep ptrying to use it in `bytestring` without knowing what it really means |
| 2026-04-23 18:52:58 +0000 | <dminuoso> | geekosaur: Sure, which is why accursedUnutterablePerformIO is neither tought in beginner resources nor made available in Prelude. ;-) |