如何解读本文中的输入规则？

Question

从"Milner-Hindley的哪个部分你不明白？" Stack Overflow问题,我可以阅读一些英文版本,但仍然很难弄清楚如何制作一个类型检查器.这是我尝试阅读前4条规则:

Ax:作为公理,如果x有A型,那么x有A型.(不是很明显吗？)
切割:如果上下文?证明t has type A,和另一种情况下?,扩展了断言x has type A,证明u has type B,那么这两个上下文一起证明的所有出现的取代x通过t在u已键入B.(那是什么意思呢？为什么有两种情况,额外的情况来自何处？另外,这似乎是一种替代规则,但如果替代不是一个术语,而是一种操作呢？经典米尔纳 - 欣德利没有这样的东西;对于App来说它只是一个非常简单的规则.)
弱:如果证明了上下文t has type A,那么用语句扩展的上下文x has type B仍然可以证明t has type A.(再说一次,这不是很明显吗？)
对照:如果上下文扩展了x1 has type !A和x2 has type !A证明t has type B,那么这种情况下,扩展了x has type !A证明代的所有出现x1并x2通过x在t具有类型B.(看来替换的另一条规则是什么呢？但是为什么上面有两个术语,下面有一个术语？另外,为什么那些!？这些都会出现在类型检查器上？)

我完全明白了这些规则想说的内容,但是在它真正点击之前我错过了一些东西,我能够实现相应的类型检查器.我该如何理解这些规则？

Answer 1

这有点过于宽泛,但从你的评论中我猜你缺乏一些线性类型系统的基础知识.这个系统有弱化(线性逻辑通常不允许),所以它实际上对应于仿射直觉逻辑.

关键的想法是:你可以使用你拥有的每个值(例如变量)一次.

类型A (x) B(张量积)大致代表对值的类型,您可以从中计算出A值和B值.

该类型A -o B代表一个消耗一个值的线性函数A(记住:最多一次使用!)并产生一个B.

你可以有例如\x.x : A -o A但你不能有任何术语,: A -o (A (x) A)因为这需要你使用两次参数.

类型!A("当然是A!")代表A可以复制的类型值- 正如你在非线性lambda演算中通常所做的那样.这是通过收缩规则完成的.

例如,!A -o !B表示一个普通函数:它需要一个值(在无限量的副本中)并产生一个值(在无限量的副本中).您可以编写!A -o (!A (x) !A)如下函数:

\a. (a (x) a)

请注意,具有多个前提的每个线性类型规则必须在前提之间拆分环境变量(例如,一个获取Gamma,另一个Delta),而不重叠.否则,您可以复制线性变量.因此,Cut有两种情况.非线性切割将是:

G |- t: A        G, x:A |- u: B
--------------------------------
  G |- u[t/x]: B

但在这里,这两个词t,并u可以使用的变量G,因此u[t/x]可以使用变量两次-并不好.相反,线性切割

G1 |- t: A        G2, x:A |- u: B
--------------------------------
  G1,G2 |- u[t/x]: B

强制您在两个前提之间拆分变量:您使用的t内容不可用u.