Strictness in Kinds

strictness_in_kinds.md

Strictness in Kinds

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

"The strictness type variable needs to show up last, and it must have role phantom."

I'm concerned about the precedent for putting erasable stuff in the runtime rep. Per https://gitlab.haskell.org/ghc/ghc/issues/14917 it would be nice to have a monomorphizing quantifier. But with your plan we are left with a requirement that the runtime rep need only be shallowly monomorphized: Strict | Lazy is behind the pointer and thus not relevent. This means the "const eval" system that would go with the memorizing compiler would have to track not just all (deep) or nothing constantness, but also shallow (head) constantness.

condensed into one example, I'm worried about how to allow:

id :: foreach (constShallow r :: RuntimeRep). forall (a  :: TYPE r). a -> a
id a = a

foo :: forall s (a  :: TYPE (Lifted s)). a -> a
foo = id

Thanks for reminding me of that thread. I'd forgotten the excellent discussion that ensued. I'll summarize the relevant parts of the thread here both for my own benefits and for the benefit others perusing the mailing list. Josef wrote:

I'd introduce a new quantifier (let's call it "V") which provides *template polymorphism*. This quantifier can quantify over all kinds, even levity polymorphic things. The idea is that whenever a function of template polymorphic type is called, a new copy of the function will be created, specialized with the instantiated type for its template polymorphic type variables. Example: id :: V r (a :: TYPE r). a -> a id a = a ... More formally: A call to a template polymorphic function must instantiate all template polymorphic type parameters. These parameters must be instantiated with either fully ground types without any variables, or variables bound by "V", the template polymorphic quantifier.

And you described this system as:

Taking a step back, I think the first thing we need is a notion of a monomorphic term. A closed term is a monomorphic term, but some open terms are too. A term whose free variables are all irrelevant is also a monomorphic term. This might seem counterintuitive--maybe I need a new name because of that!--but it makes sense because we don't actually want to specialize on types: we just want to specialize on relevant things like run-time representations and constraint dictionaries.

Now, I'll return to the concerns you raised. In the proposal, I wrote:

The strictness type variable needs to show up last, and it must have role phantom.

I communicated this poorly. What I should have written was that the strictness type variable, as used in the data constructor, would be subject to the same restrictions that a phantom-role type variable would. It wouldn't actually have role phantom though. Indeed, it couldn't because coerce (in GHC 8.10) has type: coerce :: forall (r :: RuntimeRep) (a :: TYPE r) (b :: TYPE r). a -> b That is, the kinds must match. With that clarification out of the way, I'll get back to the real issue: relevance. The problem you forsee is:

I'm concerned about the precedent for putting erasable stuff in the runtime rep... With your plan we are left with a requirement that the runtime rep need only be shallowly monomorphized: Strict | Lazy is behind the pointer and thus not relevant.

Let's use Eisenberg's definition of relevance from Section 4.2.2 of Dependent Types in Haskell: Theory and Practice:

A quantifiee may be either relevant or irrelevant. A relevant quantifiee may be used anywhere in the function quantified over; an irrelevant quantifiee may be used only in irrelevant positions—that is, as an irrelevant argument to other functions or in type annotations. Note that relevance talks about usage in the function quantified over, not the type quantified over (which is covered by the dependency property). Relevance is very closely tied to type erasure. Relevant arguments in terms are precisely those arguments that are not erased. However, the relevance property applies equally to type-level functions, where erasure does not make sense, as all types are erased. For gaining an intuition about relevance, thinking about type erasure is a very good guide.

I'm not sure if this matters in this context, but there's also this weird thing going on with type constructor kinds. Eisenberg explains this in the GHC Proposal for reserving Dependent Haskell syntax as:

Type constructors use relevant quantification for all their arguments. Consider data Proxy k (a :: k) = P. Note that the kind argument is visible here for easy reference. Is Proxy Type distinct from Proxy (Type -> Type)? Could a type family match on these and then compute based on the difference between Type and Type -> Type? Surely, yes. That means that the kind k is quantified relevantly. Accordingly, because foreach is the relevant counterpart to forall, we really should use foreach in type constructor kinds: data Proxy :: foreach k -> k -> Type (or, if we want the kind to be invisible, data ProxyInvis :: foreach k. k -> Type).

