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@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@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@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell