weihu at cs.virginia.edu
Wed Sep 17 01:05:58 EDT 2008
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?
More information about the Haskell-Cafe