I originally put this on AxiomWiki created by Bill Page but since that has disappeared I moved it here.

**Bertfried Fauser** wrote:

investigate myself. Such things can be implemented very efficiently

Formal definition

If C is a category, a monad on C consists of a functor $T \colon C \to C$ together with two natural transformations: $\eta \colon 1_{C} \to T$ (where $1_C$ denotes the identity functor on C) and $\mu \colon T^{2} \to T$ (where $T^2$ is the functor $T \circ T$ from C to C). These are required to fulfill the following conditions (sometimes called coherence conditions):

\begin{eqnarray}
\mu \circ T\mu = & \mu \circ \mu T & \textrm{(as natural transformations } T^{3} \to T); \\
\mu \circ T \eta = & \mu \circ \eta T = 1_{T} & \textrm{(as natural transformations } T \to T; \\
& & \textrm{here } 1_T \textrm{ denotes the identity transformation from T to T).}
\end{eqnarray}
We can rewrite these conditions using following commutative diagrams:
\begin{latex}
\begin{tabular}{lcr}
\xymatrix{
& T^3\ar[r]^{T\mu}\ar[d]_{\mu T}&T^2\ar[d]^{\mu}\\
& T^2\ar[r]_{\mu}&T
} &
\xymatrix{
& \ar@{=}[dr]T\ar[r]^{\eta T}\ar[d]_{T\eta}&T^2\ar[d]^{\mu}\\
& T^2\ar[r]_{\mu}&T
}
\end{tabular}
\end{latex}

On Fri, Nov 4, 2011 at 5:04 AM, **Martin Baker** wrote:

its not really what we are talking about here?

I have been thinking about what it would take to implement a monad in
SPAD, I have been doing this by taking 'List' as being an example of a
monad and then trying to generalize it.

$\mu$ = 'concat', $\eta$ = 'list', and $T$ = [ ].

Here T and $\eta$ are effectively the same but I've used a different
form 'list' and [ ] to distinguish between them. They are the same,
in this case, because we are working in terms of components. It would
be good to also be able to work in terms of functors and natural
transformations, Haskell would do this because of automatic currying

So I will check that the identities for monads are satisfied.

First something to work with:
\begin{axiom}
T2a := [[A],[B]]
T2b := [[C],[D]]
\end{axiom}
then test associative square:
\begin{axiom}
concat[concat T2a,concat T2b] = concat(concat[T2a,T2b])
\end{axiom}
then test unit triangles:
\begin{axiom}
concat(list[A]) = [A]
concat[list A] = [A]
\end{axiom}
So this seems to have the properties needed, I would like to build a

example of how it could be coded?

In Haskell the monads in the prelude is in a different form as its
purpose is to allow impure code to be wrapped in pure code. I have
modified the Monad definition in the prelude to have a more category
theoretic form as follows::

unit :: a -> m a -- usually called 'return' in Haskell
mult :: m (m a) -> m a -- usually called 'join' in Haskell

How could we write this as an SPAD category? I've tried to do a direct
(except I have changed 'm' to 'T' to give a more mathematical
notation:

MonadCat(A:Type,T: Type) : Category == with
unit :A -> T A
mult :T ( T A) -> T A

It compiles but it doesn't look very useful? Everything is just a
general type so there isn't any proper type checking and I would like
the category to have some internal type structure so that we can
relate it to the external functors and natural transformations.

There are two axiom-categories that we need to define:

- T

We can think of T as being an endofunctor on 'MonadCat' but also we want
to turn things around by defining 'MonadCat' in terms of T, that is we
start with a base 'type' and extend it by repeatedly applying T to it.

So we want to define T as an endofunctor:
$$T:\textrm{MonadCat}-> \textrm{MonadCat}$$
But we also want to define T as a axiom-category which can be extended
to domains which can then define our monad, for instance, if we want
to define a list-monad (monad for a monoid) then we start by defining
a list-t like this::

TList(A:Type) : Exports == Implementation where
...
Rep := List A

we can then define the list monad as::

MonadList(A:Type,T:TList Type) : Exports == Implementation where
...
Rep := Union(T A,T %)

Here is the code to represent the T ''endofunctor'' for a list which we
want to generate a list monad.
)abbrev domain TLIST TList
TList(A:Type) : Exports == Implementation where
Exports == CoercibleTo(OutputForm) with

