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

Question

Self Types for Dependently Typed Lambda Encodings论文(由 Peng Fu 和 Aaron Stump 撰写)提出了自我类型，据说它们足以编码归纳原理和 Scott-encoded Calculus of Constructions 上的数据类型，而不会使系统不一致或引入悖论。

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

确切地说，Fix 和 Self 的主要区别是什么？或者，换句话说:一个天真的实现的修复应该在哪些方面受到限制，这样它就不会在核心计算上留下不一致的地方？

Answer 1

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

一个 Fix type 满足打字等价(假设等递归类型)

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

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

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

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

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