[Haskell-cafe] Moving "forall" over type constructors

Ryan Ingram ryani.spam at gmail.com
Tue Jun 10 14:28:34 EDT 2008

On 6/10/08, Derek Elkins <derek.a.elkins at gmail.com> wrote:
> This is the lack of impredicativity.
> W :: a -> W a
> To get the result type W (forall a. t a), W must instantiate the a in
> W's type to (forall a. t a).  Further we then pass it to (.) which has
> type (b -> c) -> (a -> b) -> a -> c and thus require instantiating both
> a and b to higher-rank types.  A predicative type system does not allow
> instantiating type variables to quantified types.

Although if I am reading the literature correctly, that definition
will likely typecheck in the next GHC...


  -- ryan

More information about the Haskell-Cafe mailing list