[Haskell-cafe] SystemF, universal quantification, and rigid type variables
nickolay.kudasov at gmail.com
Fri Mar 7 10:37:20 UTC 2014
There certainly is a difference between those types. Let's reveal their
- 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
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
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.
2014-03-07 14:05 GMT+04:00 David Rush <kumoyuki at gmail.com>:
> In short, I'm trying to decide if there is a real difference between the
> (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
> 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
> In the expression:
> ((\ u (x :: forall a. a) y -> u x y) (\ x y -> y)) True
> Since this is a 'rigid type variable' complaint, I am inclined to think
> this is a limitation of ghc, rather than a particular issue with the logic
> 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 at haskell.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe