It seems you've already figured this out, but here's a quick counterexample:
> {-# LANGUAGE ExistentialQuantification, RankNTypes #-}
> module Box where
> data Box = forall a. B a
>
> --mapBox :: forall a b. (a -> b) -> Box -> Box -- incorrect type
> mapBox f (B x) = B (f x)
then:
> boxedInt :: Box
> boxedInt = B (1 :: Int)
> f :: [Int] -> Int
> f = sum
mf :: Box -> Box
mapBox f -- this is well-typed according to the specified type of "mapBox"
But,
mf boxedInt :: Box
mf boxedInt
= mapBox f boxedInt
= mapBox sum (B (1 :: Int))
= B (sum (1 :: Int))
which is not well-typed.
The least specific type for MapBox is
> mapBox :: forall b. (forall a. (a -> b)) -> Box -> Box
There are non-bottom functions of this type, for example:
const (1 :: Int) :: forall a. a -> Int
With this type,
> ok :: Box
> ok = mapBox (const 1) (B "hello")
is well-typed.
-- ryan
A question about existential quantification:
Given the existential type:
data Box = forall a. B a
in other words:
-- data Box = B (exists a.a)
-- B :: (exists a.a) -> Box
I cannot type-check the function:
mapBox :: forall a b. (a -> b) -> Box -> Box
-- :: forall a b. (a -> b) -> (exists
a.a) -> (exists a.a)
mapBox f (B x) = B (f x)
Nor can I type check:
mapBox :: forall a. (a -> a) -> Box -> Box
-- :: forall a. (a -> a) -> (exists a.a) -> (exists a.a)
mapBox f (B x) = B (f x)
The compiler tells me that in both functions, when it encounters the
expression |B (f x)|, it cannot unify the universally quantified |a|
(which generates a rigid type var) with the existentially quatified
|a| (which generates a different rigid type var) -- or so I interpret
the error message.
However, at first sight |f| is polymorphic so it could be applied to
any value, included the value hidden in |Box|.
Of course, this works:
mapBox :: (forall a b. a -> b) -> Box -> Box
mapBox f (B x) = B (f x)
Because it's a tautology: given a proof of a -> b for any a or b I can
prove Box -> Box. However the only value of type forall a b. a -> b is
bottom.
This also type-checks:
mapBox :: (forall a. a -> a) -> Box -> Box
mapBox f (B x) = B (f x)
When trying to give an explanation about why one works and the other
doesn't, I see that, logically, we have:
forall a. P(a) => Q implies (forall a. P(a)) => Q when a does not
occur in Q.
The proof in our scenario is trivial:
p :: (forall a. (a -> a) -> (Box -> Box)) -> (forall a. a -> a) -> Box -> Box
p mapBox f b = mapBox f b
However, the converse is not true.
Yet, could somebody tell me the logical reason for the type-checking
error? In other words, how does the unification failure translate
logically. Should the first mapBox actually type-check?
Isn't the code for mapBox :: forall a. (a -> a) -> Box -> Box
encoding the proof:
Assume forall a. a -> a
Assume exists a.a
unpack the existential, x :: a = T for some T
apply f to x, we get (f x) :: a
pack into existential, B (f x) :: exists a.a
Discharge first assumption
Discharge second assumption
The error must be in step 3. Sorry if this is obvious, it's not to me right now.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe