Edit detail for SandBoxMonads revision 1 of 2

changed:
-
**Bertfried Fauser** wrote:

  Does AXIOM have monads (like Haskell)? Sorry not much time to
investigate myself. Such things can be implemented very efficiently
and in an encapsulated way by using monads (in Haskell).

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}
Ref: http://en.wikipedia.org/wiki/Monad_%28category_theory%29

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

  As far as I can see there is already an SPAD category called Monad but
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.

First test for List being monad (monad for a monoid) with:
$\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
but with SPAD I think

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
general monad with these properties.

Haskell uses monads extensively so I thought that might provide an
example of how it could be coded?

Ref: http://en.wikipedia.org/wiki/Monad_%28functional_programming%29

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::

  class Monad m where
   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
translation from a Haskell typeclass to an SPAD category
(except I have changed 'm' to 'T' to give a more mathematical
notation:

\begin{spad}
)abbrev category MONADC MonadCat
MonadCat(A:Type,T: Type) : Category == with
 unit :A -> T A
 mult :T ( T A) -> T A
\end{spad}

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

  - 'MonadCat'

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} \to \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.
\begin{spad}
)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

 Implementation ==> Type add

   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
\end{spad}

We then use this to 'generate' a list monad:
\begin{spad}
)abbrev domain MONADL MonadList
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:%) -> %

 Implementation ==> Type add

   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)
\end{spad}

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:
\begin{spad}
)abbrev category MONADC MonadCat
MonadCat(A:Type,T: Type->Type) : Category == with
 X ==> Union(A,T X)
 unit :X -> T X
 mult :T ( T X) -> T X
\end{spad}
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}
)show Monad
\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::

  ++  Monad is the class of all multiplicative monads, i.e. sets
  ++  with a binary operation.

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 \to C$ on a category $C$, a multiplication $\mu : T T \to T$ and a unit $\eta : C \to 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.

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

(BF) ?? Monad $\ne$ monoid.

Math: A monoid is a set X with two operations $\mu : X \times X \to X$ and unit $E$ s.t. $\mu (E \times X) = X = \mu(X \times 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.

(BF) !ListMonad(Set):
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 : \mathrm{Set} \to T \mathrm{Set}$, where
$T \mathrm{Set}$ is lists of sets.
Now $T T \mathrm{Set}$ is lists of lists of sets, eg::

  [[X,Y],[Y],[X],[Z,W]] :: T

$T \textrm{Set}$ ; then the `multiplication'
$\mu : T T \to T$  is `flatening the lists' e.g. forgetting the inner
list's brackets::

  [X,Y,Y,X,Z,W]

Associativity of $\mu$ guarantees that if you have lists of lists of lists of sets (type $T T T \mathrm{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]] \to [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...

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

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

<pre>
  > )abbrev category MONADC MonadCat
  > 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
</pre>

Indeed, A and B should be objects in the base category, so they have the same `type' (above A, B :: Set) . The $A \to 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 \textrm{Set}$ (say) appear under composing maps, as in $unit \circ unit: A \to T T A$

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

It just defined what a monad is (provided you make sure in an implementation that your functor fulfills the correct associativity and unit laws. AXIOM checks in MONADWU (Monad with unit, ?)::

  recip: % -> Union(%,"failed")
        ++ recip(a) returns an element, which is both a left and a right
        ++ inverse of \spad{a},
        ++ or \spad{"failed"} if such an element doesn't exist or cannot
        ++ be determined (see unitsKnown).

if such a unit can be found (has been given?)

<pre>
  > 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.
</pre>

T (as a monad) is an endofunctor on `some' category, not on MonadCAT which is more or
less a collection of monads (functor category of monads and monad law preserving natural transformations)

<pre>
  > So we want to define T as an endofunctor:
</pre>

Yes

<pre>
  >  T:(MonadCat)-> MonadCat
</pre>

But not like this. Think of T as a container which produces a new type
out of an old:

- Set $\to$ Powerset      Power set or Manes monad

- Set $\to$ List of sets   List monad

- Int $\to$ List of ints    List monad

- Measurable Spaces $\to$ Measures on Measurable Spaces

Giry monad etc (Manes has lots of examples)

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

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
Subject: Algebras and Monads
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,

Monad

  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.

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 considered 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.

- Modelling monads and co-monads.

We can convert between algebras and co-algebras with catamorphism (generalization of the concept of 'fold') anamorphism

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.

$\Omega$-Algebra

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

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::

  Poly := () } n0 times
   /\ (%) } n1 times
   /\ (%,%) } n2 times
   /\ (%,%,%) } n3 times
  ...

