Take the humble identity function in Haskell,
id :: forall a. a -> a
Given that Haskell supposedly supports impredicative polymorphism, it seems reasonable that I should be able to "restrict" id
to the type (forall a. a -> a) -> (forall b. b -> b)
via type ascription. But this doesn't work:
Prelude> id :: (forall a. a -> a) -> (forall b. b -> b)
<interactive>:1:1:
Couldn't match expected type `b -> b'
with actual type `forall a. a -> a'
Expected type: (forall a. a -> a) -> b -> b
Actual type: (forall a. a -> a) -> forall a. a -> a
In the expression: id :: (forall a. a -> a) -> (forall b. b -> b)
In an equation for `it':
it = id :: (forall a. a -> a) -> (forall b. b -> b)
It's of course possible to define a new, restricted form of the identity function with the desired signature:
restrictedId :: (forall a. a -> a) -> (forall b. b -> b)
restrictedId x = x
However defining it in terms of the general id
doesn't work:
restrictedId :: (forall a. a -> a) -> (forall b. b -> b)
restrictedId = id -- Similar error to above
So what's going on here? It seems like it might be related to difficulties with impredicativity, but enabling -XImpredicativeTypes
makes no difference.
I'm not an expert on impredictive types, so this is at once a potential answer and a try at learning something from comments.
It doesn't make sense to specialize
to
and I don't think impredictive types are a reason to allow it. The quantifiers have the effect of making the types represented by the left and right side of (2) inequivalent sets in general. Yet the
a -> a
in (1) implies left and right side are equivalent sets.E.g. you can concretize (2) to (int -> int) -> (string -> string). But by any system I know this is not a type represented by (1).
The error message looks like it results from an attempt by the Haskel type inferencer to unify the type of
id
with the type you've given
Here I'm uniqifying quantified variables for clarity.
The job of the type inferencer is to find a most general assignment for
a
,c
, andd
that causes the two expressions to be syntactically equal. It ultimately finds that it's required to unifyc
andd
. Since they're separately quantified, it's at a dead end and quits.You are perhaps asking the question because the basic type inferencer -- with an ascription
(c -> c) -> (d -> d)
-- would just plow ahead and setc == d
. The resulting type would bewhich is just shorthand for
This is provably the least most general type (type theoretic least upper bound) expression for the type of
x = x
wherex
is constrained to be a function with the same domain and co-domain.The type of "restricedId" as given is in a real sense excessively general. While it can never lead to a runtime type error, there are many types described by the expression you've given it - like the aforementioned
(int -> int) -> (string -> string)
- that are impossible operationally even though your type would allow them.