Levity polymorphism in Core types
(This about Core for now, but writing a GHC proposal to bring simple inference of levity-polymorphism into the surface language is on my long-term TODO/wish list. I think #15532 is more relevant to the surface language.)
Today, UnliftedType
(= TYPE (BoxedRep Unlifted)
) is effectively a sub-kind of Type
(= TYPE (BoxedRep Lifted)
). But
- It's currently impossible to re-use functions expecting
Type
with values of kindUnliftedType
. It's always safe to coerce a value ofUnliftedType
into aType
and it should be pretty simple to do so! (ButCoercible
's coercions today are symmetric. The sub-kinding relation is not.) - Not every
UnliftedType
has aType
twin. I don't see why! Until recently, data types have been exclusively of lifted kind. UnliftedDatatypes changed that, now we can even have levity polymorhpic datatypes. By contrast,Array#
etc. could all reasonably have lifted counterparts at which point we can make their type constructors levity-polymorphic, too.
If we can fix (2), we'll have an easy time at fixing (1): I propose that binders in Core that have kind Type
to be reducible to the form (forall l. TYPE (BoxedRep l)) Lifted
at all times, so that it's easy to switch the Lifted
to Unlifted
when needed. I imagine a simple transformation that does levity generalisation that would probably be quite simple. Then we can make case binders have UnliftedType
and get the goodness of tag inference (#16970 (closed)) right in the kind system, for free!
Worker/wrapper can exploit strictness on boxed types that it has no unboxed equivalent for by making the binders of the worker have UnliftedType
. Example from the UnliftedDatatypes proposal:
data IntSet
= Branch !IntSet !Int !IntSet
| Leaf
member :: Int -> IntSet -> Bool
member !k Leaf = False
member k (Branch l k' r)
| k == k' = True
| k < k' = member k l
| otherwise = member k r
turns into
type IntSet :: forall l. TYPE (BoxedRep l) -- automatically generalised in Core
Branch :: forall l. IntSet @Unlifted -> Int# -> IntSet @Unlifted -> IntSet @l
Leaf :: forall l. Proxy# () -> IntSet @l -- quick fix for #19487
member :: forall l1 l2. Int @l1 -> IntSet @l2 -> Bool @Lifted
member k s = case k of (k' :: Int @Unlifted) { I# k'' ->
case s of (s' :: IntSet @Unlifted) { __DEFAULT ->
$wmember k'' s'
}
}
$wmember :: Int# -> IntSet @Unlifted -> Bool @Lifted
$wmember k s = case s of
Leaf -> False
Branch l k' r -> case k ==# k' of
1# -> True
0# -> case k <# k' of
1# -> $wmember k l
0# -> $wmember k r
Whether or not the user declared IntSet
to be levity-polymorphic, it is automatically lowered as levity-polymorphic, because of (1).
Note the lowered field types of Branch
: Strict fields are lowered as fields of the UnliftedType
twin. No need for dataConRepStrictness
anymore, it's all in the kind!
And it pays off, too: The wrapper member
does the seq
to maintain the invariant that the binder s
has UnliftedType
and thus is always tagged. Nice! No tag checks, the same generated code as if the user had declared IntSet
to be an UnliftedType
in the first place.
In the long run, I hope that we can lift part of the levity generalisation transformation into the type inference engine, so that it will infer a levity-polymorphic kind for a let-binding if that's possible. But that's pretty far in the future at the moment...