So we can use this to define a free, pure algebra and a pure coalgebra as follows::

  UniversalAlgebra() : Metacategory == with
    Poly % -> %

  UniversalCoalgebra() : Metacategory == with
    % -> Poly %

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.

Monads and T-Algebras

  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.

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.

Algebras and Coalgebras from Adjoints

  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::

           F (or U) =forgetful
           ---------->
  algebra               elements
           <----------
         G (or F) =free

Every adjunction gives rise to an monad.
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:

- unit for monad:: $\eta$::1 -> T = $\eta$ for adjunction

- multiplication for monad::$\mu$::T T -> T = G $\epsilon$ F

Every monad gives rise to a class of adjunctions.

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::

  (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)

(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::

      +:(%,%)-> %

- Coalgebra - is represented a two functions::

      zero:()-> %
      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?

(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: e:()-> %

- unary operation: inv:(%)-> %

- binary operation: *:(%,%)-> %

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$ =


From BillPage Wed Nov 9 12:40:13 -0800 2011
From: Bill Page
Date: Wed, 09 Nov 2011 12:40:13 -0800
Subject: another attempt at defining Monad in SPAD
Message-ID: <20111109124013-0800@axiom-wiki.newsynthesis.org>

This may be a better definition of Monad in Axiom:
\begin{spad}
)abbrev category MONADC MonadCat
MonadCat(A : Type, M: Type -> Type): Category == with
  unit: A -> M A
  join: M M A -> M A
  mult: (M A, M A) -> M A
\end{spad}

\begin{axiom}
)show MonadCat
\end{axiom}

\begin{spad}
)abbrev package MONADL MonadList
MonadList(A:Type): MonadCat(A,List) == add
  unit(x:A):List A == list(x)
  join(x:List List A):List A == concat x
  mult(x:List A,y:List A):List A == concat(x,y)
\end{spad}

\begin{axiom}
)show MonadList(Integer)
\end{axiom}

\begin{axiom}
L := unit(3)$MonadList(Integer)
I1:List Integer := [1,2]
I2:List Integer := [3,4,5]
J1:=mult(I1,I2)$MonadList(Integer)
J2:=join([I1,I2])$MonadList(Integer)
\end{axiom}

From MartinBaker Mon Nov 14 05:57:28 -0800 2011
From: Martin Baker
Date: Mon, 14 Nov 2011 05:57:28 -0800
Subject: checking MonadList implementation
Message-ID: <20111114055728-0800@axiom-wiki.newsynthesis.org>

Good stuff, well done,

I'm having some difficulty with the following, I would just like to
check out the axioms in (1) at the top of the page, which are:

If we take the top one (associativity square) this goes from T^3 to T.
This makes sense to me in terms of lists, that is if we start off
lists of lists of lists it does not matter if we concatenate the inner
list first or the outer list first:

\begin{axiom}
M2a := [[A],[B]]
M2b := [[C],[D]]
concat[concat M2a,concat M2b] = concat(concat[M2a,M2b])
\end{axiom}

Can we do the same thing with your example? What I would expect is to
go from::

  MonadList(List List Integer) to MonadList(Integer)

That is I was expecting:

- T^3 ~ 'MonadList(List List Integer)'

- T^2 ~ 'MonadList(List Integer)'

- T ~ 'MonadList(Integer)'

So, starting in T^3, mult/join needs to go from:
'MonadList(List List Integer)' to 'MonadList(List Integer)'
and then when applied again from:
'MonadList(List Integer)' to 'MonadList(List)'.

We can do it, this will concatenate the outer lists:
\begin{axiom}
Outer := join([[[1,2],[3,4]],[[5,6]]])$MonadList(List Integer)
\end{axiom}
Then we can join the rest:
\begin{axiom}
join(Outer)$MonadList(Integer)
\end{axiom}

I'm not sure how we can concatenate the inner list first?

(Bill) How's this:
\begin{axiom}
Inner := [join([[1,2],[3,4]])$MonadList(Integer),join([[5,6]])$MonadList(Integer)]
join(Inner)$MonadList(Integer)
\end{axiom}
(Martin) Yes, I guess that's equivalent to the List example, what would be good now
would be to go beyond that and use the power of monads. It just seems to me that if
we stay in the MonadList(Integer) domain we are only putting a thin wrapper around
Lists (working purely in T). It seems to me that the power of monads comes from the
hierarchical type structure so to fully demonstrate the associativity square we need
to start in T^3 and go both ways round to T.

