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