a:(a:List A) -> %
toList:(a:%) -> List A
baseType:(a:%) -> Type

Rep := PrimitiveArray A

a(a:List A):% == construct(a)$(PrimitiveArray A) toList(a:%):List A == entries(a::Rep)$(PrimitiveArray A)

baseType(a:%):Type == A

coerce(n: %):OutputForm ==
e := entries(n)
if #e=1 then
if A has CoercibleTo(OutputForm) then
return (first e)::OutputForm
return e::OutputForm

We then use this to 'generate' a list monad:
MonadList(A:Type) : Exports == Implementation where
Exports == CoercibleTo(OutputForm) with

t:(inpu:TList(%)) -> %
t:(inpu:List(%)) -> %
unit:(inpu:TList(A)) -> %
unit:(inpu:List(A)) -> %
unit:(inpu:A) -> %
mult:(inpu:%) -> %

Rep := Union(leaf:TList(A),branch:TList(%))
++ holds type of T A, T T A or T T T A...

t(inpu:TList(%)):% ==
[inpu]

t(inpu:List(%)):% ==
[a(inpu)$TList(%)] unit(inpu:TList(A)):% == [inpu] unit(inpu:List(A)):% == [a(inpu)$TList(A)]

unit(inpu:A):% ==
[a([inpu])$TList(A)] mult(inpu:%):% == if inpu case leaf then error "cannot apply mult here" lst:List % := toList(inpu.branch) lst2:List List % := [toList(a.branch) for a in lst] lst3 := concat(lst2) [a(lst3)$TList(%)]

coerce(n: %):OutputForm ==
if n case leaf
then
e := toList(n.leaf)
if #e=1 then
if A has CoercibleTo(OutputForm) then
return (first e)::OutputForm
return e::OutputForm
else
lst:List % := toList(n.branch)
lst2 := [a::%::OutputForm for a in lst]
if #lst2 = 1 then
return hconcat("T "::OutputForm,(first lst2)::OutputForm)
return hconcat("T "::OutputForm,lst2::OutputForm)

It might be better expressed if we had dependant variables but I think
we can do it this way:
\begin{axiom}
T2a := t[t[unit[A::Symbol]],t[unit[B::Symbol]]]
T2b := t[t[unit[C::Symbol]],t[unit[D::Symbol]]]
\end{axiom}
Going one way round the associativity square gives:
\begin{axiom}
mult(t[mult T2a,mult T2b])
\end{axiom}
Going the other way round the associativity square gives the same
result:
\begin{axiom}
mult(mult(t[T2a,T2b]))
\end{axiom}
Also the identity triangle:
\begin{axiom}
mult(t[t[unit[A::Symbol]]])
\end{axiom}

From MartinBaker Sat Nov 5 03:02:52 -0700 2011
From: Martin Baker
Date: Sat, 05 Nov 2011 03:02:52 -0700
Subject: further thoughts
Message-ID: <20111105030252-0700@axiom-wiki.newsynthesis.org>

I find myself wanting a way to define types inductively like this::

X := Union(A,T X)

so X is an infinite sequence of types: A \/ T A \/ T T A \/ ...

where::

A:Type -- base type
T:X -> X -- endofunctor

but this is a circular definition, in order to break this circle
perhaps we could start by defining T as::

T: Type->Type

and then constraining it to T:X -> X in concrete implementations.

Can anyone suggest a variation of the following that would be valid in SPAD:
MonadCat(A:Type,T: Type->Type) : Category == with
X ==> Union(A,T X)
unit :X -> T X
mult :T ( T X) -> T X
So if we take a concrete instance of List then::

X := Union(A,List A,List List A, List List List A ...)

I get the impression that there is a hack in the List implementation that allows this? That is, when checking list types, the compiler does not look too deeply into the nested types? Perhaps if lists were implemented as monads such hacks would not be needed?

