[Haskell-cafe] SystemF, universal quantification, and rigid type variables

[Ruud Koot]

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 <kumoyuki at gmail.com> wrote:
> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe