haskell - 没有 monad 转换器的 monad 的显式示例是什么？

Question

这个问题在这里已经有了答案:





Is there a monad that doesn't have a corresponding monad transformer (except IO)?

(4 个回答)


3年前关闭。




Monad 转换器以所有标准 monad(Reader、Writer、State、Cont、List 等)而闻名，但这些 monad 转换器中的每一个都以略有不同的方式工作。给定具有 monad 实例的类型构造函数的定义，没有用于构造 monad 转换器的通用方法或公式。因此，不能保证根据某些任意业务需求设计的 monad 数据类型将具有 monad 转换器。有这么明显的例子吗？

相关工作

Another question解释了两个单子(monad)的仿函数组合不一定是单子(monad)。另见 this question .这些例子并没有回答当前的问题——它们只是说明了没有构建 monad 转换器的通用方法的问题。这些例子表明，给定两个单子(monad) M 和 N，我们有时会发现 M (N a) 是单子(monad)，有时 N (M a) 是单子(monad)，有时两者都不是单子(monad)。但这既没有说明如何为 M 或 N 构造 monad 转换器，也没有说明它是否存在。

An answer to another question认为IO monad 不能有一个 monad 转换器，因为如果它有一个 IOT , 我们可以申请 IOT至 List ，然后将一个空列表( lift [] )提升到生成的 monad 中，将不得不撤消 IO monad“更早”执行的副作用。这个论点是基于 IO 的想法。 monad“实际上执行”了可能无法撤消的副作用。然而，IO monad 不是显式类型构造函数。

讨论

在每个明确给出 monad 类型的示例中，都可以以某种方式找到 monad 转换器——有时需要一定的独创性。例如，ListT Haskell 库中存在的转换器是 relatively recently发现以微妙的方式不正确，但最终通过更改 ListT 的定义解决了问题。 .

没有转换器的单子(monad)的标准示例是单子(monad)，例如 IO ，实际上不是由显式类型构造函数定义的 - IO是由库以某种方式在低级别定义的不透明“魔术”类型。显然不能定义 IO作为显式类型构造函数，具有由纯函数给出的 monad 实例。 IO示例表明，如果我们允许 monad 实例包含具有不纯副作用的隐藏低级代码，则 monad 转换器可能无法存在。因此，让我们将注意力限制在使用纯函数实现的 monad 上。

似乎没有一种算法可以从 monad 的源代码中自动推导出 monad 转换器。我们甚至知道这总是可能的吗？

为了更清楚地说明我所说的 monad 的“显式示例”是什么意思:假设我声称

 type Q u v a = ((u -> (a, Maybe a)) -> v) -> u -> (a, Maybe a)

可以有合法的 Monad相对于类型参数 a 的实例，我为 Monad 的实现生成了源代码 Q u v 的实例作为纯函数 return和 join .那么我们知道 Q u v吗？有一个 monad 转换器 QT u v使得 QT u v Id相当于 Q u v , monad 更改器(mutator)的定律成立吗？那么我们知道如何构造 QT吗？明确的？我不。

要决定这个问题，我们需要

演示一种算法，该算法可以从任意给定的类型构造函数和 monad 实例的给定实现中找到 monad 转换器；例如给定代码 type F a = r -> Either (a, a) (a, a, Maybe a)以及一个 monad 实例的实现，用于查找 monad 转换器的代码；让我们将自己限制为由 -> 的任意组合构成的类型构造函数。 、元组和 Either为简单起见；或

演示一个反例:一个显式的 monad 类型构造函数，由显式代码定义给出，例如type F a = r -> Either (a, a, a) (a, a, Maybe a)或其他什么，这样这是合法的 Monad ，带有 Monad由纯函数给出的实例，但我们可以证明 F没有单子(monad)变压器。

Answer 1

这不是答案，但对于评论来说太大了。我们可以写

{-# LANGUAGE GeneralizedNewtypeDeriving
  , DeriveFunctor #-}

import Control.Monad.Free

-- All the IO primops you could ever need
data IOF a = PutStrLn String a
           | GetLine (String -> a)
           deriving Functor

newtype MyIO a = MyIO {unMyIO :: Free IOF a}
  deriving (Functor, Applicative, Monad)

但我们实际上可以用这个来制作一个 monad 转换器:

import Control.Monad.Trans.Free

newtype IOT m a = IOT {unIOT :: FreeT IOF m a}
  deriving (Functor, Applicative, Monad, MonadTrans)

所以我什至不认为 IO被排除在外，尽管这种情况下的同构不是“内部的”。