Fix和Self在构造微积分之间的确切区别是什么？

Question

依赖类型Lambda编码论文的自我类型(由Peng Fu和Aaron Stump提出)提出了自我类型,据推测,它足以在构造微积分上编码归纳原理和Scott编码数据类型,而不会使系统不一致或引入悖论.

那篇论文的符号太重了,我无法完全理解如何实现它.

究竟什么是Fix和Self的主要区别？或者,换句话说:在什么点上应该限制天真实施的Fix,以便它不会在核心演算上留下任何不一致？

Answer 1

这是我浏览论文后的理解。

一个Fix类型满足打字等价（假设 equirecursive 类型）

G |- M : Fix x. t   <=>     G |- M : t{Fix x. t / x}

即您可以在其自身上展开类型。请注意该术语M在这里没有任何作用。如果使用 isorecursive 类型，M会应用一些同构（例如 Haskell 的newtype构造函数），但这并不重要。

相反， Self 类型满足以下条件

G |- M : Self x. t   <=>     G |- M : t{M / x}

现在，x不是类型变量，而是术语变量。该术语在类型内“移动”。这根本不是递归类型。