[Haskell-cafe] Predicativity?

[Ryan Ingram]

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 <weihu at cs.virginia.edu> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>