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 |
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 |
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 |
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 |
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 |
Free forum by Nabble | Edit this page |