ryani.spam at gmail.com
Wed Sep 17 02:34:05 EDT 2008
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?
On Tue, Sep 16, 2008 at 11:26 PM, Ryan Ingram <ryani.spam at gmail.com> 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 <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