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

Question

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

• 有两种环境，一种用于普通值/函数，另一种只有连接点。
• 合理的?是?在几个规则。在表达式中let x:? = u in ...，u不能引用任何连接点（VBIND），因为它连接点不能返回到任意位置。
• 的奇怪打字规则JBIND。这篇论文很好地解释了这一点。

这是我没有得到的。论文引入了一个符号，我将其称为“高架箭头”，但论文本身并没有明确给出名称或提及它。从视觉上看，它看起来像一个指向右侧的箭头，它位于表达式之上。粗略地说，这似乎表示“尾部上下文”（论文确实使用了这个术语）。在论文中，这些开销箭头可以应用于术语、类型、数据构造函数，甚至环境。它们也可以嵌套。这是我遇到的主要困难。有几条规则包含在头顶箭头下的类型环境。JUMP, CASE, RVBIND, 和RJBIND都包括具有这种类型环境的场所（论文中的图 2）。然而，没有一个类型规则有一个结论，其中类型环境在一个开销箭头下。所以，我看不出如何使用JUMP,CASE等，因为前提不能由任何其他规则导出。

这是问题，但如果有人有任何补充材料提供更多上下文是开销箭头约定，或者如果有人知道 System-F-with-join-points 类型系统的实现（GHC 的 IR 除外），那将也很有帮助。

Answer 1

在本文中，x? 表示“由适当的分隔符分隔的x序列”。

几个例子：

如果x是一个变量， ? X？. e是 ? × ₁。? × ₂。……？X _ñ ë。换句话说，许多嵌套的 1 参数 lambda，或多参数 lambda。

如果？和？是类型，?? ? ? 是 的缩写？₁ ? ? ₂ ? ……？? _ň？? . 换句话说，具有许多参数类型的函数类型。

如果a是类型变量并且? 是一种类型，？一种？. ? 是 的缩写？一个₁。? 一个₂。……？一个_n。? . 换句话说，许多嵌套的多态函数，或具有许多类型参数的多态函数。

在论文的图 1 中，跳转表达式的语法定义为：

e , u , v ? …… | 跳 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? , 和返回类型? .

把东西“压缩”在一起：

有时，多次使用开销箭头会隐含约束它们的序列具有相同的长度。发生这种情况的一个地方是替换。

{ ? /? 一个}手段“替换一个₁与？₁，更换一个₂与？₂，...，更换一个_ñ用？_n ”，隐含断言两者都a? 和?? 具有相同的长度n。

工作示例：JUMP规则：

该JUMP规则很有趣，因为它提供了排序的多种用途，甚至是一系列前提。这里又是一条规则：

（Ĵ：一个？。??？？- [R 。- [R ）？?

(?; ? ?? u : ? { ? /? a })

?; ? ? 跳 j ?? 你？ ? ：？

现在，第一个前提应该相当简单：在标签上下文 ? 中查找j，并检查j的类型是否以一堆 ?s 开头，然后是一堆函数类型，以 ? 结尾。r。r。

第二个“前提”实际上是一系列前提。它在循环什么？到目前为止，我们在范围内的序列是?? , ?? ，一个？，你呢？.

?? 和一个？在嵌套序列中使用，所以可能不是这两个。

另一方面，你呢？和?? 如果你考虑一下它们的意思，这似乎很合理。

?? 是标签j和u期望的参数类型列表吗？是提供给标签j的参数项列表，您可能想要一起迭代参数类型和参数项是有道理的。

所以这个“前提”实际上是这样的：

每对？和ü：

?; ? ? 你：？{ ? /? 一个}

伪 Haskell 实现

最后，这里有一个比较完整的代码示例，它说明了这个类型规则在实际实现中的样子。X？被实现为x值的列表，M当不满足前提时，一些 monad用于发出失败信号。

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