Maybe this example is more enlightening?
-- doesn't compile -- f x = x x
-- does compile under GHC at least g :: (forall a. a -> a) -> (forall a. a -> a) g x = x x
h = g id
(although I don't know if it really answers your question) One big motivation for impredicativity, as I understand it, is typing things that use runST properly: -- runST :: (forall s. ST s a) -> a -- ($) :: forall a b. (a -> b) -> a -> b -- f $ x = f x
z = runST $ return "hello"
How do you typecheck z? From what I understand, it is quite difficult
without impredicativity.
-- ryan
On Tue, Sep 16, 2008 at 10:05 PM, Wei Hu
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?
Thanks!
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe