[Haskell] Rank-N types with (.) composition

[Dan Doel]

Impredicativity, with regard to type theories, generally refers to types
being able to quantify over the collection of types that they are then a
part of. So, the judgment:

    (forall (a :: *). a -> a) :: *

is impredicative, because we have a type in * that quantifies over all
types in *, which includes itself. Impredicativity in general refers to
this sort of (mildly) self-referential definition.

GHC will tell you that the above judgment is true, but things aren't that
simple. The type inference algorithm can either try to make use of such
impredicative instantiations, or act like everything is predicative. And
aspects of GHC's algorithm are either simplified or made possible at all
because of assumptions of predicativity.

Also, I think ($) is the way it is specifically because 'runST $ ...' is
considered useful and common enough to warrant an ad-hoc solution. There
have been other ad-hoc solutions in the past, but redesigning inference to
not be ad-hoc about it would be very difficult at best.

-- Dan

On Tue, Feb 10, 2015 at 3:51 PM, David Feuer <david.feuer at gmail.com> wrote:

> The problem is that GHC's type system is (almost entirely)
> predicative. I couldn't tell you just what that means, but to a first
> approximation, it means that type variables cannot be instantiated to
> polymorphic types. You write
>
> trip = Wrap . extract
>
>
> which means
>
> (.) Wrap extract
>
> (.)::(b->c)->(a->b)->a->c
>
> Wrap :: (forall f. Functor f => f Int) -> Wrap
>
> The trouble here is that the type variable b in the type of (.) isn't
> allowed to be polymorphic, but Wrap's argument must be.
>
> Note that there's a weird exception: ($) actually has an impredicative
> type, because it's a special case in the type checker. This is largely
> for historical reasons.
>
> On Tue, Feb 10, 2015 at 3:38 PM, Tyson Whitehead <twhitehead at gmail.com>
> wrote:
> > I came across something that seems a bit strange to me.  Here is a
> simplified version (the original was trying to move from a lens ReifiedFold
> to a lens-action ReifiedMonadicFold)
> >
> >  {-# LANGUAGE RankNTypes #-}
> >
> >  import Control.Applicative
> >
> >  newtype Wrap = Wrap { extract :: forall f. Functor f => f Int }
> >
> >  trip :: Wrap -> Wrap
> >  trip a = Wrap (extract a)
> >
> > The compiler is okay with this.  It chokes on this alternative though
> >
> >  trip :: Wrap -> Wrap
> >  trip = Wrap . extract
> >
> > giving (GHC 7.8.2)
> >
> >  Couldn't match type ‘f0 Int’
> >                with ‘forall (f :: * -> *). Functor f => f Int’
> >  Expected type: f0 Int -> Wrap
> >    Actual type: (forall (f :: * -> *). Functor f => f Int) -> Wrap
> >  In the first argument of ‘(.)’, namely ‘Wrap’
> >  In the expression: Wrap . extract
> >
> > I'm guessing this is because the compiler fancy footwork to handle the
> implicit parameters, something like
> >
> >  trip a = Wrap (\f fDict -> extract a f fDict)
> >
> > where f is the Functor type and fDict is the associated dictionary,
> isn't compatible with the (.) definition of
> >
> >  f . g = \x -> f (g x)
> >
> > Is this correct?  I would appreciate anyone insight here.  Is there a
> way combine these (.) style?
> >
> > Thanks!  -Tyson
> > _______________________________________________
> > Haskell mailing list
> > Haskell at haskell.org
> > http://www.haskell.org/mailman/listinfo/haskell
> _______________________________________________
> Haskell mailing list
> Haskell at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell/attachments/20150210/0e1bc687/attachment.html>