# Predicativity?

5 messages
Open this post in threaded view
|

## Predicativity?

 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
Open this post in threaded view
|

## Re: Predicativity?

 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
Open this post in threaded view
|

## Re: 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 <[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