Support levity polymorphic interface

[konsumlamm]

Since GHC 9.4, various primitives (Array#, SmallArray#, MutVar#, ...) and their corresponding primops are now levity polymorphic. I propose making the primitive wrappers (Array, SmallArray, MutVar, ...) also levity polymorphic, so that users can take advantage of the levity polymorphism without having to use the primops from GHC.Exts directly.

This would also supersede primitive-unlifted afaict.

I'm not sure if this would be a breaking change, but it should at least be minor, since type variables default to kind Type (so Array a would still be Array (a :: Type)).

[simonpj]

Great idea!

[konsumlamm]

I though about this a bit more and there are some problems that arise:

1. Everything is gonna need an extra l :: Levity parameter, which is a lot to write unfortunately, but I don't think there's a way around that. Since a :: TYPE (BoxedRep l) needs that l, it apparently must be declared before that. So there are two options:

   • Make it an inferred type variable (forall {l :: Levity} ...), this would be backwards compatible, since the levity can't be specified with a type application.
   • Make it a specified type variable (forall (l :: Levity) ...), this would technically be a breaking change, since it changes the first applied type variable.

   Both approaches have pros and cons. The levity can probably be inferred through the type a most of the time, but i think making the levity a specified type variable would be acceptable too (for a major version bump), since I doubt that there are many people using primitive with TypeApplications.

2. A bigger problem is how to wrap mutable operations (using State# s -> (# State# s, a #)). This is the job of the PrimMonad class, but that only works for lifted types and we can't just change PrimMonad to be levity-polymorphic, since that would require changing the whole Monad hierarchy as well (and I don't see that happen any time soon). There are several possibilities to address this:

   • We could make our own class (levity-polymorphic or for unlifted types) and make instances for custom IO/ST types (levity polymorphic or for unlifted types). This would have the disadvantage that we can't simply use the standard IO/ST types (and we can't have a Monad instance either), but we could support all operations.
   • For operations that don't return anything (i.e. State# s -> State# s), we can just reuse primitive_ to return m ().
   • There could be a class to convert unlifted types to lifted types (like in the primitive-unlifted package), so that we can just use the standard PrimMonad, however it seems to be designed only for types like Array#, MutVar#, etc., that already have a lifted wrapper type. This means that using custom unlifted types (which is now possible via the UnliftedDatatypes extension) would require the boilerplate of defining a corresponding lifted type and having to convert between the two, which kinda defeats the point of having unlifted elements in the first place.
   • Use data-elevator to automatically convert between lifted/unlifted types where necessary. This is similar to the above approach, but it solves the problem of having to define a corresponding lifted type, although I'm not sure how stable it is.
   • Only make immutable stuff (Array, SmallArray) levity-polymorphic for now. I'm not sure if the above problems will change any time soon though, so I don't know if it's worth waiting for something better. We can still start by making the non-problematic stuff levity-polymorphic first though.
   • ...

Can you think of any other problems or solutions to the above problems? And what solutions would you prefer?

cc @andrewthad @sgraf812

[andrewthad]

Thanks for writing this up. I think this is a good area for improvement.

On question 1, I’m pretty strongly in favor of matching what the Array# does and making the levity argument be inferred. The backwards compatibility is nice, and in practice, I’ve never seen a situation where this would cause a problem.

On question 2, I think it would be sufficient to make write/index/copy operations levity polymorphic and leave read operations in their current deficient state. The strategy is backwards compatible, and it leaves open the possibility of improving the read operations if Monad ever becomes levity polymorphic. The other options would be a breaking change both now and possibly later if Monad were ever improved (since we would probably undo them at that point).

[simonpj]

Make it an inferred type variable (forall {l :: Levity} ...), this would be backwards compatible, since the levity can't be specified with a type application.

I believe that in many, perhaps all, existing levity-poly operations, the levity is Inferred. I think that's probably best.

But rather than guessing, this conversation would be much more concrete if you could write out

• a list of of the functions whose types would be changed (with before and after type)
• a list of functions that would become redundant (because a more polymorphic function now exists). Indeed you say that an entire package, primitive-unlifted, can go. That's great!
• a deprecation plan, for when to get rid of those unnecessary functions
• are any data types changed?

Without the specifics, it's hard to be sure that we are talking sense.

| however it seems to be designed only for types like Array#, MutVar#, etc., that already have a lifted wrapper type.

Also, about converting unlifted to lifted, as part of !8750 I have defined one "boxing type" for each RuntimeRep. These defns are in ghc-prim:GHC.Types. For example

data LiftBox   (a :: TYPE UnliftedRep) = MkLiftBox a

data IntBox    (a :: TYPE IntRep)      = MkIntBox a
data Int8Box   (a :: TYPE Int8Rep)     = MkInt8Box a
data Int16Box  (a :: TYPE Int16Rep)    = MkInt16Box a
data Int32Box  (a :: TYPE Int32Rep)    = MkInt32Box a
data Int64Box  (a :: TYPE Int64Rep)    = MkInt64Box a

Notice that these are polymorphic, although (necessarily) monomorphic in RuntimeRep.

I have not automated the boxing or unboxing steps... I just needed them internally in the compiler. Just mentioning them here in case it helps the conversation about lifting.

[andrewthad]

Here is the design that I envision (I would love to see other designs if people have other opinions about the best way to go about this):

Array :: forall {v :: Levity}. TYPE ('BoxedRep v) -> Type
MutableArray :: forall {v :: Levity}. Type -> TYPE ('BoxedRep v) -> Type
indexArray :: forall {v :: Levity} (a :: TYPE ('BoxedRep v)). Array a -> Int -> a
writeArray :: forall {v :: Levity} (m :: Type -> Type) (a :: TYPE ('BoxedRep v)). PrimMonad m => MutableArray s a -> Int -> a -> m ()
copyArray :: forall {v :: Levity} (m :: Type -> Type) (a :: TYPE ('BoxedRep v)). MutableArray s a -> Int -> Array a -> Int -> Int -> m ()
readArray :: forall (m :: Type -> Type) (a :: Type). MutableArray s a -> Int -> m a

With this design, readArray retains its existing restriction to lifted boxed types, but all other array are operators are improved to support both lifted and unlifted boxed types. To my understanding, this is completely backwards compatible. To address Simon's questions specifically:

• a list of of the functions whose types would be changed (with before and after type): an illustrative subset is given above, but other changed function include: indexArray##, copyMutableArray, newMutVar, writeMutVar, newMVar, putMVar. There are a ton of functions like cloneArray that won't really change but will pick up a forall {v :: Levity}... in their type signatures. At the module level, we would see changes in Data.Primitive.Array/SmallArray/MVar/MutVar, and no changes in Data.Primitive.Ptr/PrimArray.
• a list of functions that would become redundant (because a more polymorphic function now exists). Indeed you say that an entire package, primitive-unlifted, can go. That's great! Agreed, that's it. Nothing in primitive would be eliminated
• a deprecation plan, for when to get rid of those unnecessary functions. Nothing needs to be deprecated. The primitive-unlifted library could continue to exist but would be unneeded for some cases.
• are any data types changed? Array, MutableArray, MutVar, SmallArray, MutableSmallArray, MVar (from Data.Primitive.MVar, not from base).

The wrapper types (LiftBox, IntBox, etc.) that Simon mentions seem useful for a "one array type to rule them all" strategy. This strategy necessarily relies more heavily on typeclasses, and for an example of what this looks like, see contiguous. I think that for primitive though, we should continue to maintain the distinction between Array and PrimArray. I feel this way not because I think it's a great interface but because the breakage from any attempt to unify the types would be huge.

[sgraf812]

I think you wrote a few times LiftedRep instead of BoxedRep above. Otherwise, the types you wrote seem fine.

You might get in trouble with the type-checker though, because you will inevidably have to bind a levity-polymorphic variable x::a in, e.g., writeArray.

Anyway, I think the types are as general as possible, perhaps even more general than possible (at the moment in GHC).

[andrewthad]

Thanks. For the benefit of future readers, I've updated my previous comment to correct the mistaken uses LiftedRep.

I didn't realize that levity polymorphic binding was not yet supported by GHC. That greatly limits the utility of this change to primitive. Even so, I think I would still be fine with moving forward with my suggested interface (minus writeArray since GHC does not allow the levity polymorphized definition at the moment). On one hand, this is a bit of a rotten deal since the only convenience that users get is the ability to write folds over specialized arrays like addFields :: Array MyUnliftedType -> Int. On the other hand, there is a straightforward path for future improvements if GHC picks up additional levity-polymorphism capabilities (binding levity-polymorphic variables, having levity-polymorphic Functor/Applicative/Monad) over time.

Again, I'm open to other ideas on this. The whole thing may still be a bit premature, and we could always wait for GHC to progress a little more before changing anything.

[konsumlamm]

So I tried to make the functions levity polymorphic, using the approach @andrewthad suggested. The only functions where that is possible are the following:

• MVar: newEmptyMVar, isEmptyMVar
• MutVar: none
• Array/MutableArray: sizeofArray, sizeofMutableArray, indexArray##, freezeArray, unsafeFreezeArray, thawArray, unsafeThawArray, copyArray, copyMutableArray, cloneArray, cloneMutableArray, runArray
• SmallArray/SmallMutableArray: analogous to Array/SmallArray

In particular, there is no way to even create values of these types (with the exception of newEmptyMVar, which is pretty useless on its own). The problem is that we can't bind levity polymorphic variables, as @sgraf812 mentioned.

However, I don't think there's anything preventing levity polymorphic variables in theory (they're just a pointer either way). This has already been suggested: https://gitlab.haskell.org/ghc/ghc/-/issues/15532. @sgraf812 would it be possible to use data-elevator to somehow circumvent this problem in the meantime?

[sgraf812]

@sgraf812 would it be possible to use data-elevator to somehow circumvent this problem in the meantime?

I don't think data-elevator would help much here, because the levity polymorphism happens inside the data constructor/type constructor. If you wanted to cooperate with data-elevator (or the other way around), we could perhaps define LevitySubsumption instances like LevitySubsumption (Array (Strict a)) (Array (Lazy a)) (i.e., because Array is covariant).

What you could do to define the levity-polymorphic functions would be something like

writeArray :: forall {v :: Levity} (m :: Type -> Type) (a :: TYPE ('BoxedRep v)). PrimMonad m => MutableArray s a -> Int -> a -> m ()
writeArray = unsafeCoerce writeArrayImpl

writeArrayImpl :: forall (m :: Type -> Type) (a :: UnliftedType). PrimMonad m => MutableArray s a -> Int -> a -> m ()
writeArrayImpl = ...

(Actually, you could do a :: Type just as well, I think.)

We'll have to see wether unsafeCoerce gets in the way of optimisations, though.

Perhaps the levity-polymorphic API should go in a separate module and simply be implemented in terms of the Lifted one+unsafeCoerce.

[treeowl]

If we had a levity-polymorphic ST,

newtype ST s (a :: TYPE ('BoxedRep l)) = ST (State# s -> (# State# s, a #))

then we could support levity-polymorphic readArray, but not levity-polymorphic writeArray. Of course, >>= would still only work with lifted things, so I don't know how helpful that would be. To go further, we need a (preferably good) story for levity-polymorphic bindings. I have some opinions about that, but last I checked SPJ didn't like them.