SystemF, universal quantification, and rigid type variables
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
In a strict language (forall a.a) -> b and a -> b would be "the same"
in the sense that they are both uninhabited and thus isomorphic in a
trivial sense. However isomorphic types are generally not considered
identical by a programming language.
In a lazy language these types are inhabited, but by a different
number of terms and can thus not be isomorphic in the strict sense:
f : a -> b is only inhabited by "undefined" and "\x -> undefined"
f : (forall. a) ->b is also inhabited by \x -> x, although calling it
with any argument other than undefined will prove difficult.
Ruud
On Fri, Mar 7, 2014 at 11:05 AM, David Rush
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
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
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
So I posted:
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... I'd actually love to be wrong. Is there an actual difference between the types?
And Ruud Koot and Nikolay Kudasov both told me:
YES.
Thanks, y'all. That actually means I was doing it right :) - d
participants (3)
-
David Rush -
Nickolay Kudasov -
Ruud Koot