尾位置上下文 GHC 连接点文件是如何形成的？
How are tail-position contexts GHC join points paper formed?
Compiling without Continuations 描述了一种使用连接点扩展 ANF 系统 F 的方法。 GHC 本身在 Core（一种中间表示）中有连接点，而不是直接在表面语言中暴露连接点（Haskell）。出于好奇，我开始尝试编写一种语言来简单地使用连接点扩展 System F。也就是说，连接点是面向用户的。但是，论文中的打字规则有些地方我不明白。以下是我理解的部分：
- 有两种环境，一种是普通的values/functions，一种是只有连接点。
∆ 在几条规则中 ε 的合理性。在表达式 let x:σ = u in ... 中，u 不能引用任何连接点 (VBIND)，因为它的连接点不能 return 到任意位置。JBIND 的奇怪打字规则。这篇论文很好地解释了这一点。
这是我不明白的。这篇论文介绍了一种我称之为“头顶箭头”的符号，但论文本身并没有明确地给它命名或提及它。从视觉上看，它看起来像一个指向右边的箭头，位于表达式上方。粗略地说，这似乎表示“尾部上下文”（论文确实使用了这个术语）。在本文中，这些上方箭头可以应用于术语、类型、数据构造器，甚至环境。它们也可以嵌套。这是我遇到的主要困难。有几条规则的前提包括上方箭头下的类型环境。 JUMP、CASE、RVBIND、RJBIND均包含具有此类环境的前提（论文中的图2）。但是，none 的类型规则有一个结论，类型环境位于上方箭头下。因此，我看不出如何使用 JUMP、CASE 等，因为前提不能由任何其他规则推导出来。
这是个问题，但是如果有人有任何补充 material 提供更多上下文是开销箭头约定，或者如果有人知道 System-F-with-join-points 类型系统的实现（除了在 GHC 的 IR 中），这也会有帮助。
据我所知 SPJ 的符号风格，这确实与我在论文中看到的一致，它只是表示“0 或更多”。例如。您可以将 \overarrow{a} 替换为 a_1, …, a_n、n >= 0.
在某些情况下可能是“1个或多个”，但应该不难判断两者中的一个。
在本文中，x⃗表示“x的序列，由适当的分隔符分隔”.
举几个例子：
如果x是一个变量，λx⃗。 e是λx1的缩写。 λx2。 …λxne。换句话说，许多嵌套的 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⃗，和一个 return 类型 τ.
将东西“压缩”在一起：
有时，多次使用顶部箭头会隐含约束它们的序列具有相同的长度。发生这种情况的一个地方是替换。
{ϕ/⃗a}表示“替换a 1 为 ϕ1，替换 a2 为 ϕ 2, …, 将 an 替换为 ϕn”，隐含地断言 a⃗ 和 ϕ⃗长度相同，n.
工作示例：JUMP 规则：
JUMP 规则很有趣，因为它提供了排序的多种用途，甚至是 前提 的序列。再次重申规则：
(j : ∀a⃗. σ⃗ → ∀r. r) ∈ Δ
(Γ; ε ⊢⃗ u : σ {ϕ/⃗a})
Γ; Δ ⊢ jump j ϕ⃗ u⃗ τ : τ
第一个前提应该相当简单，现在：在标签上下文 Δ 中查找 j，并检查 j 的类型以一串∀s开头，接着是一堆函数类型，以一个∀r结尾。 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
Compiling without Continuations 描述了一种使用连接点扩展 ANF 系统 F 的方法。 GHC 本身在 Core（一种中间表示）中有连接点，而不是直接在表面语言中暴露连接点（Haskell）。出于好奇，我开始尝试编写一种语言来简单地使用连接点扩展 System F。也就是说，连接点是面向用户的。但是，论文中的打字规则有些地方我不明白。以下是我理解的部分：
- 有两种环境，一种是普通的values/functions，一种是只有连接点。
∆在几条规则中ε的合理性。在表达式let x:σ = u in ...中，u不能引用任何连接点 (VBIND)，因为它的连接点不能 return 到任意位置。JBIND的奇怪打字规则。这篇论文很好地解释了这一点。
这是我不明白的。这篇论文介绍了一种我称之为“头顶箭头”的符号，但论文本身并没有明确地给它命名或提及它。从视觉上看，它看起来像一个指向右边的箭头，位于表达式上方。粗略地说，这似乎表示“尾部上下文”（论文确实使用了这个术语）。在本文中，这些上方箭头可以应用于术语、类型、数据构造器，甚至环境。它们也可以嵌套。这是我遇到的主要困难。有几条规则的前提包括上方箭头下的类型环境。 JUMP、CASE、RVBIND、RJBIND均包含具有此类环境的前提（论文中的图2）。但是，none 的类型规则有一个结论，类型环境位于上方箭头下。因此，我看不出如何使用 JUMP、CASE 等，因为前提不能由任何其他规则推导出来。
这是个问题，但是如果有人有任何补充 material 提供更多上下文是开销箭头约定，或者如果有人知道 System-F-with-join-points 类型系统的实现（除了在 GHC 的 IR 中），这也会有帮助。
据我所知 SPJ 的符号风格，这确实与我在论文中看到的一致，它只是表示“0 或更多”。例如。您可以将 \overarrow{a} 替换为 a_1, …, a_n、n >= 0.
在某些情况下可能是“1个或多个”，但应该不难判断两者中的一个。
在本文中，x⃗表示“x的序列，由适当的分隔符分隔”.
举几个例子：
如果x是一个变量，λx⃗。 e是λx1的缩写。 λx2。 …λxne。换句话说，许多嵌套的 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⃗，和一个 return 类型 τ.
将东西“压缩”在一起：
有时，多次使用顶部箭头会隐含约束它们的序列具有相同的长度。发生这种情况的一个地方是替换。
{ϕ/⃗a}表示“替换a 1 为 ϕ1，替换 a2 为 ϕ 2, …, 将 an 替换为 ϕn”，隐含地断言 a⃗ 和 ϕ⃗长度相同，n.
工作示例：JUMP 规则：
JUMP 规则很有趣，因为它提供了排序的多种用途，甚至是 前提 的序列。再次重申规则：
(j : ∀a⃗. σ⃗ → ∀r. r) ∈ Δ
(Γ; ε ⊢⃗ u : σ {ϕ/⃗a})
Γ; Δ ⊢ jump j ϕ⃗ u⃗ τ : τ
第一个前提应该相当简单，现在：在标签上下文 Δ 中查找 j，并检查 j 的类型以一串∀s开头，接着是一堆函数类型，以一个∀r结尾。 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