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? -- ryan On Tue, Sep 16, 2008 at 11:26 PM, Ryan Ingram <[EMAIL PROTECTED]> 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 <[EMAIL PROTECTED]> 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 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? >> >> Thanks! >> >> _______________________________________________ >> Haskell-Cafe mailing list >> [email protected] >> http://www.haskell.org/mailman/listinfo/haskell-cafe >> > _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
