什么是没有monad变换器的monad的明确例子？ [英] What is an explicit example of a monad without a monad transformer?

问题描述

Monad变压器以所有标准单声道（读卡器，作者，状态，连续，列表等）而闻名，但这些单声道变压器中的每一个都以稍微不同的方式工作。没有通用的方法或公式来构造monad变换器，只要给出一个具有monad实例的类型构造函数的定义。因此，不能确定根据某些任意业务需求设计的monad数据类型将具有monad变换器。有没有这样一个明确的例子？

相关工作

另一个问题解释说，两个单子的函数组合不一定是单子。另请参阅此问题 。这些例子并没有回答目前的问题 - 它们只是说明了没有通用的方法来构建monad变压器的问题。这些例子表明，给定两个单子M和N，我们有时会发现M（N a）是一个monad，有时N（M a）是一个单子，有时也不会是单子。但是这并没有说明如何为M或N构建monad变换器，也不显示它是否存在。 question / 11792275 / is-access-to-the-internal-structure-of-monad-mon-one-one-monad-transformer>对另一个问题的回答认为 IO monad 不能具有monad转换器，因为如果它有一个 IOT ，我们可以应用 IOT 到 List ，然后解除一个空列表（ lift [] ）到由此产生的monad将不得不撤销IO monad较早执行的副作用。这个论点是基于这样的想法： IO monad实际上执行可能无法撤销的副作用。但是， IO monad不是显式类型的构造函数。

讨论

在每一个显式给出monad类型的例子中，monad变换器都可以找到 ，有时需要一定的独创性。例如，存在于Haskell库中的 ListT 转换器是相对来说最近的发现微妙地不正确，但问题最终通过改变 ListT 的定义来解决。

没有变换器的monad的标准示例是monad，如 IO ，它实际上并未由显式类型构造函数定义 - IO 是低级别的 定义的不透明的魔术类型。看起来很清楚，一个不能将 IO 定义为显式类型构造函数，而monad实例提供了monad实例。 IO 示例显示，如果我们允许monad实例包含带有不纯副作用的隐藏低级代码，则monad转换器可能无法存在。因此，让我们将注意力集中在使用纯函数实现monad上。

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

为了更清楚地说明一个monad的明确例子是什么意思：假设我声称

  type Q uva =（（u  - >（a，Maybe a）） - > v） - > u  - > （a，也许a）
  

可以有合法的 Monad c> a 类型参数的实例，我生成了 Monad 的实现的源代码。 Q uv 作为纯函数 return 和 join 的实例。然后，我们知道 Q uv 具有单变量变换 QT uv ，使得 QT uv Id 相当于 Q uv ，单变换器的定律是否成立？那么我们是否知道如何明确地构造 QT ？我不需要。

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

• 演示一个算法，该算法可以从任意给定类型的构造函数和monad实例的给定实现中找到monad变换器;例如给定代码键入F a = r - >或者（a，a）（a，a，Maybe a），并为此实现一个monad实例，以找到monad变换器的代码;为了简单起见，让我们限制自己使用 - >> ，tuple和两者的任意组合来构造构造器。或


• 来演示一个反例：由显式代码定义给出的显式 monad类型构造函数。 键入F a = r - >或者（a，a，a）（a，a，Maybe a）或其他，这是合法的 Monad ，其中 Monad 由纯函数给出的实例，但我们可以证明 F 没有monad变换。

解决方案

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

  { - ＃LANGUAGE GeneralizedNewtypeDeriving 
，DeriveFunctor＃ - } 
 
 import Control.Monad.Free 
 
  - 您可能需要的所有IO primops 
数据IOF a = PutStrLn String a 
 | GetLine（String  - > a）
派生Functor 
 
 newtype MyIO a = MyIO {unMyIO :: Free IOF a} 
派生（Functor，Applicative，Monad）
  

但是我们实际上可以使用monad变换器：

  import Control.Monad.Trans.Free 
 
 newtype IOT ma = IOT {unIOT :: FreeT IOF ma} 
派生（Functor，Applicative ，Monad，MonadTrans）
  

所以我不认为即使 IO 被排除，虽然在这种情况下的同构不是内部。

Monad transformers are known for all standard monads (Reader, Writer, State, Cont, List, etc.), but each of these monad transformers works in a slightly different way. There is no general method or formula for constructing a monad transformer given a definition of a type constructor with a monad instance. So, it is not assured that a monad data type designed according to some arbitrary business requirements will have a monad transformer. Is there such an explicit example?

Related work

Another question explains that a functor composition of two monads is not necessarily a monad. See also this question. Those examples do not answer the present question - they merely illustrate the problem of having no general method for constructing a monad transformer. Those examples show that, given two monads M and N, we will sometimes find that M (N a) is a monad, sometimes that N (M a) is a monad, and sometimes neither will be a monad. But this shows neither how to construct a monad transformer for M or N, nor whether it exists at all.

An answer to another question argues that the IO monad cannot have a monad transformer because if it had one IOT, we could apply IOT to List, and then lifting an empty list (lift []) into the resulting monad would have to undo the side effects performed "earlier" by the IO monad. This argument is based on the idea that the IO monad "actually performs" side effects that, presumably, cannot be undone. However, the IO monad is not an explicit type constructor.

Discussion

In every example where a monad type is given explicitly, a monad transformer could be found somehow, - sometimes with certain ingenuity required. For example, the ListT transformer that existed in the Haskell library was relatively recently found to be incorrect in a subtle way, but the problem was eventually fixed by changing the definition of ListT.

Standard examples of monads without transformers are monads such as IO, which is actually not defined by an explicit type constructor - IO is an opaque "magic" type defined by the library somehow, at low level. It seems clear that one cannot define IO as an explicit type constructor, with a monad instance given by pure functions. The IO example shows that a monad transformer may fail to exist if we allow the monad instance to contain hidden low-level code with impure side effects. So, let us limit our attention to monads implemented using pure functions.

There does not seem to be an algorithm that would derive monad transformers automatically from the monad's source code. Do we even know that this is always possible?

To make it more clear what I mean by an "explicit example" of a monad: Suppose I claim that

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

can have a lawful Monad instance with respect to the type parameter a, and I produce the source code for an implementation of the Monad instance for Q u v as pure functions return and join. Do we then know that Q u v has a monad transformer QT u v such that QT u v Id is equivalent to Q u v, and the laws of the monad transformers hold? Do we then know how to construct QT explicitly? I don't.

To decide this question, we need either

• to demonstrate an algorithm that would find a monad transformer from an arbitrary given type constructor and a given implementation of a monad instance; e.g. given the code type F a = r -> Either (a, a) (a, a, Maybe a) and an implementation of a monad instance for this, to find the code for the monad transformer; let's limit ourselves to type constructors made out of any combination of ->, tuple, and Either for simplicity; or
• to demonstrate a counterexample: an explicit monad type constructor, given by an explicit code definition, e.g. type F a = r -> Either (a, a, a) (a, a, Maybe a) or whatever, such that this is a lawful Monad, with a Monad instance given by pure functions, but we can prove that F has no monad transformer.

解决方案

This isn't an answer, but it's way too big for a comment. We can write

{-# 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)

But we can actually make a monad transformer out of this:

import Control.Monad.Trans.Free

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

So I don't really think even IO is excluded, although the isomorphism in that case is not "internal".

这篇关于什么是没有monad变换器的monad的明确例子？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！