Maths - Monad Code

How do we implement monads in computer code?

If we start with the definition of a monad as:

Then it might be natural to define the endofunctor as a mapping from type a to itself: 

endo: a -> a

where a is a type (plus we need the corresponding map for functions in a)

and the natural transformations as a mapping from the endofunctor to itself:

natTran: x:endo    => x -> x

However, cases like this, it makes sense to represent the function as a parameterised type. That is a type that depends on another type so it is a functor between types.

As we can see here 'List' and 'Maybe' are instances of
Type -> Type.

  

Idris> :type List
List : Type -> Type
Idris> :type Maybe
Maybe : Type -> Type

Idris Code

Monad m extends Applicative m which extends Functor f

from here

 
interface Functor f where
  ||| Apply a function across everything of type 'a' in a parameterised type
  ||| @ f the parameterised type
  ||| @ func the function to apply
  map : (func : a -> b) -> f a -> f b

interface Functor f => Applicative (f : Type -> Type) where
        pure  : a -> f a

interface Applicative m => Monad m where
  ||| Also called `bind`.
  (>>=) : m a -> (a -> m b) -> m b
  ||| Also called `flatten` or mu.
  join : m (m a) -> m a
  
x
  
public export
(>>) : (Monad m) => m a -> m b -> m b
a >> b = a >>= \_ => b
  
x

Implementations

Maybe is defined here. 
Monad Maybe where
  Nothing  >>= k = Nothing
  (Just x) >>= k = k x
Either is defined here. 
Monad (Either e) where
  (Left n) >>= _ = Left n
  (Right r) >>= f = f r
List is defined here. 
Monad List where
  m >>= f = concatMap f m
IO is defined here. 
Monad IO where
  b >>= k = io_bind b k

Example - List

Lets take the example of a list to see how this might work:

Here is the definition of a list in Idris: 
data List a =
  ||| Empty list
  Nil
  | ||| A non-empty list, consisting of a head element and the rest of the list.
  (::) a (List a)

This is recursive because the constuctor (::) take another list as input.

So if we take a type consisting of:

then we can consider the constructor to be an endofunctor in this type.

However the type of list is Type -> Type it would be nice to constrain it more to the above type.

  

Idris> :type List
List : Type -> Type

Now define a functor on this list:

For a list a functor is a map: 
Functor List where
  map f [] = []
  map f (x :: xs) = f x :: map f xs
  
x
  
x
  
x
  
x
  
x
  
x
  
x

 

Haskell Code

Code from here.

The 'monad' type class is an endofunctor so it can derive from Functor, its mathematical form would be somthing like this (where return represents unit and join represents mult): 

class Functor m => Monad m where
  return :: a -> m a
  join ::  m (m a) -> m a

The above is what might be expected from the mathematical definition of a monad but it is not the form that we normally see in Haskell. The first step to what is provided in haskell is to take the Kleisli algebra from our Monad: 

class Functor m => KleisliMonad m where
  return :: a -> m a
  -- | Left-to-right Kleisli composition of monads.
  (>=>) ::  (a -> m b) -> (b -> m c) -> (a -> m c)

But even this is not what we usually see, to get there we change >=> (Kleisli composition) to bind (>>=) as here: 

