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

Well, that might also be surprising, unless ($) is also magically made to work like a standard operator (just off the top of my head; there may be other confusing aspects). Really, I think the least ad-hoc solution (other than a hypothetical best-of-both-worlds inference algorithm) would be to allow code like: runST do ... where you can apply expressions directly to certain syntactic constructs without an operator in between. I suspect the majority of cases where 'runST $' is used are followed by a 'do,' and not having the remaining ones wouldn't be nearly as painful to use with parentheses (since they likely wouldn't be multi-line). And this extension is desirable for other reasons as well (though I can't recall any specifics off the top of my head). But I wouldn't hold your breath for that. On Tue, Feb 10, 2015 at 4:37 PM, David Feuer <david.feuer@gmail.com> wrote:

On Tue, Feb 10, 2015 at 4:28 PM, Dan Doel <dan.doel@gmail.com> wrote:

...

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

Of the ad-hoc solutions available, I'd personally think the least surprising would be to make f $ x special syntax instead of an operator. The main tricky bit would be preserving source for error messages; the type checker would have to keep track, for each application, of whether it was a standard juxtaposition or whether it used $.

On February 10, 2015 16:28:56 Dan Doel wrote:

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.

Thanks Dan and David, That was informative. Also very interesting that ($) is a special case. I tried this newtype Wrap = Wrap { extract :: forall f. Functor f => f Int } trip'' :: Wrap -> Wrap trip'' a = Wrap $ extract a and the compiler was happy. Wrapping ($) as ($') gave an error as you implied it would trip''' :: Wrap -> Wrap trip''' a = Wrap $' extract a where ($') = ($) With regard to my earlier comment about translating the (.) version trip' :: Wrap -> Wrap trip' = Wrap . extract to core, I can see it's actually okay. A most you may need is a lambda to float the implicit parameters backwards trip' :: Wrap -> Wrap trip' = Wrap . (\a f fDict -> extract f fDict a) as GHC seems to always float them as far leftward as possible extract :: Functor f => Wrap -> f Int I take it there are no user supplied types a person can give to overcome the predicative assumption? Out of curiosity, how would you write the special internal type that ($) has that separates it from ($') above? Thanks! -Tyson

There is no special type for ($). The name is simply special cased in the compiler. The rule is something like: Whenever you see: f Prelude.$ x instead try to type check: f x That may not be the exact behavior, but it's close. To fix (.) (in a similar fashion) you would have to have a similar rule, like: Whenever you see: f Prelude.. g instead try to type check: \x -> f (g x) -- Dan On Tue, Feb 10, 2015 at 6:19 PM, Tyson Whitehead <twhitehead@gmail.com> wrote:

On February 10, 2015 16:28:56 Dan Doel wrote:

...

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.

Thanks Dan and David,

That was informative. Also very interesting that ($) is a special case. I tried this

newtype Wrap = Wrap { extract :: forall f. Functor f => f Int }

trip'' :: Wrap -> Wrap trip'' a = Wrap $ extract a

and the compiler was happy. Wrapping ($) as ($') gave an error as you implied it would

trip''' :: Wrap -> Wrap trip''' a = Wrap $' extract a where ($') = ($)

With regard to my earlier comment about translating the (.) version

trip' :: Wrap -> Wrap trip' = Wrap . extract

to core, I can see it's actually okay. A most you may need is a lambda to float the implicit parameters backwards

trip' :: Wrap -> Wrap trip' = Wrap . (\a f fDict -> extract f fDict a)

as GHC seems to always float them as far leftward as possible

extract :: Functor f => Wrap -> f Int

I take it there are no user supplied types a person can give to overcome the predicative assumption?

Out of curiosity, how would you write the special internal type that ($) has that separates it from ($') above?

Thanks! -Tyson