Unlifted data types

[Dan Doel]

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