Dear Martin,
sorry for a shallow answer to your long mail, I am running against a
deadline....
First I tried to find where MONAD is defined in fricas, unfortunately
the command
(2) -> )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) (T,mu,eta) is a triple
consisting of an
endo_functor_ T : C --> C on a category C, a multiplication m : T T
---> T and a unit
eta : C --> TC such that eta is the unit, and mu is associative
(defined by some diagrams)
Let X be an object in C, then the natural transformations mu and eta
have components mu_X and eta_X, which you seem to address (and the
MONAD thing in AXIOM), this may be instantiated as a monoid (see the
book by
Arbib_Michael-Manes_E-Arrows_structures_and_functors._The_categorical_imperative-Academic_Press(1975))
which has lots of examples (power set, list, ...)
A monad as in Haskel operates on the category (including function types)
> First test for List being monad (monad for a monoid) with:
> \mu = concat
> \eta = list
> T = []
?? Monad =\= monoid.
Math: A monoid is a set X with two operations mu : X x X --> X and
unit E s.t. mu (E x X) = X = mu(X x E).
I don't see why this should come with an `fmap' function (functoriality of T)
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 : Set --> T Set, where
T Set is lists of sets.
Now T T Set is lists of lists of sets, eg, [[X,Y],[Y],[X],[Z,W]] :: T
T Set ; then the `multiplication'
mu : T T --> T is `flatening the lists' e.g. forgetting the inner
list's brackets -> [ X,Y,Y,X,Z,W]
Associativity of m guarantees that if you have lists of lists of lists
of sets (type T T T Set)
then either of the two ways to forget the inner brackets (multiplying
the monad functor T)
gives the same result. The left/right unit of this multiplication is
the empty list
mu : [[],[X]] --> [X]
The difference is that this construction is much more like a
template class in C++, as it can be instantiated on any (suitable)
category C. And this is what the list constructor actually does...
> So I will check that the identities for monads are satisfied
Yes, for lists that follows from the above definition...
> \begin{verbatim}
> )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
> @
> \end{verbatim}
Indeed, A and B should be objects in the base category, so they have
the same `type'
(above A, B :: Set) . The A-->B is in Hom(A,B) = Set(A,B), the class
of all functions from
set A to set B, fmap allows to apply f inside the container T, and
mult is actually used to
flatten the container as types of type T T Set (say) appear under
composing maps,
as in unit o unit: A --> T T A
> It compiles but it doesn't look very useful?
It just defined what a monad is (provided you make sure in an
implementation that your functor fulfils the correct associativity and
unit laws. AXIOM checks in MONADWU (Monad with unit, ?)
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
> \begin{verbatim}
> \item T:(MonadCat)-> MonadCat
> \end{verbatim}
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)
> \begin{verbatim}
> TList(A:Type) : Exports == Implementation where
> ...
> Rep := List A
> \end{verbatim}
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, .....
Cheers
BF.
--
quam cito dictur, tam facile non fit!
% Dr habil Bertfried Fauser
% Research Fellow, School of Computer Science, Univ. of Birmingham
% Honorary Associate, University of Tasmania
% contact |-> URL : http://www.cs.bham.ac.uk/~fauserb/
% Phone : +44-121-41-42795
--
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To post to this group, send email to fricas-devel@googlegroups.com.
To unsubscribe from this group, send email to
fricas-devel+unsubscr...@googlegroups.com.
For more options, visit this group at
http://groups.google.com/group/fricas-devel?hl=en.