Based on this definition of relevance, I don't understand the claim that "Strict | Lazy is behind the pointer and thus not relevant". How does that affect relevance? What would be wrong with the following function definitions (well, assuming that foreach somehow gets a magical template polymorphism ability): id :: foreach (r :: RuntimeRep). forall (a :: TYPE r). a -> a id a = a foo :: foreach (s :: Strictness). forall a :: TYPE ('Lifted s). a -> a foo = id @('Lifted s) @A

@andrewthad first of all I think you might want to check your markdown :).

If you are fine with:

id :: foreach (r :: RuntimeRep). forall (a :: TYPE r). a -> a
id a = a

foo :: foreach (s :: Strictness). forall a :: TYPE ('Lifted s). a -> a

foo = id @('Lifted s)

then there is no problem! Note that this means that foo (and forget and seqTyped like it) must be specialized to their strictness.

---

The strictness parameter could be irrelevant in principle, by which I mean not to TYPE or Lifted but the body of the \@(s : Strictness) -> body associated with a forall (s : Strictness). quantifier. (We know this is true because this is the case today, the ABI is the same!) I perhaps further discussion of this is useful to https://gitlab.haskell.org/ghc/ghc/issues/14917, but not to this issue.

---

I was just reminded of https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0019-constraint-vs-type.rst#old-proposal's third alternative. The goal there was (t :: Type) |> (Type ~R Constraint) :: Constraint. It sounds like this proposal would benefit from, if not need outright, (t :: TYPE (Lifted Strict)) |> (TYPE (Lifted Strict) ~R TYPE (Lifted Lazy)) :: TYPE (Lifted Lazy).

See also https://gitlab.haskell.org/ghc/ghc/wikis/unlifted-data-types

If the goal of this is optimizing the resulting code then the backend really wants three properties not two.

• Known tagged (WHNF)
• Unknown (Current LiftedRep behaviour)
• Known untagged (Thunk)

The known untagged isn't as important as you don't gain as much codegen wise, but you can still remove the check for the tag.

That is not to say we can't limit Core to just two and infer the rest as optimization on a best-effort basis.

What's the purpose of UnliftedRep here? Have you looked at the wiki page on unlifted data types? It has a similar approach to levity polymorphism with (non-zero-cost) coercions. In particular, I'd propose

data Levity = Lifted | Unlifted
data PointeeKind = Managed Levity | Unmanaged
data RuntimeRep
  = PtrRep PointeeKind
  | IntRep
  | ...
pattern AddrRep = PtrRep Unmanaged
pattern LiftedRep = PtrRep (Managed Lifted)
pattern UnliftedRep = PtrRep (Managed Unlifted)

And then introduce polymorphism over Levity.

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:

data Levity = Lifted | Unlifted
data RuntimeRep
  = PtrRep Levity
  | IntRep
  | ...

The structure you suggest is isomorphic to what I have in mind but with entirely different semantics communicated by the names:

data Strictness = Strict | Lazy
data Levity = Lifted Strictness | Unlifted
data RuntimeRep
  = PtrRep Levity
  | IntRep
  | ...
data ByteArray# :: TYPE ('PtrRep 'Unlifted)
data Addr# :: TYPE 'AddrRep
data UserDefined :: forall (s :: Strictness). TYPE ('PtrRep ('Lifted s))

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 of forget:

forget :: forall (a :: forall (s :: Strictness) -> TYPE ('PtrRep ('Lifted s))). a 'Strict -> a 'Lazy

Consider the above data types. We need forget to type check when called on a strict UserDefined, but it should never be able to accept ByteArray# as an argument. That is, there is no lazy variant of ByteArray#. By cutting it down to two kinds instead of three, you make it impossible to provide a meaningful type for forget.

Perhaps someone could make ByteArray# allowed to be lazy or strict with something like:

data CoreByteArray :: ... -- strictness polymorphic
newtype ByteArray# = ByteArray# (CoreByteArray# 'Strict) -- an unlifted newtype

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.

Ah, that makes sense. And indeed you say so right at the beginning, but I couldn't make much sense of it without reading the proposal first.

But then there's a cringeworthy separation between Lifted Strict and Unlifted. Apart from Lifted Strict not actually making much sense (but let's not engage in a bike-shedding discussion here), I can imagine that we want to write polymorphic functions that work on both. It sounds to me like Lifted Strict is really a sub-rep of Unlifted, namely those data types which also have a lifted variant.

But why not solve this with a type class? I called this LevityPolymorphic/LevityCoercible (seems I wasn't very consistent) on the wiki page. ByteArray# won't be an instance of this type-class, whereas user-defined data types might be. We could either have a semi-automatic mechanism via deriving or have it fully automated like Coercible. Then there's no need for a separate Unlifted anymore.