class  Monad m  where
    -- | Sequentially compose two actions, passing any value produced
    -- by the first as an argument to the second.
    (>>=)       :: forall a b. m a -> (a -> m b) -> m b
    -- | Sequentially compose two actions, discarding any value produced
    -- by the first, like sequencing operators (such as the semicolon)
    -- in imperative languages.
    (>>)        :: forall a b. m a -> m b -> m b
        -- Explicit for-alls so that we know what order to
        -- give type arguments when desugaring

    -- | Inject a value into the monadic type.
    return      :: a -> m a
    -- | Fail with a message.  This operation is not part of the
    -- mathematical definition of a monad, but is invoked on pattern-match
    -- failure in a @do@ expression.
    fail        :: String -> m a

    {-# INLINE (>>) #-}
    m >> k      = m >>= \_ -> k
    fail s      = error s

Note that monad does not usually derive from Functor although, mathematically speaking, we might expect it to.

Some Instances

instance Monad ((->) r) where
    return = const
    f >>= k = \ r -> k (f r) r

List monad: 

instance  Monad []  where
    m >>= k             = foldr ((++) . k) [] m
    m >> k              = foldr ((++) . (\ _ -> k)) [] m
    return x            = [x]
    fail _              = []

x

instance  Monad IO  where
    {-# INLINE return #-}
    {-# INLINE (>>)   #-}
    {-# INLINE (>>=)  #-}
    m >> k    = m >>= \ _ -> k
    return    = returnIO
    (>>=)     = bindIO
    fail s    = failIO s

x

 

x

 

Scala Code

Code from here. package scalaz

trait Pure[P[_]] {
  def pure[A](a: => A): P[A]
}

x

trait Pointed[P[_]] extends Functor[P] with Pure[P]

x

trait Apply[Z[_]] {
  def apply[A, B](f: Z[A => B], a: Z[A]): Z[B]
}

x

trait Bind[Z[_]] {
  def bind[A, B](a: Z[A], f: A => Z[B]): Z[B]
}

x

/** * Defines an applicative functor as described by McBride and Paterson in * Applicative Programming with Effects. * *

* All instances must satisfy 4 laws:

*

*/ 
trait Applicative[Z[_]] extends Pointed[Z] with Apply[Z] {
  override def fmap[A, B](fa: Z[A], f: A => B): Z[B] = this(pure(f), fa)
  override def apply[A, B](f: Z[A => B], a: Z[A]): Z[B] = liftA2(f, a, (_:A => B)(_: A))
  def liftA2[A, B, C](a: Z[A], b: Z[B], f: (A, B) => C): Z[C] = apply(fmap(a, f.curried), b)
}

/** * Abstract a model that sequences computation through an environment. * *

* All monad instances must satisfy 3 laws:

* */

trait Monad[M[_]] extends Applicative[M] with Bind[M] with Pointed[M] {
  override def fmap[A, B](fa: M[A], f: A => B) = bind(fa, (a: A) => pure(f(a)))

  override def apply[A, B](f: M[A => B], a: M[A]): M[B] = {
    lazy val fv = f
    lazy val av = a
    bind(fv, (k: A => B) => fmap(av, k(_: A)))
  }
}

x

sealed trait Kleisli[M[_], A, B] {
  def apply(a: A): M[B]

  import Scalaz._

  def >=>[C](k: Kleisli[M, B, C])(implicit b: Bind[M]): Kleisli[M, A, C] = ☆((a: A) => b.bind(this(a), k(_: B)))

  def >=>[C](k: B => M[C])(implicit b: Bind[M]): Kleisli[M, A, C] = >=>(☆(k))

  def <=<[C](k: Kleisli[M, C, A])(implicit b: Bind[M]): Kleisli[M, C, B] = k >=> this

  def <=<[C](k: C => M[A])(implicit b: Bind[M]): Kleisli[M, C, B] = ☆(k) >=> this

  def compose[N[_]](f: M[B] => N[B]): Kleisli[N, A, B] = ☆((a: A) => f(this(a)))

  def traverse[F[_], AA <: A](f: F[AA])(implicit a: Applicative[M], t: Traverse[F]): M[F[B]] =
    f ↦ (Kleisli.this(_))

  def =<<[AA <: A](a: M[AA])(implicit m: Bind[M]): M[B] = m.bind(a, apply _)
  
  def map[C](f: B => C)(implicit m: Functor[M]): Kleisli[M, A, C] =
    kleisli(a => m.fmap(apply(a), f))

  def bind[C](f: B => M[C])(implicit m: Monad[M]): Kleisli[M, A, C] =
    kleisli(a => m.bind(apply(a), f))

  def flatMap[C](f: B => Kleisli[M, A, C])(implicit m: Monad[M]): Kleisli[M, A, C] =
    kleisli(a => m.bind(apply(a), (x: B) => f(x)(a)))
}
metadata block
see also:
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.
flag flag flag flag flag flag The Princeton Companion to Mathematics - This is a big book that attempts to give a wide overview of the whole of mathematics, inevitably there are many things missing, but it gives a good insight into the history, concepts, branches, theorems and wider perspective of mathematics. It is well written and, if you are interested in maths, this is the type of book where you can open a page at random and find something interesting to read. To some extent it can be used as a reference book, although it doesn't have tables of formula for trig functions and so on, but where it is most useful is when you want to read about various topics to find out which topics are interesting and relevant to you.

 

Terminology and Notation

Specific to this page here:

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2024 Martin John Baker - All rights reserved - privacy policy.