Newest at the top
| 2025-12-01 01:59:16 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-01 01:58:04 +0100 | <haskellbridge> | <zoil> like, the stateful constraints make sense, but the length constraint is just garbage |
| 2025-12-01 01:57:50 +0100 | <haskellbridge> | <zoil> id rather just be able to read off constraints that arent insane |
| 2025-12-01 01:57:15 +0100 | <haskellbridge> | <zoil> https://kf8nh.com/_heisenbridge/media/matrix.org/hTIHFOzGuFAqswyfkLuIVoBL/yfXyRcmB1_8/image.png |
| 2025-12-01 01:56:49 +0100 | <glguy> | and a mess of complicated error messages and special utility functions to manage it all |
| 2025-12-01 01:56:37 +0100 | <haskellbridge> | <zoil> basically, anything that requires more than one instance, like some kind of recusion matching on the tail or something, and then im in constraints hell |
| 2025-12-01 01:56:28 +0100 | <glguy> | this route leads to brittle programs that are hard to update and refactor |
| 2025-12-01 01:56:07 +0100 | <haskellbridge> | <zoil> id rather do it right at the onset, than have these constraints following me around |
| 2025-12-01 01:55:51 +0100 | <haskellbridge> | <zoil> possible* |
| 2025-12-01 01:55:46 +0100 | <haskellbridge> | <zoil> but, iiuc your saying its theoretically possivle |
| 2025-12-01 01:55:43 +0100 | <glguy> | yeah, it's better to just not overcomplicate your program |
| 2025-12-01 01:55:33 +0100 | <haskellbridge> | <zoil> i mean, this is all super interesting, and i think it might even work, but im hardly going to be able to do it |
| 2025-12-01 01:54:48 +0100 | glguy | ponders if that's exactly right, but anyway, the way to get type information from a value is using a GADT |
| 2025-12-01 01:54:47 +0100 | <haskellbridge> | <zoil> thats what learys answer looks like its managing to acheive |
| 2025-12-01 01:53:41 +0100 | <glguy> | singletons are |
| 2025-12-01 01:53:19 +0100 | <glguy> | proxies are not for runtime type information |
| 2025-12-01 01:53:07 +0100 | <glguy> | read doesn't have a place to put the runtime type witness, it's type is fixed by the type class definition |
| 2025-12-01 01:53:03 +0100 | <haskellbridge> | <zoil> i dont see why it would erase type information from a proxy, thats all they are for! crazy compiler |
| 2025-12-01 01:52:35 +0100 | <haskellbridge> | <zoil> glguy: I could do that! i just dont want constraints all over the place from recusrive classes that cant be asserted to be exhaustive |
| 2025-12-01 01:52:21 +0100 | <glguy> | It's not that it's fussy; it's just that it if the information has been erased, you can't use it |
| 2025-12-01 01:52:08 +0100 | <Leary> | zoil: You would need e.g. `data WhichNE xs where { IsCons :: WhichNE (Cons x xs); IsLast :: WhichNE (Last x) }; class KnownNE ne where { knownNE :: WhichNE ne }; <both instances>; instance KnownNE xs => Read (Transfers xs) where { read s = case knownNE of { ... } }`. |
| 2025-12-01 01:52:00 +0100 | <haskellbridge> | <zoil> that sounds like the kind of thing the compiler is fussy about |
| 2025-12-01 01:51:56 +0100 | <glguy> | You'd have to make a new GADTs so that at runtime you can learn which type is needed via case |
| 2025-12-01 01:51:47 +0100 | <haskellbridge> | <zoil> no type information at runtime! oh no! |
| 2025-12-01 01:51:29 +0100 | <haskellbridge> | <zoil> or does it just work the way id like it too! :_D |
| 2025-12-01 01:51:27 +0100 | <glguy> | You couldn't but that won't help if it's as simple as a Data.Proxy.Proxy (which contains no type information at runtime) |
| 2025-12-01 01:51:18 +0100 | <haskellbridge> | <zoil> because of the type family? |
| 2025-12-01 01:51:12 +0100 | <haskellbridge> | <zoil> btw, does your show instance pick up the requirement for the constraint to be specified each time, like if it was recursive in different classes? |
| 2025-12-01 01:50:33 +0100 | <haskellbridge> | <zoil> well i could provide a proxy... |
| 2025-12-01 01:49:54 +0100 | <glguy> | the argument to show is a value that's going to exist at runtime |
| 2025-12-01 01:49:26 +0100 | <haskellbridge> | <zoil> * @(HList (Cons |
| 2025-12-01 01:49:16 +0100 | <glguy> | That that's not usable information in the implementation of read itself on this type |
| 2025-12-01 01:48:57 +0100 | <haskellbridge> | <zoil> read @(Cons Int (Last Bool)) |
| 2025-12-01 01:48:48 +0100 | <glguy> | No, that's not enough |
| 2025-12-01 01:48:32 +0100 | <haskellbridge> | <zoil> but i can supply a type application? |
| 2025-12-01 01:48:25 +0100 | <glguy> | the argument to show witnesses what type show is being instantiated at |
| 2025-12-01 01:48:15 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-01 01:48:06 +0100 | <glguy> | One has a https://en.wikipedia.org/wiki/Witness_(mathematics) |
| 2025-12-01 01:47:58 +0100 | <haskellbridge> | <zoil> forgive me, i dont imidiately see the difference |
| 2025-12-01 01:47:34 +0100 | <glguy> | right |
| 2025-12-01 01:47:23 +0100 | <haskellbridge> | <zoil> and your saying thats not possible for the readd instance? |
| 2025-12-01 01:47:15 +0100 | <haskellbridge> | <zoil> thats cool |
| 2025-12-01 01:47:14 +0100 | <haskellbridge> | <zoil> so you just put a type family for the constraint |
| 2025-12-01 01:47:07 +0100 | <haskellbridge> | <zoil> oh wow! thats awesome, i never thought thats what you meant when you said it could go in one instance |
| 2025-12-01 01:46:11 +0100 | <glguy> | zoil: merging Show would be like: https://paste.tomsmeding.com/UEfrQUiN |
| 2025-12-01 01:45:44 +0100 | <Leary> | There is a kind-of workaround for `Read`-like cases by taking a singleton as a constraint and matching on it, but then you have to supply that singleton constraint everywhere instead. |
| 2025-12-01 01:44:53 +0100 | <haskellbridge> | <zoil> thanks! i thought it would be a known issue |
| 2025-12-01 01:44:08 +0100 | <Leary> | zoil: This kind of exhaustiveness doesn't exist at the type level in GHC for the same reason we don't have "eta-rules" <https://gitlab.haskell.org/ghc/ghc/-/issues/7259>; it isn't sound. You want to say that `xs :: NonEmpty _` implies `xs ~ Cons _ _` or `Last _`, but that isn't true until you successfully pattern match on `Transfers xs`. |
| 2025-12-01 01:43:46 +0100 | <haskellbridge> | <zoil> but it just looks underneath and still demands the underlying constraint |
| 2025-12-01 01:43:42 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
