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