[Haskell-cafe] SystemF, universal quantification, and rigid type variables
Ruud Koot
r.koot at uu.nl
Fri Mar 7 10:35:05 UTC 2014
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
More information about the Haskell-Cafe
mailing list