[Haskell-cafe] Moving "forall" over type constructors
derek.a.elkins at gmail.com
Tue Jun 10 23:28:25 EDT 2008
On Tue, 2008-06-10 at 11:28 -0700, Ryan Ingram wrote:
> 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...
Actually some support was hacked into the current version of GHC.
More information about the Haskell-Cafe