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 definitionIf 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):
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 are effectively the same but I've used a different
form So I will check that the identities for monads are satisfied. First something to work with: fricas (1) -> 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 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 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) 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
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
is sometimes called the is sometimes called the 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 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 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. -Algebra A set of operator symbols, each operator has an F-Algebra and F-CoalgebraF-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 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-AlgebrasA 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. OperationsHow 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 AdjointsAlgebraic constructsA method where one algebraic entity is constructed from another. A (co)algebra is defined
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 Eilenberg-Moore case the algebra is a category with objects represented by a pair: (X,Ex: TX->X) where:
(Co)Algebra Example 1 - Natural NumbersNatural 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:
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 - GroupsA 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. Group defined as a co-algebra:
where:
spad )abbrev category MONADC MonadCat MonadCat(A : Type, spad Compiling FriCAS source code from file /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/3446447770260162759-25px013.spad using old system compiler. MONADC abbreviates category MonadCat ------------------------------------------------------------------------ initializing NRLIB MONADC for MonadCat compiling into NRLIB MONADC fricas )show MonadCat spad )abbrev package MONADL MonadList MonadList(A:Type): MonadCat(A, spad Compiling FriCAS source code from file /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/2154926742186104936-25px015.spad using old system compiler. Illegal NRLIB MONADLNRLIB 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. fricas )show MonadList(Integer) fricas L := unit(3)$MonadList(Integer)
Type: List(Integer)
fricas I1:List Integer := [1,
Type: List(Integer)
fricas I2:List Integer := [3,
Type: List(Integer)
fricas J1:=mult(I1,
Type: List(Integer)
fricas J2:=join([I1,
Type: List(Integer)
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: fricas M2a := [[A],
Type: List(List(Symbol))
fricas M2b := [[C],
Type: List(List(Symbol))
fricas concat[concat M2a,
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:
So, starting in T^3, mult/join needs to go from:
We can do it, this will concatenate the outer lists: fricas Outer := join([[[1,
Type: List(List(Integer))
Then we can join the rest: fricas join(Outer)$MonadList(Integer)
Type: List(Integer)
I'm not sure how we can concatenate the inner list first? (Bill) How's this: fricas Inner := [join([[1,
Type: List(List(Integer))
fricas join(Inner)$MonadList(Integer)
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 join()$MonadList(Integer) and for join()$MonadList(List Integer) so what form would Is there any way that we could include the endofunctor Or alternatively, could the functionality of I assume there is no way that we can enforce these axioms in 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. |