

last edited 9 years ago by test1 
1 2  
Editor: test1
Time: 2013/03/22 20:57:12 GMT+0 

Note: 
changed:  Implementation ==> Type add Implementation ==> add changed:  Implementation ==> Type add Implementation ==> add
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).
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) 
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:
T2a := [[A],[B]]
(2) 
T2b := [[C],[D]]
(3) 
then test associative square:
concat[concat T2a,concat T2b] = concat(concat[T2a, T2b])
(4) 
then test unit triangles:
concat(list[A]) = [A]
(5) 
concat[list A] = [A]
(6) 
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:
)abbrev category MONADC MonadCat MonadCat(A:Type,T: Type) : Category == with unit :A > T A mult :T ( T A) > T A
Compiling FriCAS source code from file /var/lib/zope2.10/instance/axiomwiki/var/LatexWiki/32590077796791546125px004.spad using old system compiler. MONADC abbreviates category MonadCat  initializing NRLIB MONADC for MonadCat compiling into NRLIB MONADC
;;; *** MonadCat REDEFINED Time: 0 SEC.
finalizing NRLIB MONADC Processing MonadCat for Browser database: >>MonadCat(constructor): Not documented!!!! >>MonadCat((unit ((T A) A))): Not documented!!!! >>MonadCat((mult ((T A) (T (T A))))): Not documented!!!! >>MonadCat(): Missing Description ; compiling file "/var/aw/var/LatexWiki/MONADC.NRLIB/MONADC.lsp" (written 05 APR 2022 08:43:37 PM):
; /var/aw/var/LatexWiki/MONADC.NRLIB/MONADC.fasl written ; compilation finished in 0:00:00.004  MonadCat is now explicitly exposed in frame initial MonadCat will be automatically loaded when needed from /var/aw/var/LatexWiki/MONADC.NRLIB/MONADC
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 axiomcategories that we need to define:
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:
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
Implementation ==> 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
Compiling FriCAS source code from file /var/lib/zope2.10/instance/axiomwiki/var/LatexWiki/537549349212764448225px005.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.01 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.01 SEC.
(time taken in buildFunctor: 0)
;;; *** TList REDEFINED
;;; *** TList REDEFINED Time: 0 SEC.
Cumulative Statistics for Constructor TList Time: 0.02 seconds
finalizing NRLIB TLIST Processing TList for Browser database: >>TList(constructor): Not documented!!!! >>TList((a (% (List A)))): Not documented!!!! >>TList((toList ((List A) %))): Not documented!!!! >>TList((baseType ((Type) %))): Not documented!!!! >>TList(): Missing Description ; compiling file "/var/aw/var/LatexWiki/TLIST.NRLIB/TLIST.lsp" (written 05 APR 2022 08:43:37 PM):
; /var/aw/var/LatexWiki/TLIST.NRLIB/TLIST.fasl written ; compilation finished in 0:00:00.016  TList is now explicitly exposed in frame initial TList will be automatically loaded when needed from /var/aw/var/LatexWiki/TLIST.NRLIB/TLIST
We then use this to generate
a list monad:
)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 ==> 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)
Compiling FriCAS source code from file /var/lib/zope2.10/instance/axiomwiki/var/LatexWiki/327634599490345850725px006.spad using old system compiler. MONADL abbreviates domain MonadList  initializing NRLIB MONADL for MonadList compiling into NRLIB MONADL Local variable Rep type redefined: (Join (SetCategory) (CATEGORY domain (SIGNATURE ~= ((Boolean) (Union (: leaf (TList A)) (: branch (TList $))) (Union (: leaf (TList A)) (: branch (TList $))))) (SIGNATURE coerce ((OutputForm) (Union (: leaf (TList A)) (: branch (TList $))))) (SIGNATURE construct ((Union (: leaf (TList A)) (: branch (TList $))) (TList A))) (SIGNATURE elt ((TList A) (Union (: leaf (TList A)) (: branch (TList $))) leaf)) (SIGNATURE case ((Boolean) (Union (: leaf (TList A)) (: branch (TList $))) leaf)) (SIGNATURE construct ((Union (: leaf (TList A)) (: branch (TList $))) (TList $))) (SIGNATURE elt ((TList $) (Union (: leaf (TList A)) (: branch (TList $))) branch)) (SIGNATURE case ((Boolean) (Union (: leaf (TList A)) (: branch (TList $))) branch)))) to (OneDimensionalArrayAggregate A) 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 SEC.
compiling exported mult : $ > $ Time: 0 SEC.
compiling exported coerce : $ > OutputForm ****** Domain: A already in scope augmenting A: (CoercibleTo (OutputForm)) ****** comp fails at level 8 with expression: ****** error in function coerce
(IF (case n leaf) (SEQ (:= e (toList (n leaf))) (SEQ (:= (: #1=#:G705 (Boolean)) (= (# e) 1)) (exit 1 (IF #1# (IF (has A (CoercibleTo (OutputForm))) (return (:: (first e) (OutputForm))) noBranch) noBranch))) (exit 1 (return (:: e (OutputForm))))) (SEQ (:= (: lst (List $)) (toList (n branch))) (:= lst2 (COLLECT (IN a lst) (:: (:: a $) (OutputForm)))) (SEQ (:= (: #2=#:G706 (Boolean)) (= (# lst2) 1)) (exit 1 (IF #2# (return (hconcat  <<  (:: "T " (OutputForm))  >>  (:: (first lst2) (OutputForm)))) noBranch))) (exit 1 (return (hconcat (:: "T " (OutputForm)) (:: lst2 (OutputForm))))))) ****** level 8 ****** $x:= (:: T (OutputForm)) $m:= $EmptyMode $f:= ((((#:G706 # #) (lst2 #) (a # #) (lst # #) ...)))
>> Apparent user error: Cannot coerce T of mode (String) to mode (OutputForm)
It might be better expressed if we had dependant variables but I think we can do it this way:
T2a := t[t[unit[A::Symbol]],t[unit[B::Symbol]]]
(7) 
T2b := t[t[unit[C::Symbol]],t[unit[D::Symbol]]]
(8) 
Going one way round the associativity square gives:
mult(t[mult T2a,mult T2b])
There are 1 exposed and 0 unexposed library operations named mult having 1 argument(s) but none was determined to be applicable. Use HyperDoc Browse,or issue )display op mult to learn more about the available operations. Perhaps packagecalling the operation or using coercions on the arguments will allow you to apply the operation.
Cannot find a definition or applicable library operation named mult with argument type(s) Symbol
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need.
Going the other way round the associativity square gives the same result:
mult(mult(t[T2a,T2b]))
There are 1 exposed and 0 unexposed library operations named mult having 1 argument(s) but none was determined to be applicable. Use HyperDoc Browse,or issue )display op mult to learn more about the available operations. Perhaps packagecalling the operation or using coercions on the arguments will allow you to apply the operation.
Cannot find a definition or applicable library operation named mult with argument type(s) Symbol
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need.
Also the identity triangle:
mult(t[t[unit[A::Symbol]]])
There are 1 exposed and 0 unexposed library operations named mult having 1 argument(s) but none was determined to be applicable. Use HyperDoc Browse,or issue )display op mult to learn more about the available operations. Perhaps packagecalling the operation or using coercions on the arguments will allow you to apply the operation.
Cannot find a definition or applicable library operation named mult with argument type(s) Symbol
Perhaps you should use "@" to indicate the required return type,or "$" to specify which version of the function you need.
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:
)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
Compiling FriCAS source code from file /var/lib/zope2.10/instance/axiomwiki/var/LatexWiki/60804501648025862925px011.spad using old system compiler. MONADC abbreviates category MonadCat ******** Spad syntax error detected ******** Expected: BACKTAB The prior line was:
2> MonadCat(A:Type,T: Type>Type) : Category == with
The current line is:
3> X ==> Union(A,T X)
The number of valid tokens is 1. The prior token was #S(TOKEN :SYMBOL X :TYPE IDENTIFIER :NONBLANK NIL :LINE_NUM 3 :CHAR_NUM 1) The current token is #S(TOKEN :SYMBOL ==> :TYPE KEYWORD :NONBLANK NIL :LINE_NUM 3 :CHAR_NUM 3)
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 (codata 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
(BF)First I tried to find where MONAD is defined in FriCAS, unfortunately the command
)show Monad
The )show system command is used to display information about types or partial types. For example,)show Integer will show information about Integer .
Monad is not the name of a known type constructor. If you want to see information about any operations named Monad ,issue )display operations Monad
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:
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.
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 contextfree 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:
Where:
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:
where
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:
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 Falgebras 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 Falgebra or Fcoalgebra.
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:
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 Falgebras or Fcoalgebras, 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 Falgebra or Fcoalgebra. Applications might include:
We can convert between algebras and coalgebras with catamorphism (generalization of the concept of fold
) anamorphism
(just checking if Ralf has read this far ;)
So far we have:
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.
A set of operator symbols, each operator has an arity
and all operators act only on the elements of the algebra.
FAlgebras and FCoalgebras 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...
Falgebras and Fcoalgebras 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 TAlgebra is an FAlgebra, as defined above, together with a set of equations (axioms) built from the FAlgebra 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.
How do we specify operations (nary functions) in a Talgebra?
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 inbetween. That is, some terms will simplify and some won't.
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:
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:
This relates to the natural transformations for monads as follows:
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:
In the EilenbergMoore case the algebra is a category with objects represented by a pair:
(X,Ex: TX>X)
where:
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:
+:(%,%)> %
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?
A group is traditionally defined as an algebra, that is as operations+equations defined over a set.
operations:
equations defined in terms of arbitrary elements of the set:
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:
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.
where:
)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
Compiling FriCAS source code from file /var/lib/zope2.10/instance/axiomwiki/var/LatexWiki/344644777026016275925px013.spad using old system compiler. MONADC abbreviates category MonadCat  initializing NRLIB MONADC for MonadCat compiling into NRLIB MONADC
;;; *** MonadCat REDEFINED Time: 0 SEC.
finalizing NRLIB MONADC Processing MonadCat for Browser database: >/var/lib/zope2.10/instance/axiomwiki/var/LatexWiki/32590077796791546125px004.spad>MonadCat(constructor): Not documented!!!! >/var/lib/zope2.10/instance/axiomwiki/var/LatexWiki/32590077796791546125px004.spad>MonadCat((unit ((M A) A))): Not documented!!!! >/var/lib/zope2.10/instance/axiomwiki/var/LatexWiki/32590077796791546125px004.spad>MonadCat((join ((M A) (M (M A))))): Not documented!!!! >/var/lib/zope2.10/instance/axiomwiki/var/LatexWiki/32590077796791546125px004.spad>MonadCat((mult ((M A) (M A) (M A)))): Not documented!!!! >/var/lib/zope2.10/instance/axiomwiki/var/LatexWiki/32590077796791546125px004.spad>MonadCat(): Missing Description ; compiling file "/var/aw/var/LatexWiki/MONADC.NRLIB/MONADC.lsp" (written 05 APR 2022 08:43:38 PM):
; /var/aw/var/LatexWiki/MONADC.NRLIB/MONADC.fasl written ; compilation finished in 0:00:00.003  MonadCat is already explicitly exposed in frame initial MonadCat will be automatically loaded when needed from /var/aw/var/LatexWiki/MONADC.NRLIB/MONADC
)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)
)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)
Compiling FriCAS source code from file /var/lib/zope2.10/instance/axiomwiki/var/LatexWiki/215492674218610493625px015.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 SEC.
compiling exported join : List List A > List A Time: 0 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 seconds
finalizing NRLIB MONADL Processing MonadList for Browser database: >>MonadList(): Missing Description ; compiling file "/var/aw/var/LatexWiki/MONADL.NRLIB/MONADL.lsp" (written 05 APR 2022 08:43:38 PM):
; /var/aw/var/LatexWiki/MONADL.NRLIB/MONADL.fasl written ; compilation finished in 0:00:00.010  MonadList is now explicitly exposed in frame initial MonadList will be automatically loaded when needed from /var/aw/var/LatexWiki/MONADL.NRLIB/MONADL
)show MonadList(Integer)
MonadList(Integer) is a domain constructor. Abbreviation for MonadList is MONADL This constructor is exposed in this frame. 3 Names for 3 Operations in this Domain.  Operations 
unit : Integer > List(Integer) join : List(List(Integer)) > List(Integer) mult : (List(Integer),List(Integer)) > List(Integer)
L := unit(3)$MonadList(Integer)
(9) 
I1:List Integer := [1,2]
(10) 
I2:List Integer := [3,4, 5]
(11) 
J1:=mult(I1,I2)$MonadList(Integer)
(12) 
J2:=join([I1,I2])$MonadList(Integer)
(13) 
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:
M2a := [[A],[B]]
(14) 
M2b := [[C],[D]]
(15) 
concat[concat M2a,concat M2b] = concat(concat[M2a, M2b])
(16) 
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:
MonadList(List List Integer)
MonadList(List Integer)
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:
Outer := join([[[1,2], [3, 4]], [[5, 6]]])$MonadList(List Integer)
(17) 
Then we can join the rest:
join(Outer)$MonadList(Integer)
(18) 
I'm not sure how we can concatenate the inner list first?
(Bill) How's this:
Inner := [join([[1,2], [3, 4]])$MonadList(Integer), join([[5, 6]])$MonadList(Integer)]
(19) 
join(Inner)$MonadList(Integer)
(20) 
(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
See SandBoxMonad for an attempt (in Aldor) 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 higherorder 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 highorder functions (functions which act on functions) is essential for this.