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 <[EMAIL PROTECTED]> 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? > > Thanks! > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
