Constrained monads

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

s₁ >>= \ x₁ -> s₂ >>= \ x₂ -> … -> s_n >>= \ x_n -> return r

where the s_i 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