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

[Dan Doel]

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 at 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell/attachments/20150210/82bb107e/attachment.html>