So I guess that if for 'mu' we work with::

  join()$MonadList(Integer)

and for 'T mu' we work with::

  join()$MonadList(List Integer)

so what form would 'mu T' take?

Is there any way that we could include the endofunctor 'T' so calling
a function 'T' in 'MonadList(Integer)' will generate a type
'MonadList(List Integer)' and calling the function 'T' in
'MonadList(List Integer)' will generate a type
'MonadList(List List Integer)' and so on?

Or alternatively, could the functionality of 'MonadList(Integer)',
'MonadList(List Integer)', 'MonadList(List List Integer)'... all be
included in 'MonadList(Integer)' so we don't have to switch types?

I assume there is no way that we can enforce these axioms in 'MonadCat'?
That is we have to do this for each implementation separately.

Martin

From BillPage Tue Nov 15 07:39:57 -0800 2011
From: Bill Page
Date: Tue, 15 Nov 2011 07:39:57 -0800
Subject: re: endofunctor T
Message-ID: <20111115073957-0800@axiom-wiki.newsynthesis.org>

See SandBoxMonad for an attempt (in Aldor)

From BillPage Tue Nov 15 07:50:28 -0800 2011
From: Bill Page
Date: Tue, 15 Nov 2011 07:50:28 -0800
Subject: re: enforcing axioms
Message-ID: <20111115075028-0800@axiom-wiki.newsynthesis.org>

In general (and perhaps ironically enough) enforcing axioms in Axiom is not possible. But there is at least one sense in which this is not quite true.

In categorical terms it is possible to make assertions "by demonstration", i.e. constructively. For example in the page LimitsAndColimits a Product is define by it's universal property: the existence (and implicitly the uniqueness) of the higher-order operator::

  product: (A:Type, A->X,A->Y) -> (A->%)

To some people and from certain points of view this might seem trivial, but to me it is one of the great opportunities to apply category theory to computer algebra.  It seems that the use of high-order functions (functions which act on functions) is essential for this.

Bertfried Fauser wrote:

Does AXIOM have monads (like Haskell)? Sorry not much time to investigate myself. Such things can be implemented very efficiently and in an encapsulated way by using monads (in Haskell).

Formal definition

If C is a category, a monad on C consists of a functor together with two natural transformations: (where denotes the identity functor on C) and (where is the functor from C to C). These are required to fulfill the following conditions (sometimes called coherence conditions):

(1)

We can rewrite these conditions using following commutative diagrams: Ref: http://en.wikipedia.org/wiki/Monad_%28category_theory%29

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

As far as I can see there is already an SPAD category called Monad but 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.

First test for List being monad (monad for a monoid) with: = concat, = list, and = [].

Here T and 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 but with SPAD I think

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

First something to work with:

axiom

T2a := [[A],[B]]

(2)

Type: List(List(Symbol))

axiom

T2b := [[C],[D]]

(3)

Type: List(List(Symbol))

then test associative square:

axiom

concat[concat T2a,concat T2b] = concat(concat[T2a,T2b])

(4)

Type: Equation(List(Symbol))

then test unit triangles:

axiom

concat(list[A]) = [A]

(5)

Type: Equation(List(Variable(A)))

axiom

concat[list A] = [A]

(6)

Type: Equation(List(Variable(A)))

So this seems to have the properties needed, I would like to build a general monad with these properties.

Haskell uses monads extensively so I thought that might provide an example of how it could be coded?

