Unlifted data types
eir at cis.upenn.edu
Mon Sep 14 15:59:36 UTC 2015
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).
=> 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.
> ghc-devs mailing list
> ghc-devs at haskell.org
More information about the ghc-devs