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?
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?
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}
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With