类型构造器`Maybe (BTree a)`是monad吗？

Question

问题

像这样在 Haskell 中定义类型构造函数

F

：

 data BTree a = Leaf a | Branch (BTree a) (BTree a)
 data F a = F (Maybe (BTree a))

类型构造函数

F

是多项式的，所以它是一个

Functor

，一个

Applicative

，一个

Traversable

，但显然不是一个

Monad

。

我们能否为

bind

实现

return

和

F

以满足单子法则，从而使

F

成为单子？或者那是不可能的？

动机

这个问题的动机是

F

是一种特殊数据结构的生成器。即，某些

F

-代数是可能违反结合律的幺半群。更严格地说，类型

F t

是由类型

t

生成的不完全幺半群类别中的初始对象，可能违反结合律。

看看为什么：

首先，我们可以在

F a

上定义类似幺半群的操作。空元素是

F Nothing

，二元运算将两个值放入树的分支中，除非其中一个值是空的。

其次，假设类型

T

是一个

F

-代数，所以我们有

h: F T -> T

。这意味着我们有

h(F Nothing)

，它是

T

类型的值，用作幺半群的空值，并且我们有一个由

(T, T) -> T

定义的二元运算

\(x,y) -> h(F(Just(Branch(Leaf x) (Leaf y))))

。此外，假设

h

保留幺半群运算，那么

h

也将保留恒等律。所以，

T

是一个不完全的幺半群，它满足恒等律（但可能违反结合律）。

F

看起来像树单子

BTree(Maybe a)

由幺半群的身份法则分解，尽管我没有从中推导出

F

的正式方法。

通常的民间传说知识是

F

-algebras with laws需要用monad代数来描述。但是，如果

F

不是单子，那么那是不正确的。需要以更一般的方式描述类型类法则。

但主要问题是：我们可以将

F

变成 monad 吗？

Answer 1

F

确实是一个单子。鉴于它是

Maybe

与

BTree

的组合，两者都是单子且

BTree

是可遍历的，我们可以暂时使用内部组合转换器实例使其成为单子：

{-# LANGUAGE GHC2021 #-}
import Control.Monad (join, ap)

newtype F a = F { runF :: Maybe (BTree a) }
    deriving (Eq, Show, Ord, Functor, Foldable, Traversable)

instance Monad F where
    m >>= f = F
        $ fmap (join @BTree) . join @Maybe . fmap (sequenceA @BTree)
        $ runF $ runF . f <$> m

instance Applicative F where
    pure = F . pure @Maybe . pure @BTree
    (<*>) = ap

data BTree a = Leaf a | Branch (BTree a) (BTree a)
    deriving (Eq, Show, Ord, Functor, Foldable, Traversable)

instance Monad BTree where
    Leaf a >>= f = f a
    Branch la ra >>= f = Branch (la >>= f) (ra >>= f)

instance Applicative BTree where
    pure = Leaf
    (<*>) = ap

有关此变压器构造的详细信息，请参阅我对Do monad transformers, generally speaking, arise out of adjunctions? 特别是，该部分指出了两个上述

Monad F

实例必须满足的条件才是合法的。首先，

join @Maybe

必须保留

(<*>)

，即：

join' :: Monad m => Compose m m a -> m a
join' = join . getCompose

mmf :: Compose Maybe Maybe (a -> b)
mma :: Compose Maybe Maybe a

join' (mmf <*> mma) = join' mmf <*> join' mma

这个等式两侧的区别归结为

mmf

和

mma

的影响顺序。由于

Maybe

是交换单子，所以这无关紧要，条件成立。

其次，

join @BTree

必须保留

toList

，即：

bba :: Compose BTree BTree a

toList bba = toList (join' bba)

由于

BTree

是一个自由单子（属于齐次对函子），它的

join

除了嫁接树以移除嵌套之外什么都不做，从

toList

的角度来看没有元素的重新排列。既然如此，第二个条件也成立，因此

F

是一个单子。