The above is done purely in terms of types/categories which would be the ideal way to implement monads but perhaps there is a less powerful but more easily implemented way to implement monads in terms of domains. In this case representations can be implemented inductively (co-data types), in category theory terms perhaps this is like working in terms of components?

So List is a monad with mult and unit defined as follows::

List(S: Type) is a domain constructor
Abbreviation for List is LIST
This constructor is exposed in this frame.
------------------------------- Operations --------------------------------
....
concat : List(%) -> % -- mult
list : S -> % -- unit
....

Martin

From MartinBaker Sat Nov 5 09:05:46 -0700 2011
From: Martin Baker
Date: Sat, 05 Nov 2011 09:05:46 -0700
Subject: From reply on FriCAS forum by Bertfried Fauser
Message-ID: <20111105090546-0700@axiom-wiki.newsynthesis.org>

(MJB)I would like to keep all the relevant information together so I have taken the liberty of copying this reply to here - marked (BF) and added some comments myself (MJB). If this page could be worked up into a full tutorial then perhaps this information could be incorporated into the main text.

(BF)First I tried to find where MONAD is defined in FriCAS, unfortunately the command
\begin{axiom}
This constructor is exposed in this frame.
------------------------------- Operations --------------------------------
?*? : (%,%) -> % ?=? : (%,%) -> Boolean
?^? : (%,PositiveInteger) -> % coerce : % -> OutputForm
hash : % -> SingleInteger latex : % -> String
?~=? : (%,%) -> Boolean
leftPower : (%,PositiveInteger) -> %
rightPower : (%,PositiveInteger) -> %
\end{axiom}
Does not say in which file the source code is (so greping is needed), it seems to be defined and used (in algebra) only in naalgc.spad.pamphlet'. There it says:
\begin{axiom}
++ with a binary operation.
\end{axiom}
and trouble starts. This is not what I understand of an monad, though they are related to monoids, but would better be understood as endofunctors in a category (or as a type constructor)

Math: A monad (triple, standard construction) (T,mu,eta) is a triple consisting of an endo_functor_ T : C --> C on a category C, a multiplication m : T T ---> T and a unit eta : C --> TC such that eta is the unit, and mu is associative (defined by some diagrams)

Let X be an object in C, then the natural transformations mu and eta have components mu_X and eta_X, which you seem to address (and the MONAD thing in AXIOM), this may be instantiated as a monoid (see the book by Arbib_Michael-Manes_E Arrows_structures_and_functors. _The_categorical_imperative-Academic_Press(1975))
which has lots of examples (power set, list, ...)

A monad as in Haskel operates on the category (including function types)

(MJB) I get the impression that the nomenclature for monads has changed over the years. Since what is currently in the Axiom code does not conform to modern conventions I suggest its name is changed to something less confusing.

> First test for List being monad (monad for a monoid) with:
> \mu = concat
> \eta = list
> T = []

Math: A monoid is a set X with two operations mu : X x X --> X and unit E s.t. mu (E x X) = X = mu(X x E).

(BF)I don't see why this should come with an fmap' function (functoriality of T)
(MJB) I have removed it in the page above.

This is actually a monad related to power sets, but lists also have order, while sets have not.

Let X be a set, eta(X)= [X] is the singleton list containing this set, eta : Set --> T Set, where
T Set is lists of sets.
Now T T Set is lists of lists of sets, eg, [[X,Y],[Y],[X],[Z,W]] :: T
T Set ; then the multiplication'
mu : T T --> T is flatening the lists' e.g. forgetting the inner
list's brackets -> [ X,Y,Y,X,Z,W]
Associativity of m guarantees that if you have lists of lists of lists of sets (type T T T Set) then either of the two ways to forget the inner brackets (multiplying the monad functor T) gives the same result. The left/right unit of this multiplication is the empty list
mu : [[],[X]] --> [X]
The difference is that this construction is much more like a template class in C++, as it can be instantiated on any (suitable) category C. And this is what the list constructor actually does...

> So I will check that the identities for monads are satisfied

Yes, for lists that follows from the above definition...

