远藤的定点有多少个值?

Question

考虑以下数据类型:

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

实质上是Endo相对于Data.Monoid的不动点。我想知道这个类型有什么值。一些例子:

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

这很快就把我们带到了一个极限点:

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

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

Answer 1

您可以从这种类型中观察到的唯一东西是不终止。

在"快速和松散"方面;推理，当你忽略非终止时，这个类型是一个单位类型(只有一个居住者/所有居住者是不可区分的)。这里的一个正式论证是，您可以在马丁-洛夫类型理论中证明，不可能存在具有同构(T -> T) <-> T和两个不同元素(x, y : T，因此x != y)的类型T。(通过对角线论证，或者更抽象地说，Lawvere的不动点定理。您可能还必须假设可确定的相等性，这可能取决于您的观点，但仍然意味着您将需要依赖一个奇特的模型来展示反例)

这意味着如果Fix Endo有什么不平凡的地方，它一定在"假装Haskell是全/类类型理论"的盲点中，也就是说，它必须涉及非终止性。

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

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

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

对EndoFix的解释基本上是对无类型lambda演算的指称语义，seq是一个额外的特性。

-- HOAS embedding of untyped lambda calculus in EndoFix
app :: EndoFix -> EndoFix -> EndoFix
lam :: (EndoFix -> EndoFix) -> EndoFix

Dana Scott在连续格中给出了一个著名的例子(在定理4.4中达到高潮)。一般的想法是将F a = a -> a视为对格/cpo的操作，并将EndoFix构造为其迭代应用F^n ∅的极限。因此，接近这个空间的一种方法是为n的小值枚举F^n ∅的居民。

另一个相关的资源是Agda中Programming Language Foundations中Untyped Lambda Calculus的指称语义一章，它给出了更具体的定义。