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
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
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
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
