用 Free 编写 Identity monad答案

【问题标题】：Writing the Identity monad in terms of Free用 Free 编写 Identity monad
【发布时间】：2015-09-22 04:42:10
【问题描述】：

在“点菜数据类型”中，Swierstra 写道，给定 Free（他称之为 Term）和 Zero，您可以实现 Identity monad：

data Term f a = Pure a
              | Impure (f (Term f a))
data Zero a

Term Zero 现在是 Identity monad。我明白为什么会这样。问题是我永远不能使用 Term Zero 作为 Monad 因为讨厌的 Functor f => 约束：

instance Functor f => Monad (Term f) where
    return x = Pure x
    (Pure x) >>= f = f x 
    (Impure f) >>= t = Impure (fmap (>>=f) t)

如何使Zero 成为 Functor？

instance Functor Zero where
    fmap f z = ???

这里似乎有一个技巧：由于Zero 没有构造函数，因此永远无法使用Impure，因此永远不会调用>>= 的Impure 案例。这意味着 fmap 永远不会被调用，所以从某种意义上说这是可以的：

instance Functor Zero where
    fmap f z = undefined

问题是，这感觉像是在作弊。我错过了什么？ Zero 真的是 Functor 吗？又或许Zero 不是Functor，这是我们在Haskell 中表达Free 的一个缺点？

【问题讨论】：

是的，Zero 是从Hask 到0 的函子，空类别（然后被嵌入回Hask）。

标签： haskell monads free-monad

【解决方案1】：

如果你打开DeriveFunctor，你可以写

data Zero a deriving Functor

但您可能会认为这是作弊。如果你想自己写，你可以打开EmptyCase，而不是，然后写时髦的

instance Functor Zero where
    fmap f z = case z of

【讨论】：

我想知道如果我们在这两个仿函数实例中作弊并执行fmap f _|_ 会发生什么。在 GHCi 7.10.2 中，第一个实例错误为Exception: Void fmap，没有尝试评估底部，而第二个实例确实评估了它。我本来预计会出现非详尽性错误。并不是说这真的很重要——这两种情况都很好，尽管如果我们超过一个，它们会产生不同的底部。
@chi 你绝对不应该期待一个非穷举错误：这些模式匹配是穷举！
我以某种方式期待case e of p1 -> e1 ; .. ; pn -> en 和case e of ... ; pn -> en ; _ -> error "non exhaustive" 之间的实际等效性。这种“幕后”等价仅在 n=0 时中断（如果我们不识别“不同”底部）。关于详尽无遗……我会更相信 Agda/Coq 或任何其他完整的编程语言。在 Haskell 中，您是对的，但底部是奇怪的野兽，从操作上讲，我不清楚 case _|_ :: Void of {} 是否应该评估参数。

【解决方案2】：

定义Zero a的技巧如下。

newtype Zero a = Zero (Zero a)

换句话说，它编码了一种愚蠢的、有点不明显的陈述，即实际上有一种方法可以获得Zero a的值：你一定已经有了！

有了这个定义，absurd :: Zero a -> b 就可以“自然”地定义了

absurd :: Zero a -> b
absurd (Zero z) = absurd z

在某种意义上，这些定义都是合法的，因为它们准确地指出了它们是如何无法实例化的。除非有人先“作弊”，否则不能构造 Zero a 的值。

instance Functor Zero where
  fmap f = absurd

【讨论】：

值得指出的是，这或多或少是Data.Void模块的实现方式。
哈，是的，没错！
Data.Void 曾经这样做，在EmptyCase 出现之前（它从void 移动到base 时发生了变化）。我不知道它是否出于清晰、效率或错误报告的原因而改变。你呢？
@dfeuer：哦，我没有注意到 base 现在有 Void（从 4.8.0.0 开始）。请注意，旧的void 包将自己宣传为“Haskell 98 逻辑上无人居住的数据类型”；这就是这个答案技巧的原点。

【解决方案3】：

解决此问题的一种方法是使用 Data.Void 而不是空的 data 声明，如下所示：

import Data.Void

-- `Zero a` is isomorphic to `Void`
newtype Zero a = Zero Void

instance Functor Zero where
    -- You can promise anything if the precondition is that
    -- somebody's gotta give you an `x :: Void`.
    fmap f (Zero x) = absurd x

请参阅 this question 以获得对 Void 有用的一些非常好的解释。但关键的想法是absurd :: Void -> a 函数可以让你从永远不会发生的x :: Void 绑定变成你喜欢的任何类型。

【讨论】：

【解决方案4】：

Luis Casillas 的 answer 的另一个变化是完全使用库存零件构建您的类型：

type Id = Free (Const Void)

Const x 的 Functor 实例将按您的意愿工作（它的 fmap 不做任何事情，这很好），您只需要在打开包装时小心：

runId (Pure x) = x
runId (Free (Const ab)) = absurd ab

当然，所有这些都只是“道德上”等同于Identity，因为它们都引入了额外的价值。特别是，我们可以区分

bottom
Pure bottom
Free bottom

【讨论】：