[Haskell-cafe] Predicativity?

[Ryan Ingram]

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 <ryani.spam at gmail.com> 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 <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
>>
>