Newest at the top
| 2025-02-12 00:44:47 +0100 | <dminuoso> | This machinery lives on not just ConstraintKinds but also GADTs. |
| 2025-02-12 00:44:13 +0100 | <ski> | that's the point, yes |
| 2025-02-12 00:43:50 +0100 | <dminuoso> | mauke: ^- you must pattern match for the GADT packed dict to discharge the surrounding constraint. |
| 2025-02-12 00:43:31 +0100 | <yahb2> | <no output> |
| 2025-02-12 00:43:31 +0100 | <dminuoso> | % withDict :: Dict a -> (a => r) -> r; withDict d r = case d of Dict -> r |
| 2025-02-12 00:42:18 +0100 | <yahb2> | <interactive>:231:54: error: [GHC-39999] ; • No instance for ‘Show a’ arising from a use of ‘show’ ; Possible fix: ; add (Show a) to the context of ; the type signature ... |
| 2025-02-12 00:42:18 +0100 | <mauke> | % let { foo :: Dict (Show a) -> a -> String; foo _ x = show x } in foo Dict '?' |
| 2025-02-12 00:42:01 +0100 | <yahb2> | "'?'" |
| 2025-02-12 00:42:01 +0100 | <mauke> | % let { foo :: Dict (Show a) -> a -> String; foo Dict x = show x } in foo Dict '?' |
| 2025-02-12 00:41:17 +0100 | <dminuoso> | I tried really hard to find a reason to use `constraints` in one of our projects.. but no matter the mental gymnastics, I couldn't even justify it to myself. |
| 2025-02-12 00:40:16 +0100 | <dminuoso> | Finally, liberated. |
| 2025-02-12 00:40:08 +0100 | <dminuoso> | And we can use them to discharge constraints at will, no longer are we at the whim of the compiler. |
| 2025-02-12 00:39:42 +0100 | <dminuoso> | Not quite the constraints, but dictionaries of them. |
| 2025-02-12 00:39:12 +0100 | <dminuoso> | Some portion of these constraints can exist at the value level too! |
| 2025-02-12 00:38:55 +0100 | <yahb2> | <no output> |
| 2025-02-12 00:38:55 +0100 | <dminuoso> | % d = Dict :: Dict (Show Int) |
| 2025-02-12 00:38:48 +0100 | <yahb2> | <no output> |
| 2025-02-12 00:38:48 +0100 | <dminuoso> | % data Dict :: Constraint -> Type where Dict :: a => Dict a |
| 2025-02-12 00:38:48 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |
| 2025-02-12 00:37:35 +0100 | <mauke> | had to look up GADT record syntax |
| 2025-02-12 00:37:21 +0100 | <mauke> | newtype Identity runIdentity where Identity :: { runIdentity :: a } -> Identity a |
| 2025-02-12 00:37:06 +0100 | mange | (~user@user/mange) mange |
| 2025-02-12 00:35:42 +0100 | <ski> | basically, "constraints live at the same level as types" |
| 2025-02-12 00:35:25 +0100 | <dminuoso> | Especially in effect systems like effectful. |
| 2025-02-12 00:35:19 +0100 | <euouae> | right |
| 2025-02-12 00:35:12 +0100 | <dminuoso> | euouae: This can be useful for situations where you may have a bunch of constraints that you want to repeatedly mention in type signatures. |
| 2025-02-12 00:35:08 +0100 | <ski> | it's a compound constraint, consisting of two part constraints |
| 2025-02-12 00:34:46 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-12 00:34:44 +0100 | <euouae> | so an intersection of Show and Num |
| 2025-02-12 00:34:27 +0100 | <euouae> | oh it's a type constraint synonym that page says |
| 2025-02-12 00:34:23 +0100 | tabaqui1 | (~root@87.200.129.102) (Ping timeout: 252 seconds) |
| 2025-02-12 00:34:10 +0100 | <yahb2> | "\"43\"" |
| 2025-02-12 00:34:09 +0100 | <ski> | % let foo :: Wtf a => a -> String; foo n = show (show (n + 1)) in foo 42 |
| 2025-02-12 00:33:31 +0100 | <yahb2> | <no output> |
| 2025-02-12 00:33:31 +0100 | <dminuoso> | % f :: Wtf a => a -> a; f = id |
| 2025-02-12 00:32:45 +0100 | <yahb2> | <no output> |
| 2025-02-12 00:32:45 +0100 | <dminuoso> | % type Wtf a = (Show a, Num a) |
| 2025-02-12 00:32:43 +0100 | <yahb2> | <interactive>:183:29: error: [GHC-76037] ; Not in scope: type variable ‘b’ |
| 2025-02-12 00:32:43 +0100 | <dminuoso> | % type Wtf a = (Show a, Num a)b |
| 2025-02-12 00:32:37 +0100 | <dminuoso> | I think they were referring to `type Wtf ...` |
| 2025-02-12 00:32:15 +0100 | <mauke> | euouae: https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/constraint_kind.html |
| 2025-02-12 00:31:39 +0100 | <dminuoso> | However... |
| 2025-02-12 00:31:23 +0100 | <dminuoso> | euouae: `type ..` introduces just a type alias. |
| 2025-02-12 00:31:02 +0100 | <jackdk> | I had some code a while back that went hard on the stuff from package `constraints` to wrangle various `KnownNat` constraints. And then I fixed my design error and it all went away. But it was fun while it lasted. |
| 2025-02-12 00:30:58 +0100 | <euouae> | mauke: I guess it's a restriction on what a can be? is that an extension? |
| 2025-02-12 00:30:55 +0100 | <ski> | heh |
| 2025-02-12 00:30:33 +0100 | <mauke> | newtype Identity runIdentity where Identity::a -> Identity a |
| 2025-02-12 00:30:11 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-12 00:29:41 +0100 | <dminuoso> | Oh I was a bit too quick with that assessment indeed. |
| 2025-02-12 00:29:20 +0100 | <ski> | `Dict (Show T)' |