Newest at the top
| 2025-02-12 00:56:31 +0100 | <dminuoso> | Oh well, I think I understand what the diagnostic is really trying to say |
| 2025-02-12 00:55:20 +0100 | <ski> | (assuming `data Showable = forall a. Show a => WrapShowable a', and `withShowable :: Showable -> (forall a. Show a => a -> o) -> o') |
| 2025-02-12 00:55:09 +0100 | <dminuoso> | But that has no associated forall either.. |
| 2025-02-12 00:54:51 +0100 | <yahb2> | <no output> |
| 2025-02-12 00:54:51 +0100 | <dminuoso> | % id :: a -> a; id @a x = (x :: a) |
| 2025-02-12 00:54:49 +0100 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 244 seconds) |
| 2025-02-12 00:54:37 +0100 | <dminuoso> | Invisible type pattern? |
| 2025-02-12 00:54:20 +0100 | <dminuoso> | Hold on. |
| 2025-02-12 00:54:13 +0100 | <ski> | withShowable (WrapShowable @a x) k = k @a x -- could one write something like this ? |
| 2025-02-12 00:54:13 +0100 | <yahb2> | <interactive>:263:4: error: [GHC-14964] ; • Invisible type pattern a has no associated forall ; • In an equation for ‘id’: id @a x = (x :: a) |
| 2025-02-12 00:54:13 +0100 | <dminuoso> | % id @a x = (x :: a) |
| 2025-02-12 00:54:02 +0100 | <yahb2> | <no output> |
| 2025-02-12 00:54:02 +0100 | <dminuoso> | % :set -XTypeAbstractions |
| 2025-02-12 00:53:02 +0100 | ski | doesn't think the selection of `@' is great |
| 2025-02-12 00:52:35 +0100 | <dminuoso> | I recall there was a proposal a while ago, but I cant quite remember the name of the extension |
| 2025-02-12 00:52:20 +0100 | <ski> | debatable |
| 2025-02-12 00:52:03 +0100 | <dminuoso> | Do we have a suitable syntax for type application, now? |
| 2025-02-12 00:51:33 +0100 | <ski> | perhaps there should be an explicit syntax for dictionary application ? |
| 2025-02-12 00:50:32 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-02-12 00:50:10 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 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> |