On Wed, Nov 9, 2011 at 2:45 AM, Ralf Hemmecke wrote:
> Looking at http://en.wikibooks.org/wiki/Haskell/Category_theory#Monads and
> my previous attempt to model it in Aldor...
> http://groups.google.com/group/fricas-devel/msg/38e7d6dca39cc46c
>
> Actually, now I believe that
>
> #include "aldor"
> Monad(C: Category, A: C, M: C -> C): Category == with {
> unit: A -> M A;
> mult: M M A -> M A;
> }
>
> is not the way one would naturally do this in Aldor.
>
What precisely do you think is wrong with what you wrote?
Although objections might be raised about the passing of categories as
parameters (see Gaby's comments), I think that in principle the syntax
and semantics of this is well defined even if not necessarily
implemented in all versions of Axiom.
For me the issue is this parameter:
M: C -> C
The natation 'C -> C' is sugar for Mapping(C,C) so here M is declared
as a function. But later you use it as a domain constructor
unit: A -> M A
Here M is clearly a 'functor'. The distinction between function and
functor is very basic to the design of Axiom goes back to the very
beginning of the project as shown in the references I gave earlier.
One should keep in mind the differences:
- A function returns a value in some domain.
- A functor returns a domain in some category.
A domain is a named set of slots containing pointers to operators
(functions). A category is a named template giving the names and types
(signatures) of a set of operators. Applying the functor M to domain A
is expected to yield a set of slots, not a value in some domain.
> Also
>
> Monad(C: Category, 1: C -> C, M: C -> C): Category == with {
> unit: 1 -> M;
> mult: (M, M) -> M;
> }
>
> doesn't look correct.
>
I don't understand your motivation for introducing this variant. Now
'1' also is declared as a function but in
unit: 1 -> M
you are using it as a domain.
> What
>
> class Monad m where
> unit :: a -> m a
> mult :: m (m a) -> m a
>
> actually says, is to attach to a type m (or in Axiom terms a domain
> constructor m) the "property" "being a Monad" where "m being a monad"
> just means that there are the two functions unit and mult with the respective
> signature.
>
How is this different than the usual declaration of a domain
constructor in Axiom? E.g. In
http://fricas.svn.sourceforge.net/viewvc/fricas/trunk/src/algebra/gaussian.spad.pamphlet?revision=1196&view=markup
we have:
565 Complex(R:CommutativeRing): ComplexCategory(R)
where ComplexCategory(R) joins other categories such as
MonogenicAlgebra(R, SparseUnivariatePolynomial R), etc.
27 ComplexCategory(R:CommutativeRing): Category ==
28 Join(MonogenicAlgebra(R, SparseUnivariatePolynomial R),
FullyRetractableTo R,
"Being a Monad" is just another category to be associated with some
constructor. Why not?
> I'd say: This is not possible, neither in Aldor nor in SPAD. If I look at my
> code above, I have M as a parameter. But I am just going to define the
> identifier "Monad", so M cannot yet be a monad.
This analysis does not make sense to me. It seems to me that you are
just talking about type declarations. Nothing more.
> I only can turn a domain constructor D into a monad by saying something like
>
> extend D(...): Monad(...) == add {...} -- Note that D has a parameter.
>
> I think that the true equivalent of the above Haskell code would be
> something like this.
>
> Monad(C: Category)(A: C): Category == with {
> unit: A -> %(A);
> mult: %(%(A)) -> %(A);
> }
>
> where as usual % mean THIS-DOMAIN. The above code is, however, not proper
> Aldor code. One reason is that % stands for a domain, not a domain
> constructor (i.e. a function that takes a parameter and returns a domain).
> So % cannot be applied to anything.
>
Your claim here is very strange to me. I do not see anything unusual
about the use of % to represent a domain constructor in the code of
Complex above.
> I don't actually see how one can solely speak about domain constructors.
>
> And even if the above were possible, I don't see how it would help to reuse
> code. My code above is just a category after all with no default
> implementation.
>
The problem as I see it is the passing of a functor as a parameter. I
want to use the terminology this way for example: 'Complex' is a
functor. 'Complex(Integer)' is a domain constructor, i.e. the
application of a functor to its argument. A functor is "like" a
function but differs in that it does not return a value in any domain.
I do not see anyway in Axiom or in Aldor to specify the type of a
functor that would be analogous to the way we specify the type of a
function. If we were to use
M: C -> C
as you do above the implication is that in this context -> refers to
something different than 'Mapping'.
Forget the issue of passing a category as a parameter for now (e.g.
assume SetCategory).
Without introducing a new meaning for ->, one way to specify the type
of a functor parameter might be the following:
Monad(A: SetCategory, M(A):SetCategory): Category == with {
unit: A -> M A;
mult: M M A -> M A;
}
Here the use of M(A) on the left of colon : is novel and not currently
supported in any variant. But I think the semantics are quite clear.
One might instantiate this category as in the follow domain:
IMList(): Monad(Integer,List) == add
unit ( x:Integer ): List Integer == list x
mult ( x: List List Integer ): List Integer = concat x
Of course this seems a little "useless" because 'list' and 'concat'
are already a part of ListAggregate category. But if this was not the
case, we would turn this around and declare ListAggregate to be a
Monad.
Regards,
Bill Page
--
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.
