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

Question

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

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

∆ 的合理性正在 ε在几个规则中。在表达式 let x:σ = u in ... , u不能引用任何连接点 ( VBIND )，因为它连接点不能返回到任意位置。

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

这是我不明白的。论文介绍了一种我称之为“头顶箭头”的符号，但论文本身并没有明确地给它命名或提及它。从视觉上看，它看起来像一个指向右侧的箭头，并且位于表达式上方。粗略地说，这似乎表明了一个“尾部上下文”(论文确实使用了这个术语)。在本文中，这些箭头可以应用于术语、类型、数据构造函数甚至环境。它们也可以嵌套。这是我遇到的主要困难。有几条前提规则包括顶箭头下的类型环境。 JUMP , CASE , RVBIND , 和 RJBIND所有都包括具有这种类型环境的场所(本文中的图 2)。但是，没有任何类型的规则得出结论，其中类型环境位于顶箭头下方。所以，我看不到 JUMP , CASE等可以使用，因为前提不能由任何其他规则推导出来。
这就是问题所在，但如果有人有任何提供更多上下文的补充 Material 是头顶箭头约定，或者如果有人知道 System-F-with-join-points 类型系统的实现(除了 GHC 的 IR)，那将也有帮助。

Answer 1

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

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

如果将此声明转换为 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} 的意思是“用 ϕ1 代替 a1，用 ϕ2 代替 a2，……，用 ϕn 代替 an”，隐含地断言 a⃗ 和 ϕ⃗ 具有相同的长度 n。
工作示例: JUMP规则: JUMP rule 很有趣，因为它提供了排序的多种用途，甚至是一系列前提。又是一条规则:

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

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

---

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

现在，第一个前提应该相当简单:在标签上下文 Δ 中查找 j，并检查 j 的类型是否以一堆 ∀s 开头，然后是一堆函数类型，以 ∀r 结尾。河。
第二个“前提”实际上是一系列前提。它在循环什么？到目前为止，我们在范围内的序列是 φ⃗、σ⃗、a⃗ 和 u⃗。
ϕ⃗ 和 a⃗ 在嵌套序列中使用，所以可能不是这两个。
另一方面，如果考虑它们的含义，u⃗ 和 σ⃗ 似乎很合理。
σ⃗ 是标签 j 期望的参数类型列表，而 u⃗ 是提供给标签 j 的参数项列表，您可能希望一起迭代参数类型和参数项是有道理的。
所以这个“前提”实际上是这样的:

for each pair of σ and u:

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

伪 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