是否真的可以从构造微积分中删除 "Pi"？
Is it actually possible to remove "Pi" from Calculus of Constructions?
文章 Simpler, Easier! 声称即使不存在 "Pi" 也可以对依赖类型系统进行编码 - 也就是说，您可以为其重用 "Lam" 构造函数。但是，如果 "Pi" 和 "Lam" 在某些情况下被区别对待，那怎么可能呢？
另外，"Star"可以去掉吗？我认为您可以将所有出现的地方替换为“λ x . x”(id)。
这就像 Haskell 中的 (a, b) 一样重载：它既可以是类型，也可以是值。您可以对 Π 和 λ 使用相同的活页夹，typechecker 将根据上下文决定您的意思。如果您将一个活页夹与另一个活页夹进行类型检查，那么前者是 λ，后者是 Π — 这就是为什么您不能明确地将 * 替换为 λ x . x — 因为那样的话前者的活页夹可能是 Π，后者是 *（* 作为活页夹对我来说没有任何意义）。 ∀ = λ 和 * = λ x . x 有一个更大的问题：通过传递性 * = ∀ x . x，这是假设 False 的常用方法——这种类型必须在声音系统中无人居住，所以你根本没有任何类型。
最近在 Coq-club "Similarities between forall and fun" 上有一个话题（gmane.org 给了我 "No such message"，是我吗？），这里是一些摘录：
多米尼克·穆里根:
And here is another with a small bibliography pointing to similar work:
http://www.macs.hw.ac.uk/~fairouz/forest/papers/journals-publications/jfp05.pdf
Ironically, according to that paper Coquand first presented the Calculus of
Constructions with a single, unified binder, following a convention
established by De Bruijn in AutoMath.
托尔斯滕·阿尔滕基希：
A function and its type are very different concepts even if they have
some superficial syntactic similarity.
Especially for the newcomer this identification is very confusing and
completely misleading. I do think that one should understand type
theoretical concepts from what they mean and not how they look like.
安德烈亚斯·阿贝尔:
My student Matthias Benkard also worked on such a system, see "Type
Checking without Types"
请注意，第一个 link 中描述的系统具有 Π 归约（即您可以像 lambda 一样应用 pi 类型）— 如果您统一 Π，您的系统也会有它和 λ 内部（而不是语法上）。第二个描述的系统 link 统一了类型和值
One immediate consequence is the absence of any distinction between
types and their inhabitants: Every value is a type containing itself
and all of its parts; and conversely, every type is a composite value
consisting of its inhabitants.
所以实际上只有一个活页夹（let 和 fix 除外）。
文章 Simpler, Easier! 声称即使不存在 "Pi" 也可以对依赖类型系统进行编码 - 也就是说，您可以为其重用 "Lam" 构造函数。但是，如果 "Pi" 和 "Lam" 在某些情况下被区别对待，那怎么可能呢？
另外，"Star"可以去掉吗？我认为您可以将所有出现的地方替换为“λ x . x”(id)。
这就像 Haskell 中的 (a, b) 一样重载：它既可以是类型，也可以是值。您可以对 Π 和 λ 使用相同的活页夹，typechecker 将根据上下文决定您的意思。如果您将一个活页夹与另一个活页夹进行类型检查，那么前者是 λ，后者是 Π — 这就是为什么您不能明确地将 * 替换为 λ x . x — 因为那样的话前者的活页夹可能是 Π，后者是 *（* 作为活页夹对我来说没有任何意义）。 ∀ = λ 和 * = λ x . x 有一个更大的问题：通过传递性 * = ∀ x . x，这是假设 False 的常用方法——这种类型必须在声音系统中无人居住，所以你根本没有任何类型。
最近在 Coq-club "Similarities between forall and fun" 上有一个话题（gmane.org 给了我 "No such message"，是我吗？），这里是一些摘录：
多米尼克·穆里根:
And here is another with a small bibliography pointing to similar work:
http://www.macs.hw.ac.uk/~fairouz/forest/papers/journals-publications/jfp05.pdf
Ironically, according to that paper Coquand first presented the Calculus of Constructions with a single, unified binder, following a convention established by De Bruijn in AutoMath.
托尔斯滕·阿尔滕基希：
A function and its type are very different concepts even if they have some superficial syntactic similarity.
Especially for the newcomer this identification is very confusing and completely misleading. I do think that one should understand type theoretical concepts from what they mean and not how they look like.
安德烈亚斯·阿贝尔:
My student Matthias Benkard also worked on such a system, see "Type Checking without Types"
请注意，第一个 link 中描述的系统具有 Π 归约（即您可以像 lambda 一样应用 pi 类型）— 如果您统一 Π，您的系统也会有它和 λ 内部（而不是语法上）。第二个描述的系统 link 统一了类型和值
One immediate consequence is the absence of any distinction between types and their inhabitants: Every value is a type containing itself and all of its parts; and conversely, every type is a composite value consisting of its inhabitants.
所以实际上只有一个活页夹（let 和 fix 除外）。