ryani.spam at gmail.com
Wed Sep 17 02:26:54 EDT 2008
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
On Tue, Sep 16, 2008 at 10:05 PM, Wei Hu <weihu at cs.virginia.edu> wrote:
> 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?
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe