haskell - GHC连接点纸的尾部位置上下文是如何形成的？

Compiling without Continuations描述了一种使用连接点扩展ANF系统F的方法。 GHC本身在Core(中间表示)中具有连接点，而不是直接在表面语言(Haskell)中公开连接点。出于好奇，我开始尝试编写一种只用连接点扩展System F的语言。也就是说，连接点是面向用户的。但是，论文中有些关于打字规则的内容我不理解。这是我确实了解的部分:

有两种环境，一种用于普通值/函数，另一种仅具有连接点。

在一些规则中，∆的合理性是ε。在表达式let x:σ = u in ...中，u无法引用任何连接点(VBIND)，因为它的连接点无法返回到任意位置。

JBIND的奇怪输入规则。这篇论文很好地解释了这一点。

这是我不明白的。本文引入了一种表示法，我将其称为“开销箭头”，但是本文本身并未明确为其命名或提及。在外观上，它看起来像是指向右侧的箭头，并且位于表达式上方。粗略地说，这似乎表明存在“尾部上下文”(本文确实使用了该术语)。在本文中，这些开销箭头可以应用于术语，类型，数据构造器甚至环境。它们也可以嵌套。这是我遇到的主要困难。有多个前提条件的规则，这些规则包括开销箭头下的类型环境。 JUMP，CASE，RVBIND和RJBIND都包含具有这种类型环境的前提(本文中的图2)。但是，在类型环境位于开销箭头下方的情况下，没有任何键入规则得出结论。因此，我看不到JUMP，CASE等如何使用，因为前提不能由其他任何规则派生。
这就是问题所在，但是如果有人有提供更多上下文的补充 Material 是开销箭头约定，或者如果有人知道System-F-join-points类型系统的实现(GHC的IR中除外)，那将是也有帮助。

最佳答案

在本文中，x⃗表示为“x的序列，由适当的定界符分隔” 。
几个例子:
如果x是一个变量，则为λx⃗。 e是λx1的缩写。 λx2。 …λxne。换句话说，许多嵌套的1参数lambda，或许多参数lambda。
如果σ和τ是类型，则σ⃗→τ是σ1→σ2→…→σn→τ的缩写。换句话说，具有许多参数类型的函数类型。
如果a是类型变量，而σ是类型，则为“a”。 σ是∀a1的缩写。 ∀a2。 ……∀。 σ。换句话说，许多嵌套的多态函数或具有许多类型参数的多态函数。
在本文的图1中，跳转表达式的语法定义为:

如果将此声明转换为Haskell数据类型，则可能如下所示:

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.

也就是说，一个数据构造函数采用一个标签变量j，一系列类型参数ϕ⃗，一系列术语参数e⃗和返回类型τ。
将内容“压缩”在一起:
有时，多次使用开销箭头会隐含一些约束，即它们的序列必须具有相同的长度。发生这种情况的地方之一就是替换。
{ϕ/⃗a}的意思是“用11替换a1，用ϕ2替换a2，…，用ϕn替换a”，隐含地断言a⃗和both的长度相同。
可行的示例:JUMP规则:JUMP规则很有趣，因为它提供了排序的几种用法，甚至提供了前提序列。再次遵循以下规则:

现在，第一个前提应该非常简单:在标签上下文Δ中查找j，并检查j的类型以一堆∀开始，然后是一堆函数类型以，r结尾。河
第二个“前提”实际上是一系列前提。它循环了什么？到目前为止，我们范围内的序列是ϕ⃗，σ⃗，a⃗和u⃗。
ϕ⃗和a⃗是按嵌套顺序使用的，因此可能不是这两个。
另一方面，如果考虑它们的含义，u⃗和σ⃗似乎很合理。
σ⃗是标签j期望的参数类型的列表，而u⃗是提供给标签j的参数术语的列表，这很有意义，您可能想一起遍历参数类型和参数项。
因此，这种“前提”实际上是这样的:


伪Haskell实现
最后，这是一个比较完整的代码示例，说明了此键入规则在实际实现中的外观。 x⃗被实现为x值的列表，并且某些monad M用于在不满足前提条件时发出故障信号。

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