Newest at the top
| 2025-02-12 00:49:50 +0100 | <ski> | (s/eta reduction/function extensionality/) |
| 2025-02-12 00:49:39 +0100 | <yahb2> | () |
| 2025-02-12 00:49:38 +0100 | <geekosaur> | % let { withDict'' :: Dict a -> (a => r) -> r; withDict'' Dict = id } in () |
| 2025-02-12 00:49:17 +0100 | <yahb2> | <no output> |
| 2025-02-12 00:49:17 +0100 | <geekosaur> | % :set -XDeepSubsumption |
| 2025-02-12 00:47:05 +0100 | <mauke> | eta reduction: destroyed |
| 2025-02-12 00:47:03 +0100 | <dminuoso> | Okay I find the diagnostic a bit surprising here. |
| 2025-02-12 00:46:14 +0100 | <yahb2> | () |
| 2025-02-12 00:46:14 +0100 | <mauke> | % let { withDict' :: Dict a -> (a => r) -> r; withDict' Dict r = r } in () |
| 2025-02-12 00:46:08 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-12 00:46:03 +0100 | <yahb2> | <interactive>:237:62: error: [GHC-91028] ; • Couldn't match type ‘r’ with ‘a => r’ ; Expected: (a => r) -> r ; Actual: r -> r ; Cannot equate type variable ‘r’ ; with ... |
| 2025-02-12 00:46:02 +0100 | <mauke> | % let { withDict' :: Dict a -> (a => r) -> r; withDict' Dict = id } in () |
| 2025-02-12 00:45:33 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 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) |