Hi David,

There certainly is a difference between those types. Let's reveal their full form:

forall b. (forall a. a) -> b
forall a b. a -> b

The first one takes a polymorphic value of type (forall a. a). This means we could instantiate it to be of any type (e.g. b).

The second one takes a value of any type (not the value of a polymorphic type).

Thus you cannot apply function with first type to True, because True has a concrete type Bool and is not polymorphic.

Consider another example:

forall b. Num b => (forall a. Num a => a) -> b
forall a b. (Num a, Num b) => a -> b

Here in first case function takes a polymorphic numeric value and returns another, you could define it to be f x = x + 1. But this function can only be applied to a polymorphic value (forall a. Num a => a). E.g. f (fromIntegral 2).

In second case you already have some numeric value and, unfortunately, you cannot use it: you have no way to convert Num types between each other.

Best regards,

Nick

2014-03-07 14:05 GMT+04:00 David Rush <kumoyuki@gmail.com>:

In short, I'm trying to decide if there is a real difference between the
types:

(forall a.a) -> b
a -> b

and frankly, I'm not seeing a difference. But ghc apparently does

*SystemF.Tests> :t ((\u (x::forall a. a) y -> u x y) (\x y -> y)) True

<interactive>:1:49:
Couldn't match type `a' with `Bool'
`a' is a rigid type variable bound by
a type expected by the context: a at <interactive>:1:1
In the second argument of `\ u (x :: forall a. a) y
-> u x y', namely
`True'
In the expression:
((\ u (x :: forall a. a) y -> u x y) (\ x y -> y)) True
*SystemF.Tests>

Since this is a 'rigid type variable' complaint, I am inclined to think that
this is a limitation of ghc, rather than a particular issue with the logic of
System F. I'd actually love to be wrong. Is there an actual difference
between the types?

- david rush

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe