Predicativity?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

Predicativity?

Wei Hu-6
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]> 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]> 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 <[hidden email]> 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
>> [hidden email]
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Predicativity?

Thomas Davie
In reply to this post by Wei Hu-6

On 17 Sep 2008, at 07:05, 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?

In your application (id id) you create two instances of id, each of  
which has type forall a. a -> a, and each of which can be applied to a  
different type.  In this case, the left one gets applied to the type  
(a -> a) and the right one a, giving them types (a -> a) -> (a -> a)  
and (a -> a) respectively.

What will not type check on the other hand is:

main = g id

g h = h h 4

which needs something along the lines of rank-2 polymorphism.

Bob
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Predicativity?

Wei Hu-6
Thomas Davie <tom.davie <at> gmail.com> writes:

> In your application (id id) you create two instances of id, each of  
> which has type forall a. a -> a, and each of which can be applied to a  
> different type.  In this case, the left one gets applied to the type  
> (a -> a) and the right one a, giving them types (a -> a) -> (a -> a)  
> and (a -> a) respectively.

Ah, I didn't realize it's because I created two instances of id, but it became
clear immediately after you pointed this out. Thank you, Ryan and Thomas, for
clarifying my confusion.

Wei




_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe