Re: [Haskell-cafe] Predicativity?

Here is another example that doesn't compile under current GHC directly:

f = (runST .)

ghci reports the type of f as (a1 -> forall s. ST s a) -> a1 -> a But (f return) doesn't typecheck, even though the type of return is

return :: forall a s. a -> ST s a

Oddly, this does typecheck if we eta-expand return: ghci> :t f (\x -> return x) f (\x -> return x) :: forall a1. a1 -> a1 Perhaps the typechecker doesn't realize that since s is not free on the lhs of the -> in return, that the two types are equivalent? -- ryan On Tue, Sep 16, 2008 at 11:26 PM, Ryan Ingram wrote:

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 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