Ref: http://en.wikipedia.org/wiki/Monad_%28functional_programming%29

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:

  class Monad m where
   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 translation from a Haskell typeclass to an SPAD category (except I have changed m to T to give a more mathematical notation:

spad

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

spad

   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/325900777967915461-25px004.spad using 
      old system compiler.
   MONADC abbreviates category MonadCat 
------------------------------------------------------------------------
   initializing NRLIB MONADC for MonadCat 
   compiling into NRLIB MONADC 

;;;     ***       |MonadCat| REDEFINED
Time: 0.01 SEC.

   finalizing NRLIB MONADC 
   Processing MonadCat for Browser database:
--->-->MonadCat((unit ((T A) A))): Not documented!!!!
--->-->MonadCat((mult ((T A) (T (T A))))): Not documented!!!!
--->-->MonadCat(constructor): Not documented!!!!
--->-->MonadCat(): Missing Description
; compiling file "/var/zope2/var/LatexWiki/MONADC.NRLIB/MONADC.lsp" (written 15 NOV 2011 08:47:24 AM):

; /var/zope2/var/LatexWiki/MONADC.NRLIB/MONADC.fasl written
; compilation finished in 0:00:00.085
------------------------------------------------------------------------
   MonadCat is now explicitly exposed in frame initial 
   MonadCat will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/MONADC.NRLIB/MONADC

   >> System error:
   The bounding indices 163 and 162 are bad for a sequence of length 162.
See also:
  The ANSI Standard, Glossary entry for "bounding index designator"
  The ANSI Standard, writeup for Issue SUBSEQ-OUT-OF-BOUNDS:IS-AN-ERROR

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
• MonadCat

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:

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.

spad

)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

 Implementation ==> Type add

   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

spad

   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/1419636053969527691-25px005.spad using 
      old system compiler.
   TLIST abbreviates domain TList 
------------------------------------------------------------------------
   initializing NRLIB TLIST for TList 
   compiling into NRLIB TLIST 
   compiling exported a : List A -> $
Time: 0.04 SEC.

   compiling exported toList : $ -> List A
Time: 0 SEC.

   compiling exported baseType : $ -> Type
Time: 0 SEC.

   compiling exported coerce : $ -> OutputForm
****** Domain: A already in scope
augmenting A: (CoercibleTo (OutputForm))
Time: 0.06 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |TList| REDEFINED

;;;     ***       |TList| REDEFINED
Time: 0 SEC.

   Cumulative Statistics for Constructor TList
      Time: 0.10 seconds

