There are Haskell types that have an associated monad structure, but cannot be made instances of the Monad
class. The reason is typically that the return or the bind operation of such a type m
has a constraint on the type parameter of m
. As a result, all the nice library support for monads is unusable for such types. This problem is called the constrained-monad problem.
In my article The Constraint
kind, I described a solution to this problem, which involved changing the Monad
class. In this article, I present a solution that works with the standard Monad
class. This solution has been developed by Neil Sculthorpe, Jan Bracker, George Giorgidze, and Andy Gill. It is described in their paper The Constrained-Monad Problem and implemented in the constrained-normal package.
This article is a write-up of a Theory Lunch talk I gave quite some time ago. As usual, the source of this article is a literate Haskell file, which you can download, load into GHCi, and play with.
Prerequisites
We have to enable a couple of language extensions:
{-# LANGUAGE ConstraintKinds,
ExistentialQuantification,
FlexibleInstances,
GADTSyntax,
Rank2Types #-}
Furthermore, we need to import some modules:
import Data.Set hiding (fold, map)
import Data.Natural hiding (fold)
These imports require the packages containers and natural-numbers to be installed.
The set monad
The Set
type has an associated monad structure, consisting of a return and a bind operation:
returnSet :: a -> Set a
returnSet = singleton
bindSet :: Ord b => Set a -> (a -> Set b) -> Set b
bindSet sa g = unions (map g (toList sa))
We cannot make Set
an instance of Monad
though, since bindSet
has an Ord
constraint on the element type of the result set, which is caused by the use of unions
.
For a solution, let us first look at how monadic computations on sets would be expressed if Set
was an instance of Monad
. A monadic expression would be built from non-monadic expressions and applications of return
and (>>=)
. For every such expression, there would be a normal form of the shape
s1 >>= \
x1 ->
s2 >>= \
x2 ->
… ->
sn >>= \
xn -> return
r
where the si would be non-monadic expressions of type Set
. The existence of a normal form would follow from the monad laws.
We define a type UniSet
of such normal forms:
data UniSet a where
ReturnSet :: a -> UniSet a
AtmBindSet :: Set a -> (a -> UniSet b) -> UniSet b
We can make UniSet
an instance of Monad
where the monad operations build expressions and normalize them on the fly:
instance Monad UniSet where
return a = ReturnSet a
ReturnSet a >>= f = f a
AtmBindSet sa h >>= f = AtmBindSet sa h' where
h' a = h a >>= f
Note that these monad operations are analogous to operations on lists, with return
corresponding to singleton construction and (>>=)
corresponding to concatenation. Normalization happens in (>>=)
by applying the left-identity and the associativity law for monads.
We can use UniSet
as an alternative set type, representing a set by a normal form that evaluates to this set. This way, we get a set type that is an instance of Monad
. For this to be sane, we have to hide the data constructors of UniSet
, so that different normal forms that evaluate to the same set cannot be distinguished.
Now we need functions that convert between Set
and UniSet
. Conversion from Set
to UniSet
is simple:
toUniSet :: Set a -> UniSet a
toUniSet sa = AtmBindSet sa ReturnSet
Conversion from UniSet
to Set
is expression evaluation:
fromUniSet :: Ord a => UniSet a -> Set a
fromUniSet (ReturnSet a) = returnSet a
fromUniSet (AtmBindSet sa h) = bindSet sa g where
g a = fromUniSet (h a)
The type of fromUniSet
constrains the element type to be an instance of Ord
. This single constraint is enough to make all invocations of bindSet
throughout the conversion legal. The reason is our use of normal forms. Since normal forms are “right-leaning”, all applications of (>>=)
in them have the same result type as the whole expression.
The multiset monad
Let us now look at a different monad, the multiset monad.
We represent a multiset as a function that maps each value of the element type to its multiplicity in the multiset, with a multiplicity of zero denoting absence of this value:
newtype MSet a = MSet { mult :: a -> Natural }
Now we define the return operation:
returnMSet :: Eq a => a -> MSet a
returnMSet a = MSet ma where
ma b | a == b = 1
| otherwise = 0
For defining the bind operation, we need to define a class Finite
of finite types whose sole method enumerates all the values of the respective type:
class Finite a where
values :: [a]
The implementation of the bind operation is as follows:
bindMSet :: Finite a => MSet a -> (a -> MSet b) -> MSet b
bindMSet msa g = MSet mb where
mb b = sum [mult msa a * mult (g a) b | a <- values]
Note that the multiset monad differs from the set monad in its use of constraints. The set monad imposes a constraint on the result element type of bind, while the multiset monad imposes a constraint on the first argument element type of bind and another constraint on the result element type of return.
Like in the case of sets, we define a type of monadic normal forms:
data UniMSet a where
ReturnMSet :: a -> UniMSet a
AtmBindMSet :: Finite a =>
MSet a -> (a -> UniMSet b) -> UniMSet b
The key difference to UniSet
is that UniMSet
involves the constraint of the bind operation, so that normal forms must respect this constraint. Without this restriction, it would not be possible to evaluate normal forms later.
The Monad
–UniMSet
instance declaration is analogous to the Monad
–UniSet
instance declaration:
instance Monad UniMSet where
return a = ReturnMSet a
ReturnMSet a >>= f = f a
AtmBindMSet msa h >>= f = AtmBindMSet msa h' where
h' a = h a >>= f
Now we define conversion from MSet
to UniMSet
:
toUniMSet :: Finite a => MSet a -> UniMSet a
toUniMSet msa = AtmBindMSet msa ReturnMSet
Note that we need to constrain the element type in order to fulfill the constraint incorporated into the UniMSet
type.
Finally, we define conversion from UniMSet
to MSet
:
fromUniMSet :: Eq a => UniMSet a -> MSet a
fromUniMSet (ReturnMSet a) = returnMSet a
fromUniMSet (AtmBindMSet msa h) = bindMSet msa g where
g a = fromUniMSet (h a)
Here we need to impose an Eq
constraint on the element type. Note that this single constraint is enough to make all invocations of returnMSet
throughout the conversion legal. The reason is again our use of normal forms.
A generic solution
The solutions to the constrained-monad problem for sets and multisets are very similar. It is certainly not good if we have to write almost the same code for every new constrained monad that we want to make accessible via the Monad
class. Therefore, we define a generic type that covers all such monads:
data UniMonad c t a where
Return :: a -> UniMonad c t a
AtmBind :: c a =>
t a -> (a -> UniMonad c t b) -> UniMonad c t b
The parameter t
of UniMonad
is the underlying data type, like Set
or MSet
, and the parameter c
is the constraint that has to be imposed on the type parameter of the first argument of the bind operation.
For every c
and t
, we make UniMonad c t
an instance of Monad
:
instance Monad (UniMonad c t) where
return a = Return a
Return a >>= f = f a
AtmBind ta h >>= f = AtmBind ta h' where
h' a = h a >>= f
We define a function lift
that converts from the underlying data type to UniMonad
and thus generalizes toUniSet
and toUniMSet
:
lift :: c a => t a -> UniMonad c t a
lift ta = AtmBind ta Return
Evaluation of normal forms is just folding with the return and bind operations of the underlying data type. Therefore, we implement a fold operator for UniMonad
:
fold :: (a -> r)
-> (forall a . c a => t a -> (a -> r) -> r)
-> UniMonad c t a
-> r
fold return _ (Return a) = return a
fold return atmBind (AtmBind ta h) = atmBind ta g where
g a = fold return atmBind (h a)
Note that fold
does not need to deal with constraints, neither with constraints on the result type parameter of return (like Eq
in the case of MSet
), nor with constraints on the result type parameter of bind (like Ord
in the case of Set
). This is because fold
works with any result type r
.
Now let us implement Monad
-compatible sets and multisets based on UniMonad
.
In the case of sets, we face the problem that UniMonad
takes a constraint for the type parameter of the first bind argument, but bindSet
does not have such a constraint. To solve this issue, we introduce a type class Unconstrained
of which every type is an instance:
class Unconstrained a
instance Unconstrained a
The implementation of Monad
-compatible sets is now straightforward:
type UniMonadSet = UniMonad Unconstrained Set
toUniMonadSet :: Set a -> UniMonadSet a
toUniMonadSet = lift
fromUniMonadSet :: Ord a => UniMonadSet a -> Set a
fromUniMonadSet = fold returnSet bindSet
The implementation of Monad
-compatible multisets does not need any utility definitions, but can be given right away:
type UniMonadMSet = UniMonad Finite MSet
toUniMonadMSet :: Finite a => MSet a -> UniMonadMSet a
toUniMonadMSet = lift
fromUniMonadMSet :: Eq a => UniMonadMSet a -> MSet a
fromUniMonadMSet = fold returnMSet bindMSet