【发布时间】：2016-03-15 01:03:53
【问题描述】：
文章Simpler, Easier! 声称，即使没有“Pi”，也可以对依赖类型系统进行编码——也就是说，您可以为它重用“Lam”构造函数。但是，如果“Pi”和“Lam”在某些情况下被区别对待，这怎么可能呢？
另外，“星”可以去掉吗？我认为你可以用 "λ x . x" (id) 替换所有出现的它。
【问题讨论】：
标签： haskell types type-systems lambda-calculus
【发布时间】：2016-03-15 01:03:53
【问题描述】：
这只是像 Haskell 中的 (a, b) 那样重载：它既可以是类型也可以是值。您可以对Π 和λ 使用相同的活页夹，类型检查器将根据上下文确定您的意思。如果您将一个活页夹与另一个活页夹进行类型检查，那么前者是λ，后者是Π——这就是为什么你不能明确地将*替换为λ x . x——因为前一个活页夹可能是Π后者是*（* 作为活页夹对我来说没有任何意义）。 ∀ = λ 和 * = λ x . x 有一个更大的问题：通过传递性 * = ∀ x . x，这是假设 False 的常用方法——这种类型必须在声音系统中无人居住，所以你不会有任何类型全部。
最近有一个关于 Coq-club 的帖子“forall 和 fun 的相似之处”（gmane.org 给了我“没有这样的信息”，只有我一个人吗？），以下是一些摘录：
多米尼克·穆里根：
这里还有一个小参考书目指向类似的工作：
http://www.macs.hw.ac.uk/~fairouz/forest/papers/journals-publications/jfp05.pdf
具有讽刺意味的是，根据那篇论文，Coquand 首先提出了微积分 具有单一、统一的活页夹的结构，遵循约定 由 De Bruijn 在 AutoMath 中建立。
索斯滕·阿尔滕基希：
一个函数和它的类型是非常不同的概念，即使它们有 一些表面的句法相似性。
特别是对于新人来说，这种识别是非常令人困惑和 完全误导。我确实认为应该理解类型 理论概念来自它们的含义，而不是它们的外观。
安德烈亚斯·阿贝尔：
我的学生 Matthias Benkard 也研究过这样的系统，请参阅“Type 无类型检查”
请注意，第一个链接中描述的系统具有 Π-reduction（即，您可以像 lambdas 一样应用 pi-types）——如果您在内部统一 Π 和 λ（相反语法上）。第二个链接描述的系统统一了类型和值
一个直接的后果是两者之间没有任何区别 类型及其居民：每个值都是包含自身的类型 及其所有部分；相反，每种类型都是复合值 由其居民组成。
所以实际上只有一个活页夹（let 和可能fix 除外）。
【讨论】：
-
对不起，我不明白你是如何知道什么时候应该是 Pi 以及什么时候应该是 λ 的上下文。你能详细说明一下区别吗？
-
举个简单的例子，
λ (a : *) -> λ (x : a) -> a应用于自身。会发生什么？既然a : *和一切都是类型，那么这个词不是接受一切吗？ -
@Viclib，我有一个用于基本依赖类型理论的小类型检查器，我将尝试合并
Π和λ。如果您有[a : *] -> [x : a] -> a并将其应用于自身，则第一个 binder 的作用类似于 lambda，结果为[x : [a : *] -> [x : a] -> a] -> a。 -
@Viclib，我写了一些代码，下面是我遇到的一些问题：在
([ x : _ ] [ y : _ ] -> x) x y中，两个活页夹都是 lambdas，但要证明这一点，我们必须尽快减少术语（不确定它是否安全，但可能是的）或跟踪一个函数应用了多少个参数。当我们推断f x的类型时（因为我们到处都有显式类型，所有项都是可推断的），我们知道f是一个函数，但不知道x是什么。如果f是一个 lambda 并且x包含绑定器，那么我们必须减少表达式。 -
我们不能将未实例化的活页夹留在完全键入的术语中。
[x : _] -> ...的类型是什么？它可以是Π _ _和*。处理所有这些细节看起来太乏味了。无论如何，最好明确使用Π和λ。