\begin{axiom}
> MonadCat(A:Type, B:Type,T: Type) : Category == with
> fmap :(A -> B) -> (T A -> T B)
> unit :A -> T A
> mult :T ( T A) -> T A
> @
\end{axiom}

Indeed, A and B should be objects in the base category, so they have the same type' (above A, B :: Set) . The A-->B is in Hom(A,B) = Set(A,B), the class of all functions from set A to set B, fmap allows to apply f inside the container T, and mult is actually used to flatten the container as types of type T T Set (say) appear under composing maps, as in unit o unit: A --> T T A

> It compiles but it doesn't look very useful?

It just defined what a monad is (provided you make sure in an implementation that your functor fulfils the correct associativity and unit laws. AXIOM checks in MONADWU (Monad with unit, ?)
\begin{axiom}
recip: % -> Union(%,"failed")
++ recip(a) returns an element, which is both a left and a right
++ or \spad{"failed"} if such an element doesn't exist or cannot
++ be determined (see unitsKnown).
\end{axiom}
if such a unit can be found (has been given?)

> We can think of T as being an endofunctor on MonadCat but also we want
> to turn things around by defining MonadCat in terms of T, that is we
> start with a base 'type' and extend it by repeatedly applying T to it.

T (as a monad) is an endofunctor on some' category, not on MonadCAT which is more or

> So we want to define T as an endofunctor:
Yes

But not like this. Think of T as a container which produces a new type
out of an old
Set --> Powerset Power set or Manes monad
Set --> List of sets List monad
Int --> List of ints List monad
Measurable Spaces --> Measures on Measurable Spaces Giry monad
etc (Manes has lots of examples)

> TList(A:Type) : Exports == Implementation where
> ...
> Rep := List A

Yes, much more like this.

I cannot comment more on the later parts of your message. Note that monad could be much more complicated functors than 'list'
T X = ( X x O)^I
where you think of I as inputs, O as outputs and X a a state. But you could have trees, binary trees, labelled trees, .....

(MJB) If this page were worked into a full tutorial then I would like to see it restructured so that there is more theory at the start and then there are several worked examples like those here in addition to the list example.

From MartinBaker Sat Nov 5 09:56:01 -0700 2011
From: Martin Baker
Date: Sat, 05 Nov 2011 09:56:01 -0700
Message-ID: <20111105095601-0700@axiom-wiki.newsynthesis.org>

I think it would be good if this page could explain why monads are important to include in a CAS, for me (MJB), this has something to do with the link between algebras and monads. I will make an attempt at explaining this and perhaps those more knowledgeable than me could correct any errors I make,

A monad gives an algebraic theory. (here we are using the word 'theory' as in: 'group theory') An algebra for a monad is a model for that theory. (model theory is the study of mathematical structures using tools from mathematical logic.)

An algebra takes an expression like this::
3*(9+4) - 5
and returns a value. This can be thought of as a monad where the endofunctor 'T' is the combination of the signatures of the operations.

An 'expression' can be constructed inductively from 'terms'. For instance, in the simple case of natural numbers, we could define a expression like this::

<Expression> ::= <Num> , <Expression> + <Expression>
<Num> ::= zero() , succ(<Num>)

This abstract syntax of a context-free language defines a free algebra, we can add the laws of addition to define the natural numbers.

So a term can contain a number, or other terms, or other terms containing other terms, and so on. We could think of this as a hierarchy of types:

- N

- T N

- T T N

- ...

Where:

- N is a numerical value.
- T N is a term containg a numerical value.
- T T N is a term containing a term containing a numerical value.
- ...

So 'T' is an endofunctor which raises the level of the term in the expression.

In order to construct and evaluate these expressions we need two natural transformations:

- \eta:N -> T N
- \mu:T T N -> T N

where
- \eta wraps an element in a term.
- \mu takes a term containing other terms and returns a term.

\eta is sometimes called the 'unit' although it will wrap any number, not just '1'. In fact it will take any term and raise its level.

\mu is sometimes called the 'multiplication' although this does not refer to the operation in the algebra being modelled so its not just multiplication or even just any binary operation, this could represent an operation of any 'arity'.

It is possible to extend the standard category theory to 'multicategories', these are the same as categories except that
instead of single arrow we can have 'arrows' with multiple inputs. This allows us to split up the function signature into individual functions.

So if we want to add 2 to 3 to find the result, they both have type 'N' so we must first we must first make them terms:
- \eta 2
- \eta 3

We can then construct
(\eta 2 + \eta 3)
which has type of T T N
We can then apply \mu which evaluates this to give a term:
\eta 5
We donâ€™t have a mechanism to unwrap this from a term and return a number. This is because pure F-algebras and inductive data types are 'initial' or 'constructive' that is they build these constructions but they are not designed to read out the data.

Of course, in a practical program, it is easy to add a function to read out the value. However when we are modelling these structures from a theoretical point of view, then there might be advantages to working with a pure F-algebra or F-coalgebra.
\section{Coalgebras and Coinductive types}
Algebras are initial and we can construct them but not necessarily read them out. Coalgebras are the reverse, that is they are final and we can read them out but not construct them.

Coalgebras and coinductive types are useful for:

- Represent free algebras.
- Infinite data types such as streams, infinite lists and non-well-founded sets.
- Dynamical systems with a hidden, black-box state space, finite automita.
- Bisimulations.
- Objects with 'hidden' (indirectly available via methods) data.

There are similarities between coinductive types and object oriented programming in that it is usually considerd good practice in OOP that the data (state space) is kept hidden from direct view and so data is only read using the objects methods (functions).

A general CAS, such as FriCAS, is very rich and does not restrict users to F-algebras or F-coalgebras, or even have these concepts. A general CAS allows any function signature (although multiple outputs may need to be wrapped in a Record or a List) since, in most cases we need to construct and observe data. However in order to model these structures it would be useful to have the concept of a pure F-algebra or F-coalgebra. Applications might include:
- converting between \lambda-calculus/combinators and a finite automata model of computation.
- converting between functional programming and object oriented programming.
- modelling algebraic, and co-algebraic structures.

We can convert between algebras and coalgebras with catamorphism (generalization of the concept of 'fold') anamorphism
\section{Object Oriented Programming}
(just checking if Ralf has read this far)
So far we have:
- Algebras: which allow us to construct instances of structures but not read them out.
- Coalgebras: which allow us to read out structures but not construct instances of them.

In a CAS it would be useful to be able to do both.

Object Oriented Programming (OOP) is closer to coalgebra in that its structure is fixed when the programmer defines the
class and can't be changed at runtime. Only the values of elements in the structure can be written and read at runtime.

So how can OOP represent an algebra? Well the object does not represent the whole algebra, it represents a single element of the algebra. However, although an object contains only a single element of the algebra it knows about the structural framework of the whole algebra, so it knows how to link to other elements to form the whole algebra.
\section{\Omega-Algebra}

A set of operator symbols, each operator has an 'arity' and all operators act only on the elements of the algebra.

\section{F-Algebra and F-Coalgebra}

F-Algebras and F-Coalgebras are the same as \Omega-(co)algebras except we denote all the operator signatures by a single functor.

If I may misuse Axiom/FriCAS notation (why stop now? I hear you say)
then I will notate this as:
\begin{verbatim}
Poly := () } n0 times
/\ (%) } n1 times
/\ (%,%) } n2 times
/\ (%,%,%) } n3 times
...
\end{verbatim}
So we can use this to define a free, pure algebra and a pure coalgebra as follows:
\begin{verbatim}
UniversalAlgebra() : Metacategory == with
Poly % -> %
@

