Unlifted data types

[Edward Z. Yang]

I'm not so sure how useful an observation this is, but Dunfield
had a paper at this very ICFP "Elaborating Evaluation-Order
Polymorphism".  He argues that polymorphism over evaluation
order should be thought of as a form of intersection type.

Edward

Excerpts from Richard Eisenberg's message of 2015-09-14 08:59:36 -0700:
> 
> 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
>