Obtaining restricted functions in Haskell as arguments

I played 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 ab -- This should return (String, String) 

myFunc must be completely polymorphic in the show signature so that it can accept a and b with different types satisfying the show .

Here is my attempt with the GHC extensions RankNTypes , ConstraintKinds , KindSignatures :

 myFunc :: forall (k :: * -> Constraint) ab d. (ka, kb) => (forall c. kc => c -> d) -> a -> b -> (d, d) 

My main goal is to understand how these extensions work; but for my eyes it seems that I am telling the GHC that there is a k restriction that some a and b satisfy, as well as a function (forall c. kc => c -> d) that can take any type c satisfying k and return concrete d , now, in these conditions, I want to apply the function to a and b to get a tuple (d,d)

Here's how the GHC complains:

 Could not deduce (k0 a, k0 b) from the context (ka, kb) bound by the type signature for myFunc :: (ka, kb) => (forall c. kc => 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) ab d. (ka, kb) => (forall c. kc => 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) ab d. (ka, kb) => (forall c. kc => c -> d) -> a -> b -> (d, d) ... Could not deduce (kc) from the context (ka, kb) bound by the type signature for myFunc :: (ka, kb) => (forall c. kc => 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) ab d. (ka, kb) => (forall c. kc => 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) ab d. (ka, kb) => (forall c. kc => c -> d) -> a -> b -> (d, d) app/Main.hs15:40 

What am I missing?

+5
source share
1 answer

The problem is that simply passing the function (forall c . kc => c -> d) as an argument is not enough for type checking to unambiguously determine that k is actually. Passing a constraint explicitly works, and you don't even need external forall or explicit types:

 import Data.Proxy myFunc :: (ka, kb) => Proxy k -> (forall c. kc => c -> d) -> a -> b -> (d, d) myFunc _ fab = (fa, fb) 

and then

 let (c, d) = myFunc (Proxy :: Proxy Show) show ab 
+5
source

All Articles