Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Is the type constructor `Maybe (BTree a)` a monad?

Question

Define the type constructor F in Haskell like this:

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

The type constructor F is polynomial, so it is a Functor, an Applicative, a Traversable, but not obviously a Monad.

Can we implement bind and return for F that satisfy the monad laws and thus make F into a monad? Or is that impossible?

Motivation

The question is motivated by the fact that F is a generator of data structures of a special kind. Namely, certain F-algebras are monoids that may violate the associativity law. More rigorously, the type F t is an initial object in the category of not-quite-monoids generated by type t that may violate the associativity law.

To see why:

First, we can define the monoid-like operations on F a. The empty element is F Nothing and the binary operation puts two values into the branches of a tree unless one of the values is empty.

Second, suppose the type T is an F-algebra, so we have h: F T -> T. This means we have h(F Nothing), which is a value of type T that serves as the empty value of the monoid, and we have a binary operation (T, T) -> T defined by \(x,y) -> h(F(Just(Branch(Leaf x) (Leaf y)))). Further, suppose that h preserves the monoid operations, then h will also preserve the identity laws. So, T is a not-quite-monoid that satisfies the identity laws (but may violate the associativity law).

F looks like the tree monad BTree(Maybe a) factored by the identity laws of a monoid, although I don't have a formal way of deriving F from that.

The usual folklore knowledge is that F-algebras with laws need to be described via monad algebras. But if F is not a monad then that is not true. The typeclass laws need to be described in a more general way.

But the main question is: can we make F into a monad?

like image 784
winitzki Avatar asked Oct 19 '25 05:10

winitzki


1 Answers

F is indeed a monad. Given that it is the composition of Maybe with BTree, with both being monads and BTree being traversable, we can tentatively make it a monad using the composed-on-the-inside transformer instance:

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

For details on this transformer construction, see the "Flipped transformers and the Eilenberg-Moore adjunction" section of my answer to Do monad transformers, generally speaking, arise out of adjunctions? In particular, that section points out there two conditions which must hold for the Monad F instance above to be lawful. Firstly, join @Maybe must preserve (<*>), that is:

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

The difference between the two sides of this equation boils down to the order in which the effects from mmf and mma are sequenced. Since Maybe is a commutative monad, that doesn't matter, and the condition holds.

Secondly, join @BTree must preserve toList, that is:

bba :: Compose BTree BTree a

toList bba = toList (join' bba)

Since BTree is a free monad (of the homogeneous pair functor), its join does nothing but grafting trees to remove the nesting, with no rearrangement of elements from the point of view of toList. That being so, this second condition holds as well, and therefore F is a monad.

P.S.: Regarding n. m.'s question in the comments:

Say you have F(Just (Branch (F(Just (Leaf 42))), F Nothing), what the result should be?

The core part of the (>>=) definition, which amounts to join sans the boilerplate, is:

fmap (join @BTree) . join @Maybe . fmap (sequenceA @BTree)

From that, we can tell that join will behave as in BTree if all Maybe values are Just in F (F a). If there is a Nothing anywhere, though, the result will be Nothing, as sequenceA and join @Maybe will propagate failure:

ghci> join $ F (Just (Branch (Leaf (F (Just (Leaf 42)))) (Leaf (F Nothing))))
F {runF = Nothing}
like image 130
duplode Avatar answered Oct 22 '25 04:10

duplode



Donate For Us

If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!