Endo 的固定点有多少个值？

Question

考虑以下数据类型：

newtype EndoFix = EndoFix {appEndoFix :: EndoFix -> EndoFix}

Endo这本质上是from的固定点Data.Monoid。我想知道这种类型有什么价值。一些例子：

example0 = EndoFix id
example1 = EndoFix (const example0)
example2 = EndoFix (const example1)

这很快就把我们引向了一个极限点：

import Data.Function
exampleOmega = fix (EndoFix . const)

但是，我找不到任何区分这些值的半决策过程。我的直觉告诉我没有，这意味着这些值实际上都是相等的。那么 所表达的实际拓扑空间是什么呢EndoFix？

Answer 1

从这种类型中你可以观察到的唯一事情就是不终止。

\n

就“快速而宽松”的推理而言，如果忽略非终止性，这种类型是一种单元类型（只有一个居民/所有居民是无法区分的）。T这里的一个正式论证是，您可以在 Martin-Lof 类型理论中证明，不可能存在具有同构(T -> T) <-> T和两个不同元素的类型（ x, y : T，使得x != y）。（通过对角论证，或更抽象地，劳维尔不动点定理。您可能还必须假设可判定的相等性，这可能非常强，具体取决于您的观点，但仍然意味着您需要依赖展示反例的奇特模型）

\n

这意味着，如果有什么不平凡的事情Fix Endo，它一定处于“假装 Haskell 是完全/类似类型理论”的盲点，即它必须涉及非终止。

\n

我们可以通过向它们传递一些未定义的参数并强制它们来区分example0, example1, 和example2。

\n

-- force1 example0 = _|_\n-- force1 example1 = () \nforce1 :: EndoFix -> ()\nforce1 f = (f `appEndoFix` undefined) `seq` ()\n\n-- force2 example1 = _|_\n-- force2 example2 = ()\nforce2 :: EndoFix -> ()\nforce2 f = ((f `appEndoFix` undefined) `appEndoFix` undefined) `seq` ()\n

\n

使用这个想法，您可以定义无限多个可区分的函数：至少有那些接受 n 个参数并返回第 i 个参数的函数。

\n

的解释EndoFix基本上是无类型 lambda 演算的指称语义，并seq作为一个额外的功能。

\n

-- HOAS embedding of untyped lambda calculus in EndoFix\napp :: EndoFix -> EndoFix -> EndoFix\nlam :: (EndoFix -> EndoFix) -> EndoFix\n

\n

Dana Scott 在Continuous Lattices（定理 4.4 中的高潮）中给出了一个著名的例子。总体思想是将其视为F a = a -> a格/CPO 上的操作，并构造EndoFix为其迭代应用的极限F^n \xe2\x88\x85。因此，处理这个空间的一种方法是枚举 的F^n \xe2\x88\x85较小值的居民n。

\n

另一个相关资源是《Agda 编程语言基础》中关于非类型化 Lambda 演算的指称语义的章节，它给出了更具体的定义。

\n