list - 列表是单子和共子吗？

Question

列表单子在这里给出。另请参阅此处的 Spivak论文。所以 list 是一个单子。是共生体吗？你将如何证明这一点？

Answer 1

列表类型构造函数a ↦ μ L. 1 + a * L不接受共单结构。回想一下，如果它是一个comonad，我们会有（使用来自HaskellFunctor和类型类的名称Comonad）

fmap :: ∀  a b. (a → b) → [a] → [b]
extract :: ∀  a. [a] → a
duplicate :: ∀  a. [a] → [[a]]

但是，即使没有进入任何必要的法律，extract也无法实施，因为它的输入可能是空列表，无法提供a.

非空列表类型构造函数a ↦ μ NE. a + a * NE确实允许一个共单结构，extract返回第一个元素，并duplicate映射[x, y, ..., z]到[[x], [x, y], ..., [x, y, ..., z]]（请注意，它们中的每一个在构造上都是非空的）。