Let's tweak GHC's RuntimeRep
stuff to try adding information about
strictness. This information could be helpful for avoiding evaluating
thunks that are guaranteed to already be evaluated. Presently,
RuntimeRep
is defined as:
data RuntimeRep
= LiftedRep
| UnliftedRep
| IntRep
| ...
Let's adjust this:
data Strictness = Strict | Lazy
data RuntimeRep
= LiftedRep Strictness
| UnliftedRep
| IntRep
| ...
type Type = TYPE ('LiftedRep 'Lazy)
In Levity Polymorphism,
Eisenberg and Peyton Jones argue that "kinds, not types, are calling
conventions". So what's the calling convention for these two new
kinds? We want LiftedRep Lazy
to behave just like the old LiftedRep
did, and we want LiftedRep Strict
to behave like UnliftedRep
.
So why bother introducing something new rather than reusing UnliftedRep
?
The answer is that we want some cool magic primitives, forget
and seqTyped
. These cannot be used with things like Array#
.
We'll get to them later. Let's write a spine-strict element-lazy
list data type as:
data List :: Type -> forall (s :: Strictness) -> TYPE ('LiftedRep s)
Cons :: a -> List a 'Strict -> List a s
Nil :: List a s
The strictness type variable needs to show up last, and it must have role phantom. That is, the data constructor cannot perform GADT-like analysis on it, and they cannot give it to their fields. With this in mind, we can throw this in the mix:
forget :: forall (a :: forall (s :: Strictness) -> TYPE ('LiftedRep s)). a 'Strict -> a 'Lazy
And forget
just compiles to a no-op. Any evaluated closure can be
treated as an unevaluated closure, a fortunate consequence of how
GHC's runtime was designed. (Notice that users cannot call this
on something like Array#
). Next, let us consider a better seq
:
seqTyped :: forall (a :: forall (s :: Strictness) -> TYPE ('LiftedRep s)). a 'Lazy -> a 'Strict
This function scrutinizes argument. This is not a no-op. It
turns into case
in GHC Core. Speaking of which, that case
would work differently. In GHC Core, we would want case
to
provide make the new identifier have a strict type:
case (ds1 :: List Int Lazy) of (ds2 :: List Int Strict) {
__DEFAULT -> ...
}
You could even have wrappers to support standard non-strict data types. If a user wrote:
data Foo = Foo Bool Bool Bool
The compiler could generate a wrapper:
data FooInternal :: forall (s :: Strictness) -> TYPE ('LiftedRep s) where
FooInternal :: Bool -> Bool -> Bool -> FooInternal s
newtype Foo = Foo (FooInternal 'Lazy)
And the user is none the wiser. Every data type would need to be internally rewritten in this way. Is all of this stuff actually sound? Who knows? It looks sound to me. But you really need someone who can write cool proofs like this:
τ type
---------------------
something → goes here
In Proposal #112, the levity type
data Levity = Lifted | Unlifted
was accepted will be implemented. I've just never gotten around to doing it. So, a future GHC will certainly have:The structure you suggest is isomorphic to what I have in mind but with entirely different semantics communicated by the names:
In your example, you've consolidated unmanaged pointers and managed pointers. That could be done with
data Levity = Lifted Strictness | Unlifted | Unmanaged
although I think it's orthogonal to the question at hand. We need three kinds, rather than two, for boxed types because offorget
:Consider the above data types. We need
forget
to type check when called on a strictUserDefined
, but it should never be able to acceptByteArray#
as an argument. That is, there is no lazy variant ofByteArray#
. By cutting it down to two kinds instead of three, you make it impossible to provide a meaningful type forforget
.Perhaps someone could make
ByteArray#
allowed to be lazy or strict with something like:Then you really could collapse unlifted types and strict lifted types into a single kind as you suggest. But this is more work, and there may be reasons not to do that to
ByteArray#
. I haven't thought about doing that much.