实际上是否可以从构造微积分中删除"Pi"？

文章更简单,更容易!声称即使没有"Pi"存在也可以对依赖类型系统进行编码 - 也就是说,你可以重复使用"Lam"构造函数.但是,如果在某些情况下对"Pi"和"Lam"的处理方式不同,那又怎么可能呢？

此外,可以删除"明星"吗？我认为你可以用"λx.x"(id)替换它的所有出现.

这就像(a, b)在Haskell中一样重载:它既可以是类型也可以是值.你可以使用相同的绑定器?,?并且typechecker将从上下文中决定你的意思.如果你认为一个粘合剂与另一个粘合剂,那么前者是?,而后者是?- 这就是为什么你不能明确地替换*为? x . x- 因为那时前者的粘合剂可能?而后者是*(*作为粘合剂没有任何意义)我).还有一个更大的问题? = ?和* = ? x . x:通过传递* = ? x . x,这是假定的常用方法False-这种类型必须在一个健全的系统中无人居住,所以你不会有任何类型的.

Coq俱乐部最近有一个帖子"forall和fun之间的相似之处"(gmane.org给了我"没有这样的信息",这只是我吗？),这里有一些摘录:

多米尼克·穆里根:

另外还有一个小型参考书目指向类似的工作:

http://www.macs.hw.ac.uk/~fairouz/forest/papers/journals-publications/jfp05.pdf

具有讽刺意味的是,根据该论文,Coquand首先根据De Bruijn在AutoMath中建立的惯例,使用单一的统一粘合剂来呈现构造微积分.

Thorsten Altenkirch:

函数及其类型是非常不同的概念,即使它们具有一些表面的句法相似性.

特别是对于新手而言,这种识别非常混乱并且完全具有误导性.我认为人们应该理解类型理论概念,而不是它们的样子.

安德烈亚斯阿贝尔:

我的学生Matthias Benkard也参与了这样一个系统,参见"无类型检查"

http://www.cse.chalmers.se/~abela/benkardThesis.pdf

请注意,在第一个链接中描述的系统具有Π减少(即,您可以像lambdas一样应用pi类型) - 如果您统一?和?内部(而不是语法上),您的系统也会拥有它.并且在第二个链接处描述的系统统一了类型和值

一个直接后果是类型与居民之间没有任何区别:每个价值观都是包含自身及其所有部分的类型; 相反,每种类型都是由其居民组成的综合价值.

所以真的只有一个活页夹(除了let和可能fix).