UniversalCoalgebra() : Metacategory == with
% -> Poly %
@
\end{verbatim}
These represent free algebras and a particular instance can be formed by choosing values for the 'components': n0,n1,n2...

F-algebras and F-coalgebras are themselves categories. They can also be defined over an arbitrary category '%' where 'Poly % -> %' is an endofunctor from % to itself.

On their own pure algebra or coalgebra would not be much use, they don't have a way to interact with other algebras, but perhaps we could add that later.

A T-Algebra is an F-Algebra, as defined above, together with a set of equations (axioms) built from the F-Algebra operations.

So we have the endofunctor but what are the two natural transformations to construct a monad from it?

Let T be a (finitary) equational theory, consisting of finitely many operational symbols, each of some arity and a set of equations between terms built from these operations.

\section{Operations}
How do we specify operations (n-ary functions) in a T-algebra?

We can use lambda calculus, or equivalently combinators.

A requirement is that we need to be able express free algebras, as well as closed algebras, and algebras in-between. That is, some terms will simplify and some won't.

Algebraic constructs
A method where one algebraic entity is constructed from another.

A (co)algebra is defined 'over' another algebra and ultimately we get back to sets. For instance:
- Complex numbers might be defined over real numbers.
- Natural numbers might be defined over sets.
- Monoid over sets: algebra=lists.
- small category over graph.

