Pun 演算

广义变量 punning（ad-hoc 多态）的 Typed Lambda 演算的一个变体。

贡献

通过复数抽象将 ad-hoc 多态引入到 Simply Typed Lambda 演算中。将如 λx:X. y 这样的项表示为 λ⟨x:X. y⟩。复数抽象用更多的花括号表示：λ⟨a:A. b⟩⟨x:X. y⟩。类型系统也略有扩展以支持复数类型：A + B。

动机

在 LSTS 证明辅助工具中，复数抽象的实用性变得明显。这在简单的函数应用 f(x) 中得到观察，其中函数候选者可以根据输入的性质证明多个属性。这是“复数箭头”概念的直接起源，这种箭头可以携带多个属性。PunC 是在升级 LSTS 框架之前尝试泛化这个想法的一种尝试。

类型

$$abstraction \quad \frac{\Gamma \vdash a:A \quad \Gamma \vdash b:B \quad \Gamma \vdash x:X \quad \Gamma \vdash y:Y \quad λ⟨a.b⟩⟨x.y⟩}{\Gamma \vdash λ⟨a.b⟩⟨x.y⟩:(A \to B) + (X \to Y)}$$

$$application \quad \frac{\Gamma \vdash f:(A \to B) + (C \to D) + (X \to Y) \quad \Gamma \vdash x:A + X \quad f(x)}{\Gamma \vdash f(x):B + Y}$$

评估

评估规则基本上与 lambda 演算相同，但有一个例外，即复数箭头可以同时携带多个值。这个特性导致可能产生新的方式的复数值。

示例分割（单值产生复数）

λ⟨a:Int.True⟩⟨x:Int.x⟩ 3
---------------------------------
⟨True⟩⟨3⟩

示例合并（复数值产生单值）

λ⟨a:Bool.2⟩⟨x:Int.2⟩ (⟨False⟩⟨5⟩)
---------------------------------
⟨2⟩

示例携带（复数值产生复数）

λ⟨a:Bool.not a⟩⟨x:Int.- x 2⟩ (⟨False⟩⟨5⟩)
---------------------------------
⟨True⟩⟨3⟩

可选约束

有时可能希望完全防止出现复数值。这要求类型系统表明不会发生任何分割，而分割总是复数值的根本原因。请注意，复数类型始终具有复数值。

$$ban \ plurals \quad \frac{\Gamma \vdash f:(A \to B)+(A \to C) \quad \Gamma \vdash x:A \quad \Gamma \vdash f(x)}{\Gamma \vdash \bot}$$

禁止复数仍然允许在“或”情况下进行特定情况的多态。

注释

"复数类型"类似于产品类型加上隐式的子类型关系，即A + B ⇒ A和A + B ⇒ B。类型要么是单数，要么是复数，永远不会同时是两者。如果你想把A + B转换成一个单数类型，那么你可以把它写成它对应的产品：(A,B)。

直接引用

类型理论的快速介绍

相关工作

特定情况多态的核心

可能的扩展

• 类型级别的字符串重写：a -> T<a>应用B尝试一个Relog统一a=B;T<a>
• $$terminal \ absurd \quad \frac{\Gamma \vdash f:A + ¬A}{\Gamma \vdash \bot}$$
• $$intermediate \ greedy \ infer \quad \frac{f:A \to B \quad f:B \to C}{f:A \to C}$$
• $$intermediate \ always \ follows \quad \frac{f: A \to B \quad f:¬ A \to B}{f(x): B}$$
• 子类型
• 依赖类型