I've been playing with some GHC extensions to define a function that can do the following:
let a = A :: A -- Show A
b = B :: B -- Show B
in
myFunc show a b -- This should return (String, String)
myFunc
should be fully polymorphic in the signature of show
, so that it can accept a
and b
with different types satisfying Show
.
Here's my attempt with the GHC extensions RankNTypes
, ConstraintKinds
, KindSignatures
:
myFunc :: forall (k :: * -> Constraint) a b d. (k a, k b)
=> (forall c. k c => c -> d) -> a -> b -> (d, d)
My main purpose is to understand how these extensions work; but to my eyes, it seems like I'm telling GHC that there's a constraint k
that some a
and b
satisfy, and there's also a function (forall c. k c => c -> d)
that can take any type c
satisfying k
and return a specific d
, now, under these conditions, I want to apply the function to a
and b
to obtain a tuple (d,d)
Here's how GHC complains:
Could not deduce (k0 a, k0 b)
from the context (k a, k b)
bound by the type signature for
myFunc :: (k a, k b) =>
(forall c. k c => c -> d) -> a -> b -> (d, d)
at app/Main.hs:(15,11)-(16,56)
In the ambiguity check for the type signature for ‘myFunc’:
myFunc :: forall (k :: * -> Constraint) a b d.
(k a, k b) =>
(forall c. k c => c -> d) -> a -> b -> (d, d)
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature for ‘myFunc’:
myFunc :: forall (k :: * -> Constraint) a b d. (k a, k b) =>
(forall c. k c => c -> d) -> a -> b -> (d, d)
...
Could not deduce (k c)
from the context (k a, k b)
bound by the type signature for
myFunc :: (k a, k b) =>
(forall c. k c => c -> d) -> a -> b -> (d, d)
at app/Main.hs:(15,11)-(16,56)
or from (k0 c)
bound by the type signature for myFunc :: k0 c => c -> d
at app/Main.hs:(15,11)-(16,56)
In the ambiguity check for the type signature for ‘myFunc’:
myFunc :: forall (k :: * -> Constraint) a b d.
(k a, k b) =>
(forall c. k c => c -> d) -> a -> b -> (d, d)
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature for ‘myFunc’:
myFunc :: forall (k :: * -> Constraint) a b d. (k a, k b) =>
(forall c. k c => c -> d) -> a -> b -> (d, d)
app/Main.hs15:40
What am I missing?
The problem is that just passing the function (forall c . k c => c -> d)
as an argument is not enough for the type-checker to unambiguously determine what k
really is. Passing the constraint explicitly works and you don't even need the outer forall
or explicit kinds:
import Data.Proxy
myFunc :: (k a, k b) => Proxy k -> (forall c. k c => c -> d) -> a -> b -> (d, d)
myFunc _ f a b = (f a, f b)
and then
let (c, d) = myFunc (Proxy :: Proxy Show) show a b
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With