Logs: liberachat/#haskell
| 2025-12-03 03:08:28 | × | mesaoptimizer quits (~user@user/PapuaHardyNet) (Remote host closed the connection) |
| 2025-12-03 03:12:08 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-03 03:20:27 | <geekosaur> | theoretically you only get that when initially applying formatting |
| 2025-12-03 03:21:20 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 240 seconds) |
| 2025-12-03 03:23:04 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-12-03 03:23:16 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 2025-12-03 03:25:54 | <EvanR> | with a properly designed algorithm? |
| 2025-12-03 03:26:07 | <EvanR> | is there a no collateral damage theorem |
| 2025-12-03 03:28:42 | × | td_ quits (~td@i53870902.versanet.de) (Ping timeout: 252 seconds) |
| 2025-12-03 03:29:35 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-03 03:30:20 | → | td_ joins (~td@i5387093E.versanet.de) |
| 2025-12-03 03:31:59 | × | peterbecich quits (~Thunderbi@172.222.148.214) (Ping timeout: 250 seconds) |
| 2025-12-03 03:35:28 | × | humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2025-12-03 03:37:28 | → | inline__ joins (~wbooze@cgn-195-14-219-152.nc.de) |
| 2025-12-03 03:40:30 | × | wbooze quits (~wbooze@2001-4dd7-9813-0-4568-5322-9334-ddaa.ipv6dyn.netcologne.de) (Ping timeout: 244 seconds) |
| 2025-12-03 03:41:06 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-12-03 03:45:40 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-12-03 03:56:50 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-12-03 04:01:34 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2025-12-03 04:07:56 | oppili- | is now known as oppili |
| 2025-12-03 04:07:56 | × | oppili quits (~oppili@lewi-27-b2-v4wan-165682-cust505.vm4.cable.virginm.net) (Changing host) |
| 2025-12-03 04:07:56 | → | oppili joins (~oppili@user/nerdypepper) |
| 2025-12-03 04:11:58 | → | Square joins (~Square@user/square) |
| 2025-12-03 04:12:37 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-12-03 04:13:54 | → | peterbecich joins (~Thunderbi@172.222.148.214) |
| 2025-12-03 04:15:53 | → | Googulator45 joins (~Googulato@2a01-036d-0106-479c-d9ec-010d-f188-ffcb.pool6.digikabel.hu) |
| 2025-12-03 04:15:53 | × | Googulator88 quits (~Googulato@85-238-68-117.pool.digikabel.hu) (Quit: Client closed) |
| 2025-12-03 04:16:09 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Remote host closed the connection) |
| 2025-12-03 04:17:49 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-12-03 04:18:09 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 2025-12-03 04:28:26 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-12-03 04:32:55 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-03 04:44:13 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-12-03 04:48:31 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-03 04:50:01 | <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 04:52:12 | <haskellbridge> | <zoil> Leary |
| 2025-12-03 04:52:13 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/meQNVtzNxaPzTuQoVMpGePld/Wmc2FsApiyo (7 lines) |
| 2025-12-03 04:52:42 | <haskellbridge> | <zoil> i didnt read the bit where it was "and then you get these new constraints instead" |
| 2025-12-03 04:52:45 | <haskellbridge> | <zoil> ... |
| 2025-12-03 04:52:56 | <haskellbridge> | <zoil> _thats the whole point_ |
| 2025-12-03 04:53:26 | <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 04:53:36 | <haskellbridge> | <zoil> it was, whats up with having to carry around these constraints |
| 2025-12-03 04:54:00 | <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 04:54:16 | <haskellbridge> | <zoil> if i have to tell it that Bool has an Eq instance, then its fine |
| 2025-12-03 04:54:35 | <haskellbridge> | <zoil> but if its, that the head and tail of a hetroginous container both have a recursive instance |
| 2025-12-03 04:54:39 | <EvanR> | a type level trust me |
| 2025-12-03 04:54:43 | <EvanR> | sounds dangerous |
| 2025-12-03 04:54:57 | <haskellbridge> | <zoil> but we have exhaustiveness elsewhere |
| 2025-12-03 04:55:03 | <haskellbridge> | <zoil> maybe not that the user can specify it |
| 2025-12-03 04:55:20 | <haskellbridge> | <zoil> we have had this whole dependant types singletons debate for years |
| 2025-12-03 04:55:25 | <haskellbridge> | <zoil> isnt this the whole point!? |
| 2025-12-03 04:55:43 | <haskellbridge> | <zoil> these damn eta constraints or whatever they are |
| 2025-12-03 04:56:06 | <EvanR> | every time I disable the type system in e.g. C it usually results in a segfault xD |
| 2025-12-03 04:56:06 | <EvanR> | it's crazy |
| 2025-12-03 04:56:06 | <EvanR> | how good humans are at messing up logic |
| 2025-12-03 04:56:15 | <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 04:56:51 | <haskellbridge> | <zoil> EvanR: sure, i dont want some unknown way to break the compiler |
| 2025-12-03 04:56:57 | <haskellbridge> | <zoil> we wouldnt know how to give reasonable errors |
| 2025-12-03 04:57:07 | <haskellbridge> | <zoil> "you aserted something wrong!" |
| 2025-12-03 04:57:24 | <haskellbridge> | <zoil> but still. languages like lean have this whole business dedicated to assertion proving |
| 2025-12-03 04:57:44 | <EvanR> | does lean let you explicitly deal with or disable exhaustiveness |
| 2025-12-03 04:57:47 | <haskellbridge> | <zoil> its like. iv even had situations where i pick up a constraint like 1 + n ~ n + 1 |
| 2025-12-03 04:58:15 | <haskellbridge> | <zoil> EvanR: idk how lean works. i think its more like a hackage for assertions |
| 2025-12-03 04:58:23 | × | marinelli quits (~weechat@gateway/tor-sasl/marinelli) (Quit: marinelli) |
| 2025-12-03 04:58:40 | <haskellbridge> | <zoil> like, there is some transistivity axiom that allows you to prove something and it does everything like that in a rigerous derived way |
| 2025-12-03 04:58:57 | <glguy> | zoil: the thing you were asking about earlier wasn't about exhaustiveness, it's about not knowing what instance to use at runtime |
| 2025-12-03 04:59:20 | <haskellbridge> | <zoil> there was some confusion, which iiuc, is because it requires 2 instances |
| 2025-12-03 04:59:30 | <haskellbridge> | <zoil> iiuc thats a problem because its not exhaustive |
| 2025-12-03 04:59:43 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-12-03 05:00:14 | <EvanR> | exhaustive sounds like something to do with a closed world assumption. type classes are open world and can never be exhaustive |
| 2025-12-03 05:00:32 | <EvanR> | for all types there either is or not an instance |
| 2025-12-03 05:00:49 | <haskellbridge> | <zoil> its saying (f :: [Type] -> Constraint) (xs :: [Type]) instance does not exist. and im saying "but i gave you a f [], and a f (x:xs) case, foolish compiler" |
| 2025-12-03 05:00:49 | <EvanR> | (yet) |
| 2025-12-03 05:01:17 | <haskellbridge> | <zoil> its exhaustive in the sum GADT cases |
| 2025-12-03 05:01:21 | <haskellbridge> | <zoil> its not an open datatype |
| 2025-12-03 05:01:35 | <haskellbridge> | <zoil> if it was a data family i would agree |
| 2025-12-03 05:01:45 | <haskellbridge> | <zoil> but its not, so i have something that can be exhaustive |
| 2025-12-03 05:02:35 | <haskellbridge> | <zoil> it seems to be like "what!? more than one instance, im confused" |
| 2025-12-03 05:02:38 | <haskellbridge> | <zoil> which doesnt seem right at all!! |
| 2025-12-03 05:03:07 | <haskellbridge> | <zoil> its like "where is the xs case, i only see [] and (x:xs), this is not xs" |
| 2025-12-03 05:03:19 | × | peterbecich quits (~Thunderbi@172.222.148.214) (Ping timeout: 260 seconds) |
| 2025-12-03 05:03:26 | <haskellbridge> | <zoil> and the user is like "but it is!! its exhaustive!!" |
| 2025-12-03 05:04:07 | → | marinelli joins (~weechat@gateway/tor-sasl/marinelli) |
| 2025-12-03 05:04:26 | × | marinelli quits (~weechat@gateway/tor-sasl/marinelli) (Remote host closed the connection) |
| 2025-12-03 05:04:45 | → | marinelli joins (~weechat@gateway/tor-sasl/marinelli) |
| 2025-12-03 05:04:56 | <haskellbridge> | <zoil> then someone said, "so just put it in one instance, and like, match the cases by a type family" |
| 2025-12-03 05:05:19 | <haskellbridge> | <zoil> and then someone else said "but this needs a type witness, use singletons" |
| 2025-12-03 05:05:51 | <haskellbridge> | <zoil> and then there was this KnownNonempty thing where head and tail could be given value level case matching that would bring the type into scope |
| 2025-12-03 05:06:20 | <haskellbridge> | <zoil> and then i picked up this KnownNonempty constraint, and this still indicates the compiler is not happy that the assertion is satisfied |
| 2025-12-03 05:06:31 | <haskellbridge> | <zoil> it says. "no. idk this instance exists, put it in a constraint" |
| 2025-12-03 05:06:34 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-12-03 05:07:02 | <haskellbridge> | <zoil> because the instances for KnownNonempty have the same problem. idk if this can be solved by the same typefamily idea or something |
| 2025-12-03 05:07:11 | <haskellbridge> | <zoil> or if its that GHC is not advanced, or what |
| 2025-12-03 05:07:15 | <EvanR> | either you missed the simple way to do what you're doing, the only way to do it in haskell is so arcane that it's probably not worth it, or it's just impossible |
| 2025-12-03 05:07:16 | <haskellbridge> | <zoil> so i need some expert input |
| 2025-12-03 05:08:08 | <EvanR> | sophisticated stuff at the type level is just easily overcomplicated here |
| 2025-12-03 05:08:39 | <haskellbridge> | <zoil> iiuc the "singletons idea" requires these exhastive instances are provided. and these have to be done in one class, and there was another idea to use type families to do this, but im totally confused. |
| 2025-12-03 05:09:07 | <haskellbridge> | <zoil> i just want to be able to describe the situation so people can understand the issue and maybe help produce a working example |
| 2025-12-03 05:10:11 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-12-03 05:10:21 | <haskellbridge> | <zoil> i had this example to work with so far; https://play.haskell.org/saved/GwyPOlmo |
All times are in UTC.