Unlifted data types

[Richard Eisenberg]

On Sep 11, 2015, at 4:28 AM, Roman Cheplyaka <roma at ro-che.info> wrote:

> On 11/09/15 06:22, Carter Schonwald wrote:
>> Would this allow having a strict monoid instance for maybe, given the
>> right hinting at the use site?
> 
> That's a fantastic idea, especially if it could be generalized to
> Applicative functors, where the problem of "inner laziness" is pervasive.
> 
> But that'd be tricky, because functions have the Lifted kind, and so
> <*> would have to be crazily levity-polymorphic. (Or is this not crazy?)

No more crazy than other things. Right now, we have

(<*>) :: forall (a :: *) (b :: *) (f :: * -> *). Applicative f => f (a -> b) -> f a -> f b

Under this proposal, we would have (ignore the Boxity stuff)

(<*>) :: forall (v1 :: Levity) (v2 :: Levity) (v3 :: Levity)
                (a :: TYPE v1) (b :: TYPE v2) (f :: forall (v4 :: Levity). TYPE v4 -> TYPE v3).
         Applicative f
      => f @'Lifted (a -> b) -> f @v1 a -> f @v2 b

The higher-rank levity-polymorphism is necessary in case `a` and `b` have different levities. This may be getting wildly out-of-hand, but I don't think it's actually breaking.

I would like to point out that using forall here is really quite wrong. As others have pointed out, levity polymorphism is ad-hoc polymorphism, not parametric. Using 'pi' would be much closer to it, but it implies the existence of more dependent types than we really need for this.

Richard

> 
> Roman
> 
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs