On 17 Sep 2008, at 07:05, Wei Hu wrote:
Hello,
I only have a vague understanding of predicativity/impredicativity,
but cannot
map this concept to practice.
We know the type of id is forall a. a -> a. I thought id could not
be applied
to itself under predicative polymorphism. But Haksell and OCaml both
type check
(id id) with no problem. Is my understanding wrong? Can you show an
example
that doesn't type check under predicative polymorphism, but would
type check
under impredicative polymorphism?
In your application (id id) you create two instances of id, each of
which has type forall a. a -> a, and each of which can be applied to a
different type. In this case, the left one gets applied to the type
(a -> a) and the right one a, giving them types (a -> a) -> (a -> a)
and (a -> a) respectively.
What will not type check on the other hand is:
main = g id
g h = h h 4
which needs something along the lines of rank-2 polymorphism.
Bob
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