This relationship between a (co)algebra and its elements is an adjunction:
\begin{verbatim}
F (or U) =forgetful
---------->
algebra elements
<----------
G (or F) =free
\end{verbatim}
Given an adjunction F -| G then GF=T for a monad where:

- \eta:1c -> GF
- \epsilon:FG -> 1d

This relates to the natural transformations for monads as follows::
\begin{itemize}
- multiplication for monad:\mu:T T -> T = G \epsilon F

This generates a whole category of monads for each algebra with extremes (canonical forms being) being:

- Eilenberg-Moore : In this case the monad is the terminal monad that is it represents the algebra
- Kleisli : In this case the monad is the initial solution so it is the algebra of free algebras.

In the Eilenberg-Moore case the algebra is a category with objects represented by a pair:
\begin{verbatim}
(X,Ex: TX->X)
where:
X is the object of the elements
T is the signature of the F-algebra (see below) this is the free functor applied to the forgetful functor (T=FU)
\end{verbatim}
\section{(Co)Algebra Example 1 - Natural Numbers}
Natural numbers give the simplest algebra, that is, they are
initial in the category of algebras. It can be represented as
an algebra or a coalgebra as follows:

- Algebra - is represented as an infinite set with a binary
operation \verb{+:(%,%)-> %}
- Coalgebra - is represented a two functions:
\verb{zero:()-> %}
\verb{succ:(%)-> %}

Using the coalgebra representation of natural numbers would not be very practical as it would not be realistic to support the level of function nesting to represent large numbers. But from a theoretical point of view it might be useful to have natural numbers which are not defined over sets and if large literal values are not required it might have some use?
\section{(Co)Algebra Example 2 - Groups}
A group is traditionally defined as an algebra, that is as operations+equations defined over a set:
operations::

- nullary operation: \verb{e:()-> %}
- unary operation: \verb{inv:(%)-> %}
- binary operation: \verb{*:(%,%)-> %}

equations defined in terms of arbitrary elements of the set::

- \forall x,y,z. x*(y*z)=(x*y)*z
- \forall x. x*inv(x)=e
- \forall x. e*x=x
- \forall x. inv(x)*x=e
- \forall x. x*e=x

Not all these equations are needed (there is some redundant information here) but there is no canonical form.
There are other problems with defining an algebra in an algebraic way such as:
- its defined over a set and we may want to define groups over other categories (known as group objects).
- this type of definition may not scale up well, especially if we define multiplication for a specific group using Cayley table.

Question - how does this relate to permutation groups? A permutation group looks to me like an endofunctor (viewing a group as a kind of category with just one object) and monad is related to monoid.

Group defined as a co-algebra:

Associativity:\mu\cdotp(id x \mu) = \mu\cdotp(\mu x id)
Identity :\mu\cdotp(\eta x id) = id = \mu\cdotp(id x \eta)
Inverse: \mu\cdotp(id x \delta)\cdotp\Delta = \eta\cdotp\epsilon = \mu\cdotp(\delta x id)\cdotp\Delta

where:

$\cdotp$ = function composition
x = Cartesian product
$\mu$ =multiplication
$\eta$ =
$\Delta$ = diagonalise
$\delta$ =
$\epsilon$ =