How are tail-position contexts GHC join points paper formed?

Question

Compiling without Continuations describes a way to extend ANF System F with join points. GHC itself has join points in Core (an intermediate representation) rather than exposing join points directly in the surface language (Haskell). Out of curiosity, I started trying to write a language that simply extends System F with join points. That is, the join points are user facing. However, there's something about the typing rules in the paper that I don't understand. Here are the parts that I do understand:

• There are two environments, one for ordinary values/functions and one that only has join points.
• The rational for ∆ being ε in several of the rules. In the expression let x:σ = u in ..., u cannot reference any join points (VBIND) because it join points cannot return to arbitrary locations.
• The strange typing rule for JBIND. The paper does a good job explaining this.

Here's what I don't get. The paper introduces a notation that I will call the "overhead arrow", but the paper itself does not explicitly give it a name or mention it. Visually, it looks like a arrow pointing to the right, and it goes above an expression. Roughly, this seems to indicate a "tail context" (the paper does use this term). In the paper, these overhead arrows can be applied to terms, types, data constructors, and even environments. They can be nested as well. Here's the main difficulty I'm having. There are several rules with premises that include type environments under an overhead arrow. JUMP, CASE, RVBIND, and RJBIND all include premises with such a type environment (Figure 2 in the paper). However, none of the typing rules have a conclusion where the type environment is under an overhead arrow. So, I cannot see how JUMP, CASE, etc. can ever be used since the premises cannot be derived by any of the other rules.

That's the question, but if anyone has any supplementary material that provides more context are the overhead arrow convention or if anyone is aware an implementation of the System-F-with-join-points type system (other than in GHC's IR), that would be helpful too.

Answer 1

In this paper, x⃗ means “A sequence of x, separated by appropriate delimiters”.

A few examples:

If x is a variable, λx⃗. e is an abbreviation for λx₁. λx₂. … λx_ne. In other words, many nested 1-argument lambdas, or a many-argument lambda.

If σ and τ are types, σ⃗ → τ is an abbreviation for σ₁ → σ₂ → … → σ_n → τ. In other words, a function type with many parameter types.

If a is a type variable and σ is a type, ∀a⃗. σ is an abbreviation for ∀a₁. ∀a₂. … ∀a_n. σ. In other words, many nested polymorphic functions, or a polymorphic function with many type parameters.

In Figure 1 of the paper, the syntax of a jump expression is defined as:

e, u, v ⩴ … | jump j ϕ⃗ e⃗ τ

If this declaration were translated into a Haskell data type, it might look like this:

data Term
  -- | A jump expression has a label that it jumps to, a list of type argument
  -- applications, a list of term argument applications, and the return type
  -- of the overall `jump`-expression.
  = Jump LabelVar [Type] [Term] Type
  | ... -- Other syntactic forms.

That is, a data constructor that takes a label variable j, a sequence of type arguments ϕ⃗, a sequence of term arguments e⃗, and a return type τ.

“Zipping” things together:

Sometimes, multiple uses of the overhead arrow place an implicit constraint that their sequences have the same length. One place that this occurs is with substitutions.

{ϕ/⃗a} means “replace a₁ with ϕ₁, replace a₂ with ϕ₂, …, replace a_n with ϕ_n”, implicitly asserting that both a⃗ and ϕ⃗ have the same length, n.

Worked example: the JUMP rule:

The JUMP rule is interesting because it provides several uses of sequencing, and even a sequence of premises. Here’s the rule again:

(j : ∀a⃗. σ⃗ → ∀r. r) ∈ Δ

(Γ; ε ⊢⃗ u : σ {ϕ/⃗a})

---

Γ; Δ ⊢ jump j ϕ⃗ u⃗ τ : τ

The first premise should be fairly straightforward, now: lookup j in the label context Δ, and check that the type of j starts with a bunch of ∀s, followed by a bunch of function types, ending with a ∀r. r.

The second “premise” is actually a sequence of premises. What is it looping over? So far, the sequences we have in scope are ϕ⃗, σ⃗, a⃗, and u⃗.

ϕ⃗ and a⃗ are used in a nested sequence, so probably not those two.

On the other hand, u⃗ and σ⃗ seem quite plausible if you consider what they mean.

σ⃗ is the list of argument types expected by the label j, and u⃗ is the list of argument terms provided to the label j, and it makes sense that you might want to iterate over argument types and argument terms together.

So this “premise” actually means something like this:

for each pair of σ and u:

Γ; ε ⊢ u : σ {ϕ/⃗a}

Pseudo-Haskell implementation

Finally, here’s a somewhat-complete code sample illustrating what this typing rule might look like in an actual implementation. x⃗ is implemented as a list of x values, and some monad M is used to signal failure when a premise is not satisfied.

data LabelVar
data Type
  = ...
data Term
  = Jump LabelVar [Type] [Term] Type
  | ...

typecheck :: TermContext -> LabelContext -> Term -> M Type
typecheck gamma delta (Jump j phis us tau) = do
  -- Look up `j` in the label context. If it's not there, throw an error.
  typeOfJ <- lookupLabel j delta
  -- Check that the type of `j` has the right shape: a bunch of `foralls`,
  -- followed by a bunch of function types, ending with `forall r.r`. If it
  -- has the correct shape, split it into a list of `a`s, a list of `\sigma`s
  -- and the return type, `forall r.r`.
  (as, sigmas, ret) <- splitLabelType typeOfJ
  
  -- exactZip is a helper function that "zips" two sequences together.
  -- If the sequences have the same length, it produces a list of pairs of
  -- corresponding elements. If not, it raises an error.
  for each (u, sigma) in exactZip (us, sigmas):
    -- Type-check the argument `u` in a context without any tail calls,
    -- and assert that its type has the correct form.
    sigma' <- typecheck gamma emptyLabelContext u
    
    -- let subst = { \sequence{\phi / a} }
    subst <- exactZip as phis
    assert (applySubst subst sigma == sigma')
  
  -- After all the premises have been satisfied, the type of the `jump`
  -- expression is just its return type.
  return tau
-- Other syntactic forms
typecheck gamma delta u = ...

-- Auxiliary definitions
type M = ...
instance Monad M

lookupLabel :: LabelVar -> LabelContext -> M Type
splitLabelType :: Type -> M ([TypeVar], [Type], Type)
exactZip :: [a] -> [b] -> M [(a, b)]
applySubst :: [(TypeVar, Type)] -> Type -> Type

Answer 2

As far as I know SPJ’s style for notation, and this does align with what I see in the paper, it simply means “0 or more”. E.g. you can replace \overarrow{a} with a_1, …, a_n, n >= 0.

It may be “1 or more” in some cases, but it shouldn’t be hard to figure one which one of the two.