I'm new to some of the more complicated type constructs in Haskell, and have been messing around. I'm currently stuck trying to get a function that I think should work to type check.
Take the following code as an example:
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
class X a where
data Y a
z :: Y a -> Int
data D1 = D1
instance X D1 where
data Y D1 = YD1
z _ = 1
data D2 = D2
instance X D2 where
data Y D2 = YD2
z _ = 2
sumZ :: X a => [Y a] -> Int
sumZ = foldl' sumFn 0
where sumFn = flip ((+) . z)
I want a = sumZ [YD1, YD2]
to type check. This (obviously) doesn't work since the a
type variable gets fixed with the first YD1
.
I understand enough to know that I should probably use higher ranked types here, so I tried this:
sumZ' :: [(forall a. X a => Y a)] -> Int
sumZ' = foldl' sumFn 0
where sumFn = flip ((+) . z)
But, when I try and compile it I run into "impredicative polymorphism":
• Illegal polymorphic type: forall a. X a => Y a
GHC doesn't yet support impredicative polymorphism
• In the type signature: sumZ' :: [(forall a. X a => Y a)] -> Int
|
48 | sumZ' :: [(forall a. X a => Y a)] -> Int
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
After doing a bit of reading, I see that the conventional solution is to wrap the value in a newtype
to skirt around the impredicative polymorphism.
newtype Wrap = Wrap { unWrap :: forall a. X a => Y a }
sumZ'' :: [Wrap] -> Int
sumZ'' = foldl' sumFn 0
where
sumFn acc (Wrap v) = acc + (z v)
Unfortunately, this doesn't seem to work either. Compilation fails with this message:
• Ambiguous type variable ‘a0’ arising from a use of ‘z’
prevents the constraint ‘(X a0)’ from being solved.
Probable fix: use a type annotation to specify what ‘a0’ should be.
These potential instances exist:
instance X D1
-- Defined at ...
instance X D2
-- Defined at ...
• In the second argument of ‘(+)’, namely ‘(z v)’
In the expression: acc + (z v)
In an equation for ‘sumFn’: sumFn acc (Wrap v) = acc + (z v)
|
64 | sumFn acc (Wrap v) = acc + (z v)
| ^^^
Finally, my question(s):
- Why doesn't the standard "wrapping" technique work in this case? When inspecting the type of
v
I see that it has the typeforall a. X a => Y a
, to me this seems like it should work. - How can I get the
a = sumZ [YD1, YD2]
to work? Am I going about this wrong?
The fact that
v :: forall a. X a => Y a
is exactly why applyingz
doesn't work.That
forall
in there means thatv
can be of any type, you choose which one. To illustrate, compare to this:There value
empty
can be of any type, the consumer chooses which type. That's whatforall
means here. I hope this much is obvious.And so it is with your value
v
: it can be of any type, you choose which. But in your code you don't choose a type: you're applyingz
, which itself can work with any type, and so the type ofv
remains unchosen. This is exactly what the compiler is telling you when it complains about the "ambiguous type variable a0".To make this work, you should put the
forall
on the other side ofWrap
:(you'll need to enable the
GADTs
extension for this to be allowed)This way, whoever constructs a
Wrap
has to choose the specific typea
. And on the other side, when you do pattern matching, you get the typea
that was chosen by whoever constructed the value.