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
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 First test for List being monad (monad for a monoid) with:
Here T and So I will check that the identities for monads are satisfied. First something to work with: fricas T2a := [[A],
Type: List(List(Symbol))
fricas T2b := [[C],
Type: List(List(Symbol))
then test associative square: fricas concat[concat T2a,
Type: Equation(List(Symbol))
then test unit triangles: fricas concat(list[A]) = [A]
Type: Equation(List(Variable(A)))
fricas concat[list A] = [A]
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 spad )abbrev category MONADC MonadCat MonadCat(A:Type, spad Compiling FriCAS source code from file
/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/325900777967915461-25px004.spad
using old system compiler.
MONADC abbreviates category MonadCat
------------------------------------------------------------------------
initializing NRLIB MONADC for MonadCat
compiling into 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 axiom-categories that we need to define:
We can think of T as being an endofunctor on 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. spad )abbrev domain TLIST TList TList(A:Type) : Exports == Implementation where Exports == CoercibleTo(OutputForm) with spad Compiling FriCAS source code from file
/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/5375493492127644482-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.01 SEC.We then use this to spad )abbrev domain MONADL MonadList MonadList(A:Type) : Exports == Implementation where Exports == CoercibleTo(OutputForm) with spad Compiling FriCAS source code from file
/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/3276345994903458507-25px006.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.It might be better expressed if we had dependant variables but I think we can do it this way: fricas T2a := t[t[unit[A::Symbol]],
Type: Symbol
fricas T2b := t[t[unit[C::Symbol]],
Type: Symbol
Going one way round the associativity square gives: fricas mult(t[mult T2a, Going the other way round the associativity square gives the same result: fricas mult(mult(t[T2a, Also the identity triangle: fricas mult(t[t[unit[A::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, spad Compiling FriCAS source code from file
/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/608045016480258629-25px011.spad
using old system compiler.
MONADC abbreviates category MonadCat
******** Spad syntax error detected ********
Expected: BACKTAB
The prior line was: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 fricas )show 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) Let X be an object in C, then the natural transformations 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 Math: A monoid is a set X with two operations (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,Y],[Y],[X],[Z,W]] :: T
[X,Y,Y,X,Z,W] Associativity of > 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 > 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
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,MonadA 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 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:
Where:
So In order to construct and evaluate these expressions we need two natural transformations:
where
It is possible to extend the standard category theory to So if we want to add 2 to 3 to find the result, they both have type
We can then construct
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 typesAlgebras 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:
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:
We can convert between algebras and co-algebras with catamorphism (generalization of the concept of Object Oriented Programming(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.
|
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):![\label{eq1}
\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).}](images/8019230973110099146-16.0px.png "\label{eq1}
\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).}")
![\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
}](images/2398827330270852675-16.0px.png "\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
}")
= 
= 
= [].![\label{eq2}\left[{\left[ A \right]}, \:{\left[ B \right]}\right]](images/318932535670649065-16.0px.png "\label{eq2}\left[{\left[ A \right]}, \:{\left[ B \right]}\right]")
![\label{eq3}\left[{\left[ C \right]}, \:{\left[ D \right]}\right]](images/2475988003480733344-16.0px.png "\label{eq3}\left[{\left[ C \right]}, \:{\left[ D \right]}\right]")
![\label{eq4}{\left[ A , \: B , \: C , \: D \right]}={\left[ A , \: B , \: C , \: D \right]}](images/254350511047754390-16.0px.png "\label{eq4}{\left[ A , \: B , \: C , \: D \right]}={\left[ A , \: B , \: C , \: D \right]}")
![\label{eq5}{\left[ A \right]}={\left[ A \right]}](images/110844751533603257-16.0px.png "\label{eq5}{\left[ A \right]}={\left[ A \right]}")
![\label{eq6}{\left[ A \right]}={\left[ A \right]}](images/6702261161917126472-16.0px.png "\label{eq6}{\left[ A \right]}={\left[ A \right]}")
is a triple consisting of an endofunctor 
on a category 
, a multiplication 
and a unit 
such that 
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, ...)
monoid.
and unit 
s.t. 
.
be a set, ![\eta(X)= [X]](images/3729854948363741002-16.0px.png "\eta(X)= [X]")
is the singleton list containing this set, 
, where
is lists of sets.
Now 
is lists of lists of sets, eg:
; then the `multiplication'
) 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]](images/2083959855475493047-16.0px.png "\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 
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 
Powerset Power set or Manes monad
which has type of 
We can then apply 
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.
-calculus/combinators and a finite automata model of computation.
-Algebra
:FG -> 1d
x,y,z. x(yz)=(xy)z
)
= function composition
= diagonalise
= ![\label{eq9}\left[ 3 \right]](images/3593937028497067977-16.0px.png "\label{eq9}\left[ 3 \right]") | (9) |
I1:List Integer := [1,2]
![\label{eq10}\left[ 1, \: 2 \right]](images/8560831852088961606-16.0px.png "\label{eq10}\left[ 1, \: 2 \right]") | (10) |
I2:List Integer := [3,4, 5]
![\label{eq11}\left[ 3, \: 4, \: 5 \right]](images/9127597459900288712-16.0px.png "\label{eq11}\left[ 3, \: 4, \: 5 \right]") | (11) |
J1:=mult(I1,I2)$MonadList(Integer)
![\label{eq12}\left[ 1, \: 2, \: 3, \: 4, \: 5 \right]](images/6001987805961962306-16.0px.png "\label{eq12}\left[ 1, \: 2, \: 3, \: 4, \: 5 \right]") | (12) |
J2:=join([I1,I2])$MonadList(Integer)
![\label{eq13}\left[ 1, \: 2, \: 3, \: 4, \: 5 \right]](images/5413933420029064711-16.0px.png "\label{eq13}\left[ 1, \: 2, \: 3, \: 4, \: 5 \right]") | (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]]
![\label{eq14}\left[{\left[ A \right]}, \:{\left[ B \right]}\right]](images/2296727626696617921-16.0px.png "\label{eq14}\left[{\left[ A \right]}, \:{\left[ B \right]}\right]") | (14) |
M2b := [[C],[D]]
![\label{eq15}\left[{\left[ C \right]}, \:{\left[ D \right]}\right]](images/5696271978829973832-16.0px.png "\label{eq15}\left[{\left[ C \right]}, \:{\left[ D \right]}\right]") | (15) |
concat[concat M2a,concat M2b] = concat(concat[M2a, M2b])
![\label{eq16}{\left[ A , \: B , \: C , \: D \right]}={\left[ A , \: B , \: C , \: D \right]}](images/4131301370787433030-16.0px.png "\label{eq16}{\left[ A , \: B , \: C , \: D \right]}={\left[ A , \: B , \: C , \: D \right]}") | (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:
- 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:
Outer := join([[[1,2], [3, 4]], [[5, 6]]])$MonadList(List Integer)
![\label{eq17}\left[{\left[ 1, \: 2 \right]}, \:{\left[ 3, \: 4 \right]}, \:{\left[ 5, \: 6 \right]}\right]](images/3008614566949830147-16.0px.png "\label{eq17}\left[{\left[ 1, \: 2 \right]}, \:{\left[ 3, \: 4 \right]}, \:{\left[ 5, \: 6 \right]}\right]") | (17) |
Then we can join the rest:
join(Outer)$MonadList(Integer)
![\label{eq18}\left[ 1, \: 2, \: 3, \: 4, \: 5, \: 6 \right]](images/6870536118186174174-16.0px.png "\label{eq18}\left[ 1, \: 2, \: 3, \: 4, \: 5, \: 6 \right]") | (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)]
![\label{eq19}\left[{\left[ 1, \: 2, \: 3, \: 4 \right]}, \:{\left[ 5, \: 6 \right]}\right]](images/607368336104088508-16.0px.png "\label{eq19}\left[{\left[ 1, \: 2, \: 3, \: 4 \right]}, \:{\left[ 5, \: 6 \right]}\right]") | (19) |
join(Inner)$MonadList(Integer)
![\label{eq20}\left[ 1, \: 2, \: 3, \: 4, \: 5, \: 6 \right]](images/5672663921592228757-16.0px.png "\label{eq20}\left[ 1, \: 2, \: 3, \: 4, \: 5, \: 6 \right]") | (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 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.