Unlifted data types

[Edward Kmett]

I think ultimately the two views of levity that we've been talking diverge
along the same lines as the pi vs forall discussion from your Levity
polymorphism talk.

I've been focused entirely on situations where forall suffices, and no
distinction is needed in how you compile for both levities.

Maybe could be polymorphic using a mere forall in the levity of the boxed
argument it carries as it doesn't care what it is, it never forces it,
pattern matching on it just gives it back when you pattern match on it.

Eq or Ord could just as easily work over anything boxed. The particular Eq
_instance_ needs to care about the levity.

Most of the combinators for working with Maybe do need to care about that
levity however.

e.g. consider fmap in Functor, the particular instances would care. Because
you ultimately wind up using fmap to build 'f a' values and those need to
know how the let binding should work. There seems to be a pi at work there.
Correct operational behavior would depend on the levity.

But if we look at what inference should probably grab for the levity of
Functor:

you'd get:

class Functor (l : Levity) (l' : Levity') (f :: GC l -> GC l') where
   fmap :: forall a b. (a :: GC l) (b :: GC l). (a -> b) -> f a -> f b

Baed on the notion that given current practices, f would cause us to pick a
common kind for a and b, and the results of 'f'. Depending on how and if we
decided to default to * unless annotated in various situations would drive
this closer and closer to the existing Functor by default.

These are indeed distinct functors with distinct operational behavior, and
we could implement each of them by supplying separate instances, as the
levity would take part in the instance resolution like any other kind
argument.

Whether we could expect an average Haskeller to be willing to do so is an
entirely different matter.

-Edward


On Wed, Sep 9, 2015 at 12:44 PM, Dan Doel <dan.doel at gmail.com> wrote:

> On Wed, Sep 9, 2015 at 9:03 AM, Richard Eisenberg <eir at cis.upenn.edu>
> wrote:
> > No functions (excepting `error` and friends) are truly levity
> polymorphic.
>
> I was talking with Ed Kmett about this yesterday, and he pointed out
> that this isn't true. There are a significant array of levity
> polymorphic functions having to do with reference types. They simply
> shuffle around pointers with the right calling convention, and don't
> really care what levity their arguments are, because they're just
> operating uniformly either way. So if we had:
>
>     MVar# :: forall (l :: Levity). * -> TYPE (Boxed l) -> TYPE (Boxed
> Unlifted)
>
> then:
>
>     takeMVar :: forall s (l :: Levity) (a :: TYPE (Boxed l)). MVar# s
> l a -> State# s -> (# State# s, a #)
>     putMVar :: forall s (l :: Levity) (a :: Type (Boxed l)). MVar# s l
> a -> a -> State# s -> State# s
>
> are genuinely parametric in l. And the same is true for MutVar#,
> Array#, MutableArray#, etc.
>
> I think data type constructors are actually parametric, too (ignoring
> data with ! in them for the moment; the underlying constructors of
> those). Using a constructor just puts the pointers for the fields in
> the type, and matching on a constructor gives them back. They don't
> need to care whether their fields are lifted or not, they just
> preserve whatever the case is.
>
> But this:
>
> > We use levity polymorphism in the types to get GHC to use its existing
> type inference to infer strictness. By the time type inference is done, we
> must ensure that no levity polymorphism remains, because the code generator
> won't be able to deal with it.
>
> Is not parametric polymorphism; it is ad-hoc polymorphism. It even has
> the defaulting step from type classes. Except the ad-hoc has been
> given the same notation as the genuinely parametric, so you can no
> longer identify the latter. (I'm not sure I'm a great fan of the
> ad-hoc part anyway, to be honest.)
>
> -- Dan
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20150909/7bd0c6aa/attachment-0001.html>