Newest at the top
| 2025-12-03 05:58:15 +0100 | <haskellbridge> | <zoil> EvanR: idk how lean works. i think its more like a hackage for assertions |
| 2025-12-03 05:57:47 +0100 | <haskellbridge> | <zoil> its like. iv even had situations where i pick up a constraint like 1 + n ~ n + 1 |
| 2025-12-03 05:57:44 +0100 | <EvanR> | does lean let you explicitly deal with or disable exhaustiveness |
| 2025-12-03 05:57:24 +0100 | <haskellbridge> | <zoil> but still. languages like lean have this whole business dedicated to assertion proving |
| 2025-12-03 05:57:07 +0100 | <haskellbridge> | <zoil> "you aserted something wrong!" |
| 2025-12-03 05:56:57 +0100 | <haskellbridge> | <zoil> we wouldnt know how to give reasonable errors |
| 2025-12-03 05:56:51 +0100 | <haskellbridge> | <zoil> EvanR: sure, i dont want some unknown way to break the compiler |
| 2025-12-03 05:56:15 +0100 | <haskellbridge> | <zoil> if its an exhaustiveness issue, thats at least an expression of the problem in a way, that, at least personally, i have never heard it phrased |
| 2025-12-03 05:56:06 +0100 | <EvanR> | how good humans are at messing up logic |
| 2025-12-03 05:56:06 +0100 | <EvanR> | it's crazy |
| 2025-12-03 05:56:06 +0100 | <EvanR> | every time I disable the type system in e.g. C it usually results in a segfault xD |
| 2025-12-03 05:55:43 +0100 | <haskellbridge> | <zoil> these damn eta constraints or whatever they are |
| 2025-12-03 05:55:25 +0100 | <haskellbridge> | <zoil> isnt this the whole point!? |
| 2025-12-03 05:55:20 +0100 | <haskellbridge> | <zoil> we have had this whole dependant types singletons debate for years |
| 2025-12-03 05:55:03 +0100 | <haskellbridge> | <zoil> maybe not that the user can specify it |
| 2025-12-03 05:54:57 +0100 | <haskellbridge> | <zoil> but we have exhaustiveness elsewhere |
| 2025-12-03 05:54:43 +0100 | <EvanR> | sounds dangerous |
| 2025-12-03 05:54:39 +0100 | <EvanR> | a type level trust me |
| 2025-12-03 05:54:35 +0100 | <haskellbridge> | <zoil> but if its, that the head and tail of a hetroginous container both have a recursive instance |
| 2025-12-03 05:54:16 +0100 | <haskellbridge> | <zoil> if i have to tell it that Bool has an Eq instance, then its fine |
| 2025-12-03 05:54:00 +0100 | <haskellbridge> | <zoil> why cant I _assert to the compiler_ that the exhaustiveness is something i have ensured I have taken care of |
| 2025-12-03 05:53:36 +0100 | <haskellbridge> | <zoil> it was, whats up with having to carry around these constraints |
| 2025-12-03 05:53:26 +0100 | <haskellbridge> | <zoil> it wasnt a question about "how do i refactor these dumb constraints so i can carry around a more effecient expression" |
| 2025-12-03 05:52:56 +0100 | <haskellbridge> | <zoil> _thats the whole point_ |
| 2025-12-03 05:52:45 +0100 | <haskellbridge> | <zoil> ... |
| 2025-12-03 05:52:42 +0100 | <haskellbridge> | <zoil> i didnt read the bit where it was "and then you get these new constraints instead" |
| 2025-12-03 05:52:13 +0100 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/meQNVtzNxaPzTuQoVMpGePld/Wmc2FsApiyo (7 lines) |
| 2025-12-03 05:52:12 +0100 | <haskellbridge> | <zoil> Leary |
| 2025-12-03 05:50:01 +0100 | <haskellbridge> | <zoil> i cant beleive i went to all the trouble of putting together an example just to discover the advice was corrupt |
| 2025-12-03 05:48:31 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-03 05:44:13 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-03 05:32:55 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-03 05:28:26 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-03 05:18:09 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-12-03 05:17:49 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-12-03 05:16:09 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Remote host closed the connection) |
| 2025-12-03 05:15:53 +0100 | Googulator88 | (~Googulato@85-238-68-117.pool.digikabel.hu) (Quit: Client closed) |
| 2025-12-03 05:15:53 +0100 | Googulator45 | (~Googulato@2a01-036d-0106-479c-d9ec-010d-f188-ffcb.pool6.digikabel.hu) |
| 2025-12-03 05:13:54 +0100 | peterbecich | (~Thunderbi@172.222.148.214) peterbecich |
| 2025-12-03 05:12:37 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-03 05:11:58 +0100 | Square | (~Square@user/square) Square |
| 2025-12-03 05:07:56 +0100 | oppili | (~oppili@user/nerdypepper) nerdy |
| 2025-12-03 05:07:56 +0100 | oppili | (~oppili@lewi-27-b2-v4wan-165682-cust505.vm4.cable.virginm.net) (Changing host) |
| 2025-12-03 05:07:56 +0100 | oppili- | oppili |
| 2025-12-03 05:01:34 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2025-12-03 04:56:50 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-03 04:45:40 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-12-03 04:41:06 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-03 04:40:30 +0100 | wbooze | (~wbooze@2001-4dd7-9813-0-4568-5322-9334-ddaa.ipv6dyn.netcologne.de) (Ping timeout: 244 seconds) |
| 2025-12-03 04:37:28 +0100 | inline__ | (~wbooze@cgn-195-14-219-152.nc.de) Inline |