Re: [Haskell-cafe] Predicativity?

2008-09-16 Thread Thomas Davie
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

Re: [Haskell-cafe] Predicativity?

2008-09-16 Thread 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

Re: [Haskell-cafe] Predicativity?

2008-09-16 Thread 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 under

[Haskell-cafe] Predicativity?

2008-09-16 Thread Wei Hu
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 prob