--------------non extending category----------------------
.. TList(#1) of cat 
(|Join| (|CoercibleTo| (|OutputForm|))
        (CATEGORY |domain| (SIGNATURE |a| ($ (|List| |#1|)))
         (SIGNATURE |toList| ((|List| |#1|) $))
         (SIGNATURE |baseType| ((|Type|) $))))   has no 
(|Category|)    finalizing NRLIB TLIST 
   Processing TList for Browser database:
--->-->TList((a (% (List A)))): Not documented!!!!
--->-->TList((toList ((List A) %))): Not documented!!!!
--->-->TList((baseType ((Type) %))): Not documented!!!!
--->-->TList(constructor): Not documented!!!!
--->-->TList(): Missing Description
; compiling file "/var/zope2/var/LatexWiki/TLIST.NRLIB/TLIST.lsp" (written 15 NOV 2011 08:47:26 AM):

; /var/zope2/var/LatexWiki/TLIST.NRLIB/TLIST.fasl written
; compilation finished in 0:00:00.132
------------------------------------------------------------------------
   TList is now explicitly exposed in frame initial 
   TList will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/TLIST.NRLIB/TLIST

   >> System error:
   The bounding indices 163 and 162 are bad for a sequence of length 162.
See also:
  The ANSI Standard, Glossary entry for "bounding index designator"
  The ANSI Standard, writeup for Issue SUBSEQ-OUT-OF-BOUNDS:IS-AN-ERROR

We then use this to generate a list monad:

spad

)abbrev domain MONADL MonadList
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:%) -> %

 Implementation ==> Type add

   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)

spad

   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/8559905649552304410-25px006.spad using 
      old system compiler.
   MONADL abbreviates domain MonadList 
------------------------------------------------------------------------
   initializing NRLIB MONADL for MonadList 
   compiling into NRLIB MONADL 
   compiling exported t : TList $ -> $
      MONADL;t;Tl$;1 is replaced by CONS1inpu 
Time: 0.01 SEC.

   compiling exported t : List $ -> $
Time: 0 SEC.

   compiling exported unit : TList A -> $
      MONADL;unit;Tl$;3 is replaced by CONS0inpu 
Time: 0 SEC.

   compiling exported unit : List A -> $
Time: 0 SEC.

   compiling exported unit : A -> $
Time: 0.01 SEC.

   compiling exported mult : $ -> $
Time: 0.03 SEC.

   compiling exported coerce : $ -> OutputForm
****** Domain: A already in scope
augmenting A: (CoercibleTo (OutputForm))
Time: 0.02 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |MonadList| REDEFINED

;;;     ***       |MonadList| REDEFINED
Time: 0.01 SEC.

   Warnings: 
      [1] mult:  branch has no value
      [2] coerce:  leaf has no value
      [3] coerce:  branch has no value

   Cumulative Statistics for Constructor MonadList
      Time: 0.08 seconds

--------------non extending category----------------------
.. MonadList(#1) of cat 
(|Join| (|CoercibleTo| (|OutputForm|))
        (CATEGORY |domain| (SIGNATURE |t| ($ (|TList| $)))
         (SIGNATURE |t| ($ (|List| $))) (SIGNATURE |unit| ($ (|TList| |#1|)))
         (SIGNATURE |unit| ($ (|List| |#1|))) (SIGNATURE |unit| ($ |#1|))
         (SIGNATURE |mult| ($ $))))   has no 
(|Category|)    finalizing NRLIB MONADL 
   Processing MonadList for Browser database:
--->-->MonadList((t (% (TList %)))): Not documented!!!!
--->-->MonadList((t (% (List %)))): Not documented!!!!
--->-->MonadList((unit (% (TList A)))): Not documented!!!!
--->-->MonadList((unit (% (List A)))): Not documented!!!!
--->-->MonadList((unit (% A))): Not documented!!!!
--->-->MonadList((mult (% %))): Not documented!!!!
--->-->MonadList(constructor): Not documented!!!!
--------constructor---------
; compiling file "/var/zope2/var/LatexWiki/MONADL.NRLIB/MONADL.lsp" (written 15 NOV 2011 08:47:26 AM):

; /var/zope2/var/LatexWiki/MONADL.NRLIB/MONADL.fasl written
; compilation finished in 0:00:00.197
------------------------------------------------------------------------
   MonadList is now explicitly exposed in frame initial 
   MonadList will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/MONADL.NRLIB/MONADL

   >> System error:
   The bounding indices 163 and 162 are bad for a sequence of length 162.
See also:
  The ANSI Standard, Glossary entry for "bounding index designator"
  The ANSI Standard, writeup for Issue SUBSEQ-OUT-OF-BOUNDS:IS-AN-ERROR

It might be better expressed if we had dependant variables but I think we can do it this way:

axiom

T2a := t[t[unit[A::Symbol]],t[unit[B::Symbol]]]

(7)

Type: MonadList?(Symbol)

axiom

T2b := t[t[unit[C::Symbol]],t[unit[D::Symbol]]]

(8)

Type: MonadList?(Symbol)

Going one way round the associativity square gives:

axiom

mult(t[mult T2a,mult T2b])

(9)

Type: MonadList?(Symbol)

Going the other way round the associativity square gives the same result:

axiom

mult(mult(t[T2a,T2b]))

(10)

Type: MonadList?(Symbol)

Also the identity triangle:

axiom

mult(t[t[unit[A::Symbol]]])

(11)

Type: MonadList?(Symbol)

further thoughts --Martin Baker, Sat, 05 Nov 2011 03:02:52 -0700 reply

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:

spad

)abbrev category MONADC MonadCat
MonadCat(A:Type,T: Type->Type) : Category == with
 X ==> Union(A,T X)
 unit :X -> T X
 mult :T ( T X) -> T X

spad

   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/608045016480258629-25px011.spad using 
      old system compiler.
   MONADC abbreviates category MonadCat 
******** Boot Syntax Error detected ********
The prior line was:

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

The current line is:

    2> (X ==> Union(A,T X); 
             ^
First currently preparsed lines are:

    3>  unit :X -> T X;
    4>  mult :T ( T X) -> T X)

The number of valid tokens is 1.
The prior token was #S(TOKEN :SYMBOL X :TYPE IDENTIFIER :NONBLANK T)
The current token is #S(TOKEN :SYMBOL ==> :TYPE KEYWORD :NONBLANK NIL)

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 reply on FriCAS? forum by Bertfried Fauser --Martin Baker, Sat, 05 Nov 2011 09:05:46 -0700 reply

(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

axiom

)show Monad

 Monad  is a category constructor
 Abbreviation for Monad is MONAD 
 This constructor is exposed in this frame.
------------------------------- Operations --------------------------------
 ?*? : (%,%) -> %                      ?=? : (%,%) -> Boolean
 ?^? : (%,PositiveInteger) -> %        coerce : % -> OutputForm
 hash : % -> SingleInteger             latex : % -> String
 ?~=? : (%,%) -> Boolean              
 leftPower : (%,PositiveInteger) -> %
 rightPower : (%,PositiveInteger) -> %

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:

  ++  Monad is the class of all multiplicative monads, i.e. sets
  ++  with a binary operation.

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) is a triple consisting of an endofunctor on a category , a multiplication and a unit such that is the unit, and is associative (defined by some diagrams)

Let X be an object in C, then the natural transformations and have components and , 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 = []

(BF) ?? Monad monoid.

Math: A monoid is a set X with two operations and unit s.t. .

(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.

(BF) ListMonad(Set): This is actually a monad related to power sets, but lists also have order, while sets have not.

Let be a set, is the singleton list containing this set, , where is lists of sets. Now is lists of lists of sets, eg:

  [[X,Y],[Y],[X],[Z,W]] :: T

; then the `multiplication' is `flatening the lists' e.g. forgetting the inner list's brackets:

  [X,Y,Y,X,Z,W]

Associativity of guarantees that if you have lists of lists of lists of sets (type ) 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 The difference is that this construction is much more like a template class in C++, as it can be instantiated on any (suitable) category . 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...

  > )abbrev category MONADC MonadCat
  > 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

Indeed, A and B should be objects in the base category, so they have the same `type' (above A, B :: Set) . The is in , 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 (say) appear under composing maps, as in

  > 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 fulfills the correct associativity and unit laws. AXIOM checks in MONADWU (Monad with unit, ?):

  recip: % -> Union(%,"failed")
        ++ recip(a) returns an element, which is both a left and a right
        ++ inverse of \spad{a},
        ++ or \spad{"failed"} if such an element doesn't exist or cannot
        ++ be determined (see unitsKnown).

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 less a collection of monads (functor category of monads and monad law preserving natural transformations)

  > So we want to define T as an endofunctor:

Yes

  >  T:(MonadCat)-> MonadCat

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.

Algebras and Monads --Martin Baker, Sat, 05 Nov 2011 09:56:01 -0700 reply

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,

Monad

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:

• :N -> T N
• :T T N -> T N

where

• wraps an element in a term.
• takes a term containing other terms and returns a term.

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.

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:

• 2
• 3

We can then construct which has type of We can then apply which evaluates this to give a term: 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.

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 considered 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 -calculus/combinators and a finite automata model of computation.
• Converting between functional programming and object oriented programming.
• Modelling algebraic, and co-algebraic structures.
• Modelling monads and co-monads.

We can convert between algebras and co-algebras with catamorphism (generalization of the concept of fold) anamorphism

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.

-Algebra

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

F-Algebra and F-Coalgebra

F-Algebras and F-Coalgebras are the same as -(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:

  Poly := () } n0 times
   /\ (%) } n1 times
   /\ (%,%) } n2 times
   /\ (%,%,%) } n3 times
  ...

So we can use this to define a free, pure algebra and a pure coalgebra as follows:

  UniversalAlgebra() : Metacategory == with
    Poly % -> %

  UniversalCoalgebra() : Metacategory == with
    % -> Poly %

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.

Monads and T-Algebras

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.

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.

Algebras and Coalgebras from Adjoints

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:

           F (or U) =forgetful
           ---------->
  algebra               elements
           <----------
         G (or F) =free

Every adjunction gives rise to an monad. Given an adjunction F -| G then GF=T for a monad where:

• :1c -> GF
• :FG -> 1d

This relates to the natural transformations for monads as follows:

• unit for monad:: ::1 -> T = for adjunction
• multiplication for monad::::T T -> T = G F

Every monad gives rise to a class of adjunctions.

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:

  (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)

(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:

        +:(%,%)-> %
  

• Coalgebra - is represented a two functions:

        zero:()-> %
        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?

(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: e:()-> %
• unary operation: inv:(%)-> %
• binary operation: *:(%,%)-> %

equations defined in terms of arbitrary elements of the set:

• x,y,z. x(yz)=(xy)z
• x. x*inv(x)=e
• x. e*x=x
• x. inv(x)*x=e
• 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:
• Identity :)
• Inverse:

where:

• = function composition
• x = Cartesian product
• =multiplication
• =
• = diagonalise
• =
• =

another attempt at defining Monad in SPAD --Bill Page, Wed, 09 Nov 2011 12:40:13 -0800 reply

This may be a better definition of Monad in Axiom:

spad

)abbrev category MONADC MonadCat
MonadCat(A : Type, M: Type -> Type): Category == with
  unit: A -> M A
  join: M M A -> M A
  mult: (M A, M A) -> M A

spad

   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/3446447770260162759-25px013.spad using 
      old system compiler.
   MONADC abbreviates category MonadCat 
------------------------------------------------------------------------
   initializing NRLIB MONADC for MonadCat 
   compiling into NRLIB MONADC 

;;;     ***       |MonadCat| REDEFINED
Time: 0.01 SEC.

   finalizing NRLIB MONADC 
   Processing MonadCat for Browser database:
--->/var/zope2/var/LatexWiki/325900777967915461-25px004.spad-->MonadCat((unit ((M A) A))): Not documented!!!!
--->/var/zope2/var/LatexWiki/325900777967915461-25px004.spad-->MonadCat((join ((M A) (M (M A))))): Not documented!!!!
--->/var/zope2/var/LatexWiki/325900777967915461-25px004.spad-->MonadCat((mult ((M A) (M A) (M A)))): Not documented!!!!
--->/var/zope2/var/LatexWiki/325900777967915461-25px004.spad-->MonadCat(constructor): Not documented!!!!
--->/var/zope2/var/LatexWiki/325900777967915461-25px004.spad-->MonadCat(): Missing Description
; compiling file "/var/zope2/var/LatexWiki/MONADC.NRLIB/MONADC.lsp" (written 15 NOV 2011 08:47:26 AM):

; /var/zope2/var/LatexWiki/MONADC.NRLIB/MONADC.fasl written
; compilation finished in 0:00:00.013
------------------------------------------------------------------------
   MonadCat is already explicitly exposed in frame initial 
   MonadCat will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/MONADC.NRLIB/MONADC

   >> System error:
   The bounding indices 163 and 162 are bad for a sequence of length 162.
See also:
  The ANSI Standard, Glossary entry for "bounding index designator"
  The ANSI Standard, writeup for Issue SUBSEQ-OUT-OF-BOUNDS:IS-AN-ERROR

axiom

)show MonadCat

 MonadCat(A: Type,M: (Type -> Type))  is a category constructor
 Abbreviation for MonadCat is MONADC 
 This constructor is exposed in this frame.
------------------------------- Operations --------------------------------
 join : M(M(A)) -> M(A)                mult : (M(A),M(A)) -> M(A)
 unit : A -> M(A)

spad

)abbrev package MONADL MonadList
MonadList(A:Type): MonadCat(A,List) == add
  unit(x:A):List A == list(x)
  join(x:List List A):List A == concat x
  mult(x:List A,y:List A):List A == concat(x,y)

spad

   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/2154926742186104936-25px015.spad using 
      old system compiler.
   Illegal NRLIB 
   MONADL.NRLIB claims that its constructor name is the package 
      MonadList but MonadList is already known to be the for domain 
      MONADL .
   MONADL abbreviates package MonadList 
------------------------------------------------------------------------
   initializing NRLIB MONADL for MonadList 
   compiling into NRLIB MONADL 
   compiling exported unit : A -> List A
Time: 0.02 SEC.

   compiling exported join : List List A -> List A
Time: 0.01 SEC.

   compiling exported mult : (List A,List A) -> List A
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |MonadList| REDEFINED

;;;     ***       |MonadList| REDEFINED
Time: 0 SEC.

   Cumulative Statistics for Constructor MonadList
      Time: 0.03 seconds

   finalizing NRLIB MONADL 
   Processing MonadList for Browser database:
--->/var/zope2/var/LatexWiki/8559905649552304410-25px006.spad-->MonadList(): Missing Description
; compiling file "/var/zope2/var/LatexWiki/MONADL.NRLIB/MONADL.lsp" (written 15 NOV 2011 08:47:27 AM):

; /var/zope2/var/LatexWiki/MONADL.NRLIB/MONADL.fasl written
; compilation finished in 0:00:00.038
------------------------------------------------------------------------
   MonadList is already explicitly exposed in frame initial 
   MonadList will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/MONADL.NRLIB/MONADL

   >> System error:
   The bounding indices 163 and 162 are bad for a sequence of length 162.
See also:
  The ANSI Standard, Glossary entry for "bounding index designator"
  The ANSI Standard, writeup for Issue SUBSEQ-OUT-OF-BOUNDS:IS-AN-ERROR

axiom

)show MonadList(Integer)

 MonadList(Integer) is a domain constructor.
 Abbreviation for MonadList is MONADL 
 This constructor is exposed in this frame.
------------------------------- Operations --------------------------------

 unit : Integer -> List(Integer)      
 join : List(List(Integer)) -> List(Integer)
 mult : (List(Integer),List(Integer)) -> List(Integer)

axiom

L := unit(3)$MonadList(Integer)

(12)

Type: List(Integer)

axiom

I1:List Integer := [1,2]

(13)

Type: List(Integer)

axiom

I2:List Integer := [3,4,5]

(14)

Type: List(Integer)

axiom

J1:=mult(I1,I2)$MonadList(Integer)

(15)

Type: List(Integer)

axiom

J2:=join([I1,I2])$MonadList(Integer)

(16)

Type: List(Integer)

checking MonadList? implementation --Martin Baker, Mon, 14 Nov 2011 05:57:28 -0800 reply

Good stuff, well done,

I'm having some difficulty with the following, I would just like to check out the axioms in (1) at the top of the page, which are:

If we take the top one (associativity square) this goes from T^3 to T. This makes sense to me in terms of lists, that is if we start off lists of lists of lists it does not matter if we concatenate the inner list first or the outer list first:

axiom

M2a := [[A],[B]]

(17)

Type: List(List(Symbol))

axiom

M2b := [[C],[D]]

(18)

Type: List(List(Symbol))

axiom

concat[concat M2a,concat M2b] = concat(concat[M2a,M2b])

(19)

Type: Equation(List(Symbol))

Can we do the same thing with your example? What I would expect is to go from:

  MonadList(List List Integer) to MonadList(Integer)

That is I was expecting:

• T^3 ~ MonadList(List List Integer)
• T^2 ~ MonadList(List Integer)
• T ~ MonadList(Integer)

So, starting in T^3, mult/join needs to go from: MonadList(List List Integer) to MonadList(List Integer) and then when applied again from: MonadList(List Integer) to MonadList(List).

We can do it, this will concatenate the outer lists:

axiom

Outer := join([[[1,2],[3,4]],[[5,6]]])$MonadList(List Integer)

(20)

Type: List(List(Integer))

Then we can join the rest:

axiom

join(Outer)$MonadList(Integer)

(21)

Type: List(Integer)

I'm not sure how we can concatenate the inner list first?

(Bill) How's this:

axiom

Inner := [join([[1,2],[3,4]])$MonadList(Integer),join([[5,6]])$MonadList(Integer)]

(22)

Type: List(List(Integer))

axiom

join(Inner)$MonadList(Integer)

(23)

Type: List(Integer)

(Martin) Yes, I guess that's equivalent to the List example, what would be good now would be to go beyond that and use the power of monads. It just seems to me that if we stay in the MonadList?(Integer) domain we are only putting a thin wrapper around Lists (working purely in T). It seems to me that the power of monads comes from the hierarchical type structure so to fully demonstrate the associativity square we need to start in T^3 and go both ways round to T.

So I guess that if for mu we work with:

  join()$MonadList(Integer)

and for T mu we work with:

  join()$MonadList(List Integer)

so what form would mu T take?

Is there any way that we could include the endofunctor T so calling a function T in MonadList(Integer) will generate a type MonadList(List Integer) and calling the function T in MonadList(List Integer) will generate a type MonadList(List List Integer) and so on?

Or alternatively, could the functionality of MonadList(Integer), MonadList(List Integer), MonadList(List List Integer)... all be included in MonadList(Integer) so we don't have to switch types?

I assume there is no way that we can enforce these axioms in MonadCat? That is we have to do this for each implementation separately.

Martin

re: endofunctor T --Bill Page, Tue, 15 Nov 2011 07:39:57 -0800 reply

See SandBoxMonad? for an attempt (in Aldor)

re: enforcing axioms --Bill Page, Tue, 15 Nov 2011 07:50:28 -0800 reply

In general (and perhaps ironically enough) enforcing axioms in Axiom is not possible. But there is at least one sense in which this is not quite true.

In categorical terms it is possible to make assertions "by demonstration", i.e. constructively. For example in the page LimitsAndColimits? a Product is define by it's universal property: the existence (and implicitly the uniqueness) of the higher-order operator:

  product: (A:Type, A->X,A->Y) -> (A->%)

To some people and from certain points of view this might seem trivial, but to me it is one of the great opportunities to apply category theory to computer algebra. It seems that the use of high-order functions (functions which act on functions) is essential for this.