单子固定点不是直接限制背后的直觉是什么？

Question

考虑以下数据类型：

data Foo = Halt | Iter Foo

这是 的不动点Maybe。它包含序列、、等的直接极限，其中是注入态射。然而，有一个元素没有被直接极限覆盖，即。VoidMaybe VoidMaybe (Maybe Void)pureFoofix Iter

让我再举一个例子：

data Bar = Bar Bar Bar

这是 的不动点Complex。由于Void、Complex Void、Complex (Complex Void)等都同胚于Void，所以直接极限也Void。然而，Bar有一个元素，即fix (join Bar)。

那么这些“剩余”元素的数学依据是什么？

Answer 1

正如评论中所指出的，这些元素的存在是由于不终止的结果。

\n

在终止语言中，或者等效地，在集合范畴中， 的初始代数（最小不动点）是Maybe，( )Nat的初始代数是空类型。并且不存在，因为无法在终止语言中定义。Complexdata Complex a = Complex a aVoidfix Iterfix (join Complex)fix

\n

由于无限制的非终止，集合不再是一个好的类型模型，因为无限循环存在于所有类型中。在这种情况下，常见的替代方案是DCPO或一些类似的订单结构。特别是，递增序列的底部和极限的存在正是需要能够定义的fix（通过克莱恩定理）。例如，在 的情况下data Nat = Z | S Nat，获得作为序列, , ,等fix S的极限。\xe2\x8a\xa5S \xe2\x8a\xa5S (S \xe2\x8a\xa5)S (S (S \xe2\x8a\xa5))

\n

您确实需要小心底部的位置。例如，在 Haskell 中，是由、和Maybe a组成的 DCPO ，代表的居民。您还可以定义严格变体：\xe2\x8a\xa5NothingJust xxa

\n

data SMaybe a\n  = Nothing\n  | Just !a\n

\n

作为 DCPO 包含\xe2\x8a\xa5, Nothing，并且Just x对于的非底层x居民。特别是，序列、、等不再明确定义（或者如果你真的想给它一个值，它将始终等于），因此你不再有办法构造 、 的无限序列，实际上， 的初始代数（最小不动点）仅包含应用于/的/的有限序列，并且是单独的。a\xe2\x8a\xa5Just \xe2\x8a\xa5Just (Just \xe2\x8a\xa5)\xe2\x8a\xa5JustSMaybeJustSNothingZ\xe2\x8a\xa5

\n

请注意，这并不限于惰性语言。DCPO 也可以用来建模严格的语言。只是值和计算之间存在明确的区别，这在某种程度上使事情变得更加明显。例如ML中的选项类型

\n

type \'a option = None | Some of \'a\n

\n

None对应于由和Some xfor xin组成的值集\'a。但类型unit -> \'a option并不是从unit值到\'a option值的纯函数。unit它是一个从to 计算结果的函数\'a option。结果类型的计算表示提升类型t的元素（即，底部或 中的值）。因此，您可以将 Haskell 用作一种类型的 thunk，并以严格的语言对 Haskell 中发生的所有事情进行编码。 {\xe2\x8a\xa5} + ttunit -> _

\n