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