Monads in FriCAS
Bill Page
> 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).
>
> As far as I can see there is already an SPAD domain 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 generalise it.
>
> ...
I added Martin Baker's example monad code here:
http://axiom-wiki.newsynthesis.org/SandBoxMonads
I've re-organized it a little and added some references. Maybe it is a
little easier to follow that the original email. Free free to
experiment with it online, extend it or add comments, etc.
Regards,
Bill Page.
Bertfried Fauser
well done, I'll have a look at it
Cheers
BF.
--
% PD Dr Bertfried Fauser
% Research Fellow, School of Computer Science, Univ. of Birmingham
% Honorary Associate, University of Tasmania
% Privat Docent: University of Konstanz, Physics Dept
<http://www.uni-konstanz.de>
% contact |-> URL : http://www.cs.bham.ac.uk/~fauserb/
% Phone : +44-121-41-42795
Martin Baker
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:
MonadCat(A:Type,T: Type->Type) : Category == with
X ==> Union(A,T X)
unit :X -> T X
mult :T ( T X) -> T X
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
Martin Baker
> sorry for a shallow answer to your long mail, I am running against a
> deadline....
Not at all, any information you can give is very useful. I hope you
don't mind as I have copied most of your reply to the page Bill
created at:
http://axiom-wiki.newsynthesis.org/SandBoxMonads
I hope this is OK, its just that I thought it would be useful to have
all the relevant information together in one place.
I have added some further stuff of my own, at the end of the page,
about the relationship between monads and algebras (and therefore why
I think is it very important to support monads in a CAS like FriCAS).
I am hoping that those more knowledgeable than me will look at the
page and suggest ways to implement this.
Thanks,
Martin
Martin Baker
> 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 how would this be implemented?
Lists might be implemented, in a co-data structure, like this:
.... domain List(S) ....
Rep := Union(Empty,Record(%,S))
and we could define PowerList, in a co-data structure, as:
.... domain PowerList(S) ....
Rep := Union(S,List %)
eta:(%) -> List %
mu:(List List %) -> List %
But here % is an instance of PowerList(S) and List % is also an
instance of PowerList(S) so does eta:(%) -> List % actually enforce an
increment in the nesting level or would we have to write eta:(%) -> %
and enforce a step in the nesting in the implementation?
If this is valid then the next step would be to generalise from List
to T
.... domain Monad(S,T) ....
Rep := Union(S,T %)
eta:(%) -> T %
mu:(T T %) -> T %
Martin
Ralf Hemmecke
> I find myself wanting a way to define types inductively like this:
>
> X := Union(A,T X)
Have you studied Aldor-Combinat? I'm not sure whether it helps you with
monads, though. But it has some code to define inductive types...
Ralf
Martin Baker
I have had a quick look at:
http://www.risc.jku.at/people/hemmecke/AldorCombinat/
It looks very interesting and it is one of the things I have been
intending to get back to and study in more detail.
Just looking at some of your description, for instance:
"Speaking in terms of category theory, a combinatorial species is
nothing but an endofunctor F : B -> B from the category B of finite
sets and bijections to itself."
It looks like there may be a lot of commonalty between what we are
both trying to do?
Could you point me to the part which deals with defining inductive
types?
Also I would be interested in your more general views on the
suitability of certain languages for this type of programming. Are
there language features that I should be asking for in SPAD that would
make modelling this type of mathematics more practical? (well I can
ask).
I'm only guessing here but, for some reason, I suspect you may be keen
on Aldor language features such as 'dependant parameters'? However
although it is useful, it doesn't seem to be enough. For example Saul
Youssef code at:
http://axiom-wiki.newsynthesis.org/SandBoxAldorCategoryTheoryCategories?root=SandBox%20Aldor%20Category%20Theory
seems less than ideal?
What I would really like to work out is why things like this Haskell
code:
class Monad m where
unit :: a -> m a
mult :: m (m a) -> m a
which are so powerful seem to be hard to do in SPAD related languages?
Could it be that SPAD and Haskell are complementory, SPAD is better
for maths that is characterised in a set-theoretic way and Haskell is
better for maths that is characterised in a category-theoretic way?
Then we should not try to force a single language to do both? I'm not
saying I have come to this conclusion, I just don't know.
It would help if I understood what it is about the above Haskell class
that makes it so difficult to represent in SPAD. Is it somthing about
allowing partial types to be combined to form a complete type? I just
can't work it out.
Martin
Ralf Hemmecke
> Could you point me to the part which deals with defining inductive
> types?
No. The definition of inductive types is entirely inherited from Aldor.
Search for the section "Test Recursive Structures".
You'll find something like
testRecursive1(): () == {
macro {
E == EmptySetSpecies;
X == SingletonSpecies;
+ == Plus;
* == Times;
}
A(L: LabelType): CombinatorialSpecies L == (E + X*A*A)(L) add;
check(
A,
[1, 1, 4, 30, 336, 5040],
[1, 1, 2, 5, 14, 42],
[1, 1, 2, 5, 14, 42]
);
}
And the line that starts with A(...) is all to define an inductive type.
(I only used macros to make it look nicer.)
At the beginning I had some problem, but the "add" at the end of the
line makes this whole definition lazy and thus working.
I have not yet tried something like this in SPAD. And as you can see, in
this particular case, the result type depends on the input L.
> Also I would be interested in your more general views on the
> suitability of certain languages for this type of programming.
I'm currently looking deeper into Haskell, but my interest is more the
algebraic part not so much higher categorial stuff. So my view might not
count for your interest.
Anyway, being lazy, Haskell has some nice and simple ways to define
recursive structures. But I still think, it's not suitable for Computer
Algebra.
Maybe an advantage of Aldor/SPAD in contrast to Haskell is the two level
type hierarchy, i.e. domains vs. categories. Maybe I don't yet know
Haskell well enough, but I don't see it in Haskell.
> example Saul Youssef code at:
> http://axiom-wiki.newsynthesis.org/SandBoxAldorCategoryTheoryCategories?root=SandBox%20Aldor%20Category%20Theory
>seems less than ideal?
This is very advanced code that stresses the compiler. I don't know what
in particular one can actually compute with it, but it's nice to see
Aldor's expressiveness.
> What I would really like to work out is why things like this Haskell
> code:
>
> class Monad m where
> unit :: a -> m a
> mult :: m (m a) -> m a
>
> which are so powerful seem to be hard to do in SPAD related languages?
Does the above express something similar to
#include "aldor"
Monad(C: Category, A: C, M: C -> C): Category == with {
unit: A -> M A;
mult: M M A -> M A;
}
? That's compiling in Aldor, but as such is pretty useless. You would
have to give some implementation of that category.
But what I've written above, is actually not really, what I imagine you
want. In fact, in the end, you might want something like this:
Monad(C: Category, 1: C -> C, M: C -> C): Category == with {
unit: 1 -> M;
mult: (M, M) -> M;
}
(which doesn't compile in aldor).
> It would help if I understood what it is about the above Haskell
> class that makes it so difficult to represent in SPAD. Is it somthing
> about allowing partial types to be combined to form a complete type?
> I just can't work it out.
The Haskell class alone doesn't help much. What do you want to achieve?
You might want to write a Haskell program (with monads) and explain what
it does and only then we can try to represent it in SPAD.
Ralf
Bill Page
I think this is a very good exercise for both the SPAD compiler and
for the application of category theory in Axiom and it's derivatives.
The following code "almost compiles" in FriCAS and the way it fails
illustrates some problems in both SPAD and Aldor:
First 'Category' is not a known type in FriCAS (It is a type in
OpenAxiom! and in Aldor). So instead of 'Category' I wrote 'Type'.
But the output of the command ')show MonadCat2' already suggests that
something is going wrong. If MonadCat2 is compiled with Aldor using
Category then things look better but we still run into problems later
when trying to instantiate this category.
There always has been a problem at the top of the type hierachy in
Axiom. Various flavors have tried to solve this - all unsuccessfully,
I think.
Second, we are trying to pass the functor M as a parameter.
Specifying this is a currently very awkward in both SPAD and Aldor.
What Ralph wrote involves passing a function which returns domain. In
Axiom and it's derivatives this is not the same thing as a domain
constructor (= functor). This is a rather deep issue in the
fundamental design of SPAD and Aldor where types are supposed to be
static and I am not sure if it was ever fully resolved. Maybe
OpenAxiom has made some progress here as well?
--
)abbrev category MONADC MonadCat2
MonadCat2(C: Type, A : C, M: C -> C): Category == with
unit: A -> M A
mult: (M A, M A) -> M A
--
)show MonadCat2
MonadCat2(C: Type,A: t#1,M: (t#1 -> t#1)) is a category constructor
Abbreviation for MonadCat2 is MONADC
This constructor is exposed in this frame.
------------------------------- Operations --------------------------------
mult : (M(A),M(A)) -> M(A) unit : A -> M(A)
In principle would could instantiate MonadCat2 as follows:
MonadCat2(SetCategory, Integer, (X:SetCategory):SetCategory+->List X)
but we can not write this in FriCAS, so try to use Type instead.
--
)abbrev domain MONDIL MonadIntegerList
MonadIntegerList(): MonadCat2(Type, Integer, (X:Type):Type+->List X) == add
unit(x:Integer):List Integer == list(x)
mult(x:List Integer,y:List Integer):List Integer == concat(x,y)
--
Notice here that I explicitly attempted to construct a function which
returns a domain:
(X:SetCategory):SetCategory +-> List X
'List' is the domain constructor (functor), but both FriCAS and Aldor
complain in various ways. Maybe someone else can find a variant that
does compile?
Regards,
Bill Page.
> Martin Baker wrote:
>> What I would really like to work out is why things like this Haskell
>> code:
>>
>> class Monad m where
>> unit :: a -> m a
>> mult :: m (m a) -> m a
>>
>> which are so powerful seem to be hard to do in SPAD related languages?
Martin Baker
> #include "aldor"
> Monad(C: Category, A: C, M: C -> C): Category == with {
> unit: A -> M A;
> mult: M M A -> M A;
> }
>
> ? That's compiling in Aldor, but as such is pretty useless. You would
> have to give some implementation of that category.
>
> But what I've written above, is actually not really, what I imagine you
> want. In fact, in the end, you might want something like this:
>
> Monad(C: Category, 1: C -> C, M: C -> C): Category == with {
> unit: 1 -> M;
> mult: (M, M) -> M;
> }
As I mentioned before, I have a suspicion that this has something to
do with partial types such as 'List' as opposed to a full type like
'List Integer'. So M would be a partial type:
Monad(A: Type, M: partialType): Category == with {
unit: A -> M o A
mult: M o M o A -> M o A
}
Where 'o' means apply partial (or full) type to a type to give another
type. So this would need a way to pass a partial type to a category
and a way to combine it with other types. Of course a partial type M
could not be used on its own, only after it has been combined with
other types.
The advantage of this over the dependant parameter method above is
that we don't need to define the category C and it looks (in my non-
expert opinion) to be closer to the way Haskell works.
I don't know what would be easier to implement in SPAD, partial types
or dependant parameters? Or if either would ever be practical?
The important point is that we need to be able apply M not only to
types like A but also to types like A->A so we get:
M o unit = M o A -> M o M o A
M o mult =M o M o M o A -> M o M o A
Martin
Gabriel Dos Reis
[...]
Bill --
I think this essentially goes back to a discussion we had recently. I
am not sure I succeeded in getting my points trough:-)
Yes, functors and category constructors are functions, but they are not
ordinary functions. In general type constructor (in SPAD or any ML
descendent, which includes Haskell) and data constructors are special
functions. In terms of formal semantics, they are not reducible.
This is a very important point. That allows the compiler to internally
reason on some usage, including deciding equality when type checking an
expression.
At the moment, all AXIOM variants do not allow you to pass a category as
a parameter in a domain or category definition -- well, you can in
OpenAxiom but the usage then is limited. As a consequence,
you can't introduce a category as a parameter and a domain parameter
depending on the category parameter and expect anything useful to come
out. In your definition of MonadCat2, the compiler internally assumes
that the parameter 'C' designates a domain -- not a category as you
intended -- because its type is a category. You can check that by
looking at the dual signature (or COSIG property of the DB) of MonadCat2.
So, your attempt to call it with SetCategory for C is a type violation.
All AXIOM compilers assume that when they see a category form, the
head is a category constructor, not an arbritrary function (or
parameter) that may evaluate at runtime to a category. This allows the
compiler to type check domains. The story is almost the same for
domain forms in certain situations. See the roundabout hack in
the implementation of Table (table.spad.pamphlet) just to conditionally
select the representation domain (InnerTable.) OpenAxiom's compiler
tried to improve on the situation, but only marginally at the moment.
But, whatever is done there is no way around the fact that a constructor
is not an ordinary function -- being in Haskell or in Spad.
-- Gaby
Ralf Hemmecke
> unit: A -> M o A
> mult: M o M o A -> M o A
> }
Everything must have a type. Do you mean that partialType is a built-in
type that allows application? What would be the return type then?
It's not going to work that way in SPAD. You have to be very explicit
about types.
Ralf
Martin Baker
Perhaps if I give a concrete example:
Monad(String,List)
would have:
unit: String -> List String
mult: List List String -> List String
Martin
Ralf Hemmecke
> ordinary functions. In general type constructor (in SPAD or any ML
> descendent, which includes Haskell) and data constructors are special
> functions. In terms of formal semantics, they are not reducible.
Maybe this is also the reason why
#include "aldor"
Monad(C: Category, 1: C -> C, M: C -> C): Category == with {
unit: 1 -> M;
mult: (M, M) -> M;
}
does not compile in Aldor? Or would that just be a weakness of the
compiler implementation?
Not that I need that now, but is there a chance that it will work some
time in the future?
In fact, -> is the same as the Domain constructor Map, the only problem
is that Map requires domains as input, not categories like the C above.
So indeed my code should give a type error.
Maybe that can only be solved by allowing more general parameters for ->
or introducing a special constructor CategoryMap, which takes categories
as arguments.
Ralf
aldor monad.as
"monad.as", line 3: unit: E -> M;
........^....^
[L3 C9] #6 (Error) There are 0 meanings for `E' in this context.
The possible types were:
E: C -> C, a local
The context requires an expression of type Tuple(Type).
[L3 C9] #8 (Error) Argument 1 of `->' did not match any possible
parameter type.
The rejected type is C -> C.
Expected type Tuple(Type).
[L3 C14] #1 (Error) There are 0 meanings for `M' in this context.
The possible types were:
M: C -> C, a local
The context requires an expression of type Tuple(Type).
"monad.as", line 4: mult: (M, M) -> M;
.........^
[L4 C10] #3 (Error) Have determined 1 possible types for the expression.
Meaning 1: C -> C, C -> C
The context requires an expression of type Tuple(Type).
[L4 C10] #5 (Error) Argument 1 of `->' did not match any possible
parameter type.
The rejected type is C -> C, C -> C.
Expected type Tuple(Type).
Ralf Hemmecke
Can you give an argument why a compiler would accept your expression,
but reject
Monad(String, Map)
or
Monad(String, Fraction)
?
In SPAD such things are decided at compile time, not runtime.
Ralf
Martin Baker
Monad(A: Type, M: partialType): Category == with {
unit: A -> M o A
mult: M o M o A -> M o A
}
Monad(String, Fraction)
It would not be detected as an error at that stage because it would
not do the substiutions inside Monad and see that 'Fraction String' is
not a valid type. Perhaps this is another difference between SPAD and
Haskell?
In that case I guess it would need some extra syntax to enforce this
better, perhaps a symbol that means 'can-be-applied-to' like this:
Monad(M: partialType can-be-applied-to A or M): Category == with {
mult: M o M o A -> M o A
}
Bill Page
I do not know what you mean by "partial types such as 'List' as
opposed to a full type like 'List Integer' ". 'List' is not "partial"
any more than "f' is partial when you would normally write "f(x)".
'List' is a domain constructor. Domain constructors in Axiom are also
often called functors for the same reason that functors are called
functors in Haskell.
'List Integer' is not a "full type", rather it is the domain
constructor 'List' applied to the argument 'Integer', i.e. a domain
constant.
Regards,
Bill Page.
On Tue, Nov 8, 2011 at 10:32 AM, Martin Baker <ax8...@martinb.com> wrote:
> ...
Bill Page
> ...
> | Second, we are trying to pass the functor M as a parameter.
> | Specifying this is a currently very awkward in both SPAD and Aldor.
> | What Ralph wrote involves passing a function which returns domain. In
> | Axiom and it's derivatives this is not the same thing as a domain
> | constructor (= functor). This is a rather deep issue in the
> | fundamental design of SPAD and Aldor where types are supposed to be
> | static and I am not sure if it was ever fully resolved. Maybe
> | OpenAxiom has made some progress here as well?
> |
On Tue, Nov 8, 2011 at 10:44 AM, Gabriel Dos Reis wrote:
>
> I think this essentially goes back to a discussion we had recently. I
> am not sure I succeeded in getting my points trough:-)
>
Yes, I have been listening. I think I understand this in the context
of the changes that you have made to OpenAxiom.
> Yes, functors and category constructors are functions, but they are not
> ordinary functions. In general type constructor (in SPAD or any ML
> descendent, which includes Haskell) and data constructors are special
> functions. In terms of formal semantics, they are not reducible.
> This is a very important point. That allows the compiler to internally
> reason on some usage, including deciding equality when type checking an
> expression.
>
Do you think we should be allowed to write something like the
following in the OpenAxiom compiler (SPAD)?
(X:Domain):Domain+->List X
i.e. define a function that takes a domain as an argument and returns
a domain? Could we use such a thing in a statically typed language? I
suppose not.
> At the moment, all AXIOM variants do not allow you to pass a category as
> a parameter in a domain or category definition -- well, you can in
> OpenAxiom but the usage then is limited. As a consequence,
> you can't introduce a category as a parameter and a domain parameter
> depending on the category parameter and expect anything useful to come
> out. In your definition of MonadCat2, the compiler internally assumes
> that the parameter 'C' designates a domain -- not a category as you
> intended -- because its type is a category. You can check that by
> looking at the dual signature (or COSIG property of the DB) of MonadCat2.
> So, your attempt to call it with SetCategory for C is a type violation.
>
It is not so clear to me that Aldor intended to duplicate this part of
the Axiom semantics.
> All AXIOM compilers assume that when they see a category form, the
> head is a category constructor, not an arbritrary function (or
> parameter) that may evaluate at runtime to a category. This allows the
> compiler to type check domains. The story is almost the same for
> domain forms in certain situations. See the roundabout hack in
> the implementation of Table (table.spad.pamphlet) just to conditionally
> select the representation domain (InnerTable.) OpenAxiom's compiler
> tried to improve on the situation, but only marginally at the moment.
>
Yes, that is interesting.
> But, whatever is done there is no way around the fact that a constructor
> is not an ordinary function -- being in Haskell or in Spad.
>
Yet in Haskell we do have functors and monads ... One question being
asked here is "what is required in Axiom (and/or its descendants) to
do something equivalent?
Regards,
Bill Page.
Gabriel Dos Reis
| Bill Page <bill...@newsynthesis.org> writes:
| > ...
| > | Second, we are trying to pass the functor M as a parameter.
| > | Specifying this is a currently very awkward in both SPAD and Aldor.
| > | What Ralph wrote involves passing a function which returns domain. In
| > | Axiom and it's derivatives this is not the same thing as a domain
| > | constructor (= functor). This is a rather deep issue in the
| > | fundamental design of SPAD and Aldor where types are supposed to be
| > | static and I am not sure if it was ever fully resolved. Maybe
| > | OpenAxiom has made some progress here as well?
| > |
|
| On Tue, Nov 8, 2011 at 10:44 AM, Gabriel Dos Reis wrote:
| >
| > I think this essentially goes back to a discussion we had recently. I
| > am not sure I succeeded in getting my points trough:-)
| >
|
| Yes, I have been listening. I think I understand this in the context
| of the changes that you have made to OpenAxiom.
Hmm, I am not sure I understand, but let's see.
| > Yes, functors and category constructors are functions, but they are not
| > ordinary functions. In general type constructor (in SPAD or any ML
| > descendent, which includes Haskell) and data constructors are special
| > functions. In terms of formal semantics, they are not reducible.
| > This is a very important point. That allows the compiler to internally
| > reason on some usage, including deciding equality when type checking an
| > expression.
| >
|
| Do you think we should be allowed to write something like the
| following in the OpenAxiom compiler (SPAD)?
|
| (X:Domain):Domain+->List X
|
| i.e. define a function that takes a domain as an argument and returns
| a domain? Could we use such a thing in a statically typed language? I
| suppose not.
In OpenAxiom, that depends on the context of usage.
| > At the moment, all AXIOM variants do not allow you to pass a category as
| > a parameter in a domain or category definition -- well, you can in
| > OpenAxiom but the usage then is limited. As a consequence,
| > you can't introduce a category as a parameter and a domain parameter
| > depending on the category parameter and expect anything useful to come
| > out. In your definition of MonadCat2, the compiler internally assumes
| > that the parameter 'C' designates a domain -- not a category as you
| > intended -- because its type is a category. You can check that by
| > looking at the dual signature (or COSIG property of the DB) of MonadCat2.
| > So, your attempt to call it with SetCategory for C is a type violation.
| >
|
| It is not so clear to me that Aldor intended to duplicate this part of
| the Axiom semantics.
I am not sure I understand; could you elaborate?
| > All AXIOM compilers assume that when they see a category form, the
| > head is a category constructor, not an arbritrary function (or
| > parameter) that may evaluate at runtime to a category. This allows the
| > compiler to type check domains. The story is almost the same for
| > domain forms in certain situations. See the roundabout hack in
| > the implementation of Table (table.spad.pamphlet) just to conditionally
| > select the representation domain (InnerTable.) OpenAxiom's compiler
| > tried to improve on the situation, but only marginally at the moment.
| >
|
| Yes, that is interesting.
|
| > But, whatever is done there is no way around the fact that a constructor
| > is not an ordinary function -- being in Haskell or in Spad.
| >
|
| Yet in Haskell we do have functors and monads ...
Yes, but I am not seeing the implication. Could you elaborate?
| One question being asked here is "what is required in Axiom (and/or
| its descendants) to do something equivalent?
Equivalent to what? I'm afraid I do not understand the description of the
thing being claimed to be in Haskell -- to remove any misunderstanding I
understand Haskell, but I do not understand the *claim* being made and what
"equivalent" is being sought.
Any clear elaboration of the original issue will help.
-- Gaby
Bill Page
variant including Aldor)? How does or how could the monad construction
in Haskell fit into Axiom?
> --
> 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...@googlegroups.com.
> To unsubscribe from this group, send email to fricas-devel...@googlegroups.com.
> For more options, visit this group at http://groups.google.com/group/fricas-devel?hl=en.
>
>
Martin Baker
> Martin,
>
> I do not know what you mean by "partial types such as 'List' as
> opposed to a full type like 'List Integer' ". 'List' is not "partial"
> any more than "f' is partial when you would normally write "f(x)".
> 'List' is a domain constructor. Domain constructors in Axiom are also
> often called functors for the same reason that functors are called
> functors in Haskell.
>
> 'List Integer' is not a "full type", rather it is the domain
> constructor 'List' applied to the argument 'Integer', i.e. a domain
> constant.
>
> Regards,
> Bill Page.
What I was trying to do was understand why powerful concepts like
monads can be easily used in Haskell but we are having problems
modelling them in SPAD. So I was trying to choose a level of language
that is general enough to apply accross different computer languages
but specific enough so that we can compare it with SPAD.
If you are going to insist that the only definition of something like
'List' in this context is a 'domain constructor' then how can we
compare different languges?
I guess that if you want to limit this discussion to precise
definitions then I guess they should come from type theory rather than
something language specific?
Martin
Gabriel Dos Reis
| How can I implement Haskell monads in OpenAxiom (or any other Axiom
| variant including Aldor)? How does or how could the monad construction
| in Haskell fit into Axiom?
OK. Show me your version of Haskell monad -- the reason I am asking is
that there are many things people call "monad" (including in Haskell)
and it would be not productive that I second guess what you meant.
-- Gaby
Bill Page
I think precise definitions are essential to make any progress in
understanding this issue. My preference is that these definitions
should come from category theory. In this case, specifically the
definition of monad in category theory. Prior to that is the
definition of functor in category theory. Before asking about monads,
I think it is important first to ask about functors. The point of my
last message is that 'List' is a functor. I hope that was clear.
Regards,
Bill Page.
Bill Page
http://en.wikibooks.org/wiki/Haskell/Category_theory
will suffice for my purpose, especially when expressed in terms of
'unit' and 'join'. Is that OK with you?
Gabriel Dos Reis
| I think the definition given here:
|
| http://en.wikibooks.org/wiki/Haskell/Category_theory
|
| will suffice for my purpose, especially when expressed in terms of
| 'unit' and 'join'. Is that OK with you?
No. Because you are still asking me to second-guess what you meant.
I am very willing to discuss the specifics of how this and that
construct in Haskell is or is not available in SPAD, but you need to
come forward with a specific example. Another reason is that that wiki
uses terminology slightly different from what we use in Spad (e.g. they
have a type class named Functor, but the equivalent of a type class in
Spad would be a category, their Functor is unary but there is no such
restriction in the terminology of Spad, etc.)
What I am asking, for the purpose of making progress on this apparently
recurrent and important issue, is that you put forward a specific
program example in Haskell and say exactly what you want. I am just
following through your previous statement "How can I implement Haskell
monads in OpenAxiom".
I want to see your Haskell monads, so that I can discuss how they relate
to OpenAxiom notions. It isn't a trick question. It is just that there
are so many things out there that one easily mistakes something for
another thing. Hope that clears things a big.
Martin Baker
> Martin,
>
> understanding this issue. My preference is that these definitions
> should come from category theory. In this case, specifically the
> definition of monad in category theory. Prior to that is the
> definition of functor in category theory. Before asking about monads,
> I think it is important first to ask about functors. The point of my
> last message is that 'List' is a functor. I hope that was clear.
>
> Regards,
> Bill Page.
concepts in various computer languages. Are you now saying that all
these language concepts have now to be redefined in category theory
terms?
Your last message defined List as a domain constructor, now you are
defining it: 'List' is a functor, I only point out this inconsistency
to point out that there is a limit to precision in natural language
and if you trying to over prescribe the language it has the effect of
narrowing the scope of the discussion and missing possible
alternatives.
Martin
Bill Page
> On Tuesday 08 Nov 2011 18:59:04 Bill Page wrote:
>> Martin,
>>
>> I think precise definitions are essential to make any progress in
>> understanding this issue. My preference is that these definitions
>> should come from category theory. In this case, specifically the
>> definition of monad in category theory. Prior to that is the
>> definition of functor in category theory. Before asking about monads,
>> I think it is important first to ask about functors. The point of my
>> last message is that 'List' is a functor. I hope that was clear.
>>
>> Regards,
>> Bill Page.
>
> But we are trying to understand how to implement these category theory
> concepts in various computer languages.
Yes.
> Are you now saying that all these language concepts have now to be
> redefined in category theory terms?
>
No.
> Your last message defined List as a domain constructor, now you are
> defining it: 'List' is a functor,
No. 'List' in SPAD is whatever 'List' is in SPAD. I am just saying
that it can be described mathematically as a functor. And following
that is the claim that it is also what is called a 'functor' in
Haskell.
> I only point out this inconsistency to point out that there is a limit to
> precision in natural language and if you trying to over prescribe the
> language it has the effect of narrowing the scope of the discussion and
> missing possible alternatives.
>
I don't really want to talk about what a 'List' is in general. I want
to do what you said at first:
"trying to understand how to implement these category theory concepts in
various computer languages".
Regards,
Bill Page.
Martin Baker
> to do what you said at first:
>
> "trying to understand how to implement these category theory concepts in
> various computer languages".
appear to have the concept of 'functor' built into the core of the
language then perhaps this might be modelled in the type system in the
way I described. It may well be that I'm just approaching what you
call 'domain constructors' from a different direction, I don't know,
but there is obviously no consensus about that terminology either.
Martin
Bill Page
Why do you say:
> It may well be that I'm just approaching what you
> call 'domain constructors' from a different direction, I don't know,
> but there is obviously no consensus about that terminology either.
The term 'domain constructor' is used throughout the Axiom Book:
http://axiom-wiki.newsynthesis.org/Mirrors?go=/public/book2.pdf&it=Axiom+Book
For example, section 2.1.1, page 131
If you given the command in Axiom
)show X
and X is a domain, then it says:
X is a domain constructor
...
As far as I know I am not using this term in any other way then it is
used in the Axiom Book. I have not heard anyone dispute the use of
this term.
The issue that I was discussing with Gaby earlier today involved
contrasting domain constructors with other types of functions in
Axiom. Again as far as I know there is no dispute about this
difference although it might be sufficiently subtle that not everyone
is aware of it. This is made a bit more complicated because to some
extent the Aldor language tries to minimize this difference.
Actual the word 'functor' as a synonym of domain constructor in the
context of category theory was used very early on in the design of
Axiom. See for example: Davenport, 1991:
http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.7694
(bottom page 11).
Regards,
Bill Page.
Bill Page
http://dl.acm.org/citation.cfm?id=988127
A language for computational algebra
Authors:
Richard D. Jenks IBM Research Center, Yorktown Heights, New York
Barry M. Trager IBM Research Center, Yorktown Heights, New York
Volume 16 Issue 11, November 1981
ACM New York, NY, USA
I've also put a copy here in case you don't have access to acm publications:
http://axiom-portal.newsynthesis.org/refs/articles/p22-jenks.pdf
Regards,
Bill Page.
Ralf Hemmecke
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.
Also
Monad(C: Category, 1: C -> C, M: C -> C): Category == with {
unit: 1 -> M;
mult: (M, M) -> M;
}
doesn't look correct.
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.
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.
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.
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.
Ralf
Martin Baker
> 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.
Monad are defined as typeclasses and then implemented in the standard
Haskell prelude:
class Functor f where
fmap :: (a -> b) -> f a -> f b
class Monad m where
(>>=) :: m a -> (a -> m b) -> m b
(>>) :: m a -> m b -> m b
return :: a -> m a
fail :: String -> m a
-- Minimal complete definition:
-- (>>=), return
m >> k = m >>= \_ -> k
fail s = error s
and then to go on to see how instances of it are used, perhaps the
simplest is the maybe monad:
instance Monad Maybe where
(Just x) >>= k = k x
Nothing >>= k = Nothing
return = Just
fail s = Nothing
The problem is that I think we are trying to do something different
from Haskell. Haskell is using this mostly as a tool to separate the
pure from the impure code but languages like SPAD don't try to do
that, I think we would be more interested in modelling the
mathematical concept of the monad and perhaps exploring its
relationship to T-algebras? (well that what I'm interested in).
So from the mathematical point of view we may need to keep in mind
that:
1) The above Monad typeclass is not built from the Functor in the way
that a mathematical monads is built from an (endo-)Functor (the above
typeclasses are separate).
2) 'return' above corresponds to what we have been calling 'unit' but
'>>=' does not quite correspond to what we have been calling 'mult'.
They have swapped things around a bit to make it easier to simulate
imperative code.
Martin
Bill Page
> 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
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
Gabriel Dos Reis
| 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.
I suspect the reason why it is not implemented is that the semantics may
not be well-defined in the AXIOM model. In that model, there is no
category variable/parameter and every category form is evaluated. See
uses of compMakeCategoryObject to type check domain forms.
One thing that is lost in this discussion is that Haskell does not have
type classes as parameters. The parameter to Monad is not an arbitrary
function, it is a type constructor. All attempts I have seen so far
have been busy trying to pass a category (what would be a type class in
Haskell) to a functor.
-- Gaby
Gabriel Dos Reis
[...]
| - A functor returns a domain in some category.
A point of precision: A category is not a representational type in the
way that a domain is. A category is a predicate.
-- Gaby
Bill Page
as such, consider instead
Monad(A: SetCategory, M: SetCategory -> SetCategory): Category == with {
unit: A -> M A;
mult: M M A -> M A;
}
Regards,
Bill Page
Bill Page
Agreed.
In early Axiom literature a category is sometimes referred to as a
"template" in as much as it prescribes (a subset of) the names and
types of operators to be exported by the domain are declared to
satisfy these categories. But categories also have names and as such
are intended to abstractly represent some property of mathematics or
data structures. Certainly
X has C
is a proposition (true or false) where X is a domain and C some
category, so ' _ has C' must be some kind of predicate.
It is conceivable to me that a notation such as
Monad(C:Category, ... )
could refer to C as formal parameter representing such a template.
But as I said earilier, I do not think this is an essential part of
this disucussion about Monad (at least not yet).
Regards,
Bill Page.
Gabriel Dos Reis
Sure. Sometimes syntation (notation) seems to take precedence over
content (semantics), or sometimes syntax is deceiving, so I was just
pointing that the notation
x: T
does not necessarily mean that x has a representational type T -- as
many people would "naively" think. That said, I am returning to
observational state.
-- Gaby
Gabriel Dos Reis
| Since this is a discussion of Monad and not categories as parameters
| as such, consider instead
|
| Monad(A: SetCategory, M: SetCategory -> SetCategory): Category == with {
| unit: A -> M A;
| mult: M M A -> M A;
| }
OK, then what is the question?
-- Gaby
Bill Page
2) If yes, is it useful? How to use it?
3) Why doesn't this compile? (Discussion of function versus functor.)
4) Is there another way to write it that does compile and that would
be a useful way to represent a monad-like construction in Axiom?
5) What would have to change (if anything) in Axiom to allow it or
something similar to compile?
6) Should we be able to pass functors as arguments, store them in
variables, etc. the way we do with functions (and as implied in the
original Axiom literature)?
7) What type (if any) should be associated with a functor?
Note: Here functor, like function, refers to a constructor that is
unapplied but applicable.
For example in OpenAxiom you have a Maybe domain presumably modeled
after Haskell (or perhaps modeled after whatever the Haskell Maybe
type is modeled after). In Haskell Maybe is an example of a monad.
(Perhaps not such a good example?) If we could code "monad" explicitly
in Axiom and assuming it could be implemented efficiently, could we
code domains more general than Maybe without any other special
built-in support? Would this allow SPAD to be a more purely functional
language? Would that be a good thing?
Is this a useless exercise? Maybe we should stop?
Gabriel Dos Reis
| 1) Does this code (in principle) capture the notion of Monad?
For me, it is just a set of signatures; I should NOT be the person
being asked to reverse engineer what you wrote! :-)
| 2) If yes, is it useful? How to use it?
I do not know how useful it is until you've shown concrete examples
(Spad) illustrating why you wrote it in the first place and what it is
useful for.
| 3) Why doesn't this compile? (Discussion of function versus functor.)
It compiles in OpenAxiom. I do not see a fundamental reason why it
should not compile in other AXIOM flavours.
| 4) Is there another way to write it that does compile and that would
| be a useful way to represent a monad-like construction in Axiom?
It compiles; I have no idea how you wanted to use it, so I cannot tell
you whether it is useful.
| 5) What would have to change (if anything) in Axiom to allow it or
| something similar to compile?
At the moment, the definition you gave (when properly written in Spad
syntax) compiles. That alone does not say much to me, because I do not
know exactly how you are using it. So far it is just a category!
| 6) Should we be able to pass functors as arguments, store them in
| variables, etc. the way we do with functions (and as implied in the
| original Axiom literature)?
Which functors do you want to pass? Example of code.
| 7) What type (if any) should be associated with a functor?
Every functor in AXIOM has a type. You get it by executing
)boot getConstructorSignature ctor
where <ctor> is the name of the constructor you want, e.g. 'List,
'Integer, etc. You get the target type by
)boot getConstructorSignature(ctor).target
and the list of arguments types with
)boot getConstructorSignature(ctor).source
| Note: Here functor, like function, refers to a constructor that is
| unapplied but applicable.
understood.
| For example in OpenAxiom you have a Maybe domain presumably modeled
| after Haskell (or perhaps modeled after whatever the Haskell Maybe
| type is modeled after). In Haskell Maybe is an example of a monad.
The *concept* of a monadic type to indicate possible failure has always
existed in AXIOM. To express that in Spad, you just form
Union(T,"failed") where T is the actual data type in case of
non-failure. However, that -expression- of the idea of monadic type
has its own set of problems, starting with serious hackery in the Spad
compiler, including inefficiency such as consing every time one
performs an operation on SingleInteger that might fail. Consequently, I
decided to have a better expression of the idea of failure monadic type.
I decided on the name Maybe (from Haskell), as opposed to 'option'
(from ML, which existed before Haskell was invented.)
So, yes I took the *name* from Haskell, but my primary goal was not to
write Haskell in Spad. Rather, I was looking for a name to designate a
type I designed as an efficient expression of an idea that already existed.
To be clear, I am not claiming that the notion of monadic type is
special to Haskell or Spad. It is an idea that exists in any serious
programming language that I have used -- C/C++ (null pointer to
represent absence of information),
Lisp (certain usage of NIL), Java/C# (null references), scripting
languages, etc.
| (Perhaps not such a good example?) If we could code "monad" explicitly
| in Axiom and assuming it could be implemented efficiently, could we
| code domains more general than Maybe without any other special
| built-in support?
As ever, my question has always been: to what end? What *problem* are
you trying to solve? Why is that solution better than the alternatives
(for a definition of "better")? If I do not know what problem you are
trying to solve, how do I know that what is being proposed is in fact a
solution to a known/serious problem in Spad?
| Would this allow SPAD to be a more purely functional
| language? Would that be a good thing?
What problems are you trying to solve? Sorry for asking again. I must
ask because I do not understand the goal.
| Is this a useless exercise? Maybe we should stop?
I do not know. You tell me. And this is not rhetorical.
I am just having hard time understanding the problem you are trying to
solve, and why it is a problem.
-- Gaby
Bill Page
were specified earlier in this thread. See also message in related
thread LazyList by Martin Baker.
On Wed, Nov 9, 2011 at 3:08 PM, Gabriel Dos Reis wrote:
> Bill Page <bill...@newsynthesis.org> writes:
>
> | 2) If yes, is it useful? How to use it?
>
> I do not know how useful it is until you've shown concrete examples
> (Spad) illustrating why you wrote it in the first place and what it is
> useful for.
An example usage was already given earlier in this same thread which
you omitted when you quoted.
> IMList(): Monad(Integer,List) == add
> unit ( x:Integer ): List Integer == list x
> mult ( x: List List Integer ): List Integer = concat x
Note especially the 2nd argument to Monad.
>
> | 3) Why doesn't this compile? (Discussion of function versus functor.)
>
> It compiles in OpenAxiom. I do not see a fundamental reason why it
> should not compile in other AXIOM flavours.
>
I presume you mean:
Monad(A: SetCategory, M: SetCategory -> SetCategory): Category == with
unit: A -> M A
mult: M M A -> M A
Yes that does compile. Is M compiled as a function or as a functor? If
function what does M A mean in the signatures for unit and mult ?
The code that does not compile is when we try to use it. See above or
http://axiom-wiki.newsynthesis.org/SandBoxMonads#msg20111109...@axiom-wiki.newsynthesis.org
> | 4) Is there another way to write it that does compile and that would
> | be a useful way to represent a monad-like construction in Axiom?
>
> It compiles; I have no idea how you wanted to use it, so I cannot tell
> you whether it is useful.
>
> | 5) What would have to change (if anything) in Axiom to allow it or
> | something similar to compile?
>
> At the moment, the definition you gave (when properly written in Spad
> syntax) compiles. That alone does not say much to me, because I do not
> know exactly how you are using it. So far it is just a category!
>
Is it really a category? Can you show example code that uses it successfully?
> | 6) Should we be able to pass functors as arguments, store them in
> | variables, etc. the way we do with functions (and as implied in the
> | original Axiom literature)?
>
> Which functors do you want to pass? Example of code.
>
I am sorry you missed the example I gave earlier in this thread.
> | 7) What type (if any) should be associated with a functor?
>
> Every functor in AXIOM has a type. You get it by executing
>
> )boot getConstructorSignature ctor
>
> where <ctor> is the name of the constructor you want, e.g. 'List,
> 'Integer, etc.
In FriCAS I get with Complex for example:
)boot getConstructorSignature 'Complex
(|getConstructorSignature| '|Complex|)
Value = ((|Join| (|ComplexCategory| |#1|)
(CATEGORY |package|
(IF (|has| |#1| (|OpenMath|))
(ATTRIBUTE (|OpenMath|))
|noBranch|)))
(|CommutativeRing|))
--
How would I write that type in an argument list in SPAD? Really this
issue is: Can I pass a functor as a parameter? If so, how can I write
it's type?
> ...
> ...
Bertfried Fauser
> Every functor in AXIOM has a type. You get it by executing
>
> )boot getConstructorSignature ctor
Yes:(1) -
> )boot getConstructorSignature 'List
(EVAL-WHEN (EVAL LOAD) (PROG () (RETURN (|getConstructorSignature| '|List|))))
Value = ((|Join| (|ListAggregate| |#1|)
(CATEGORY |domain| (SIGNATURE |nil| ($))
(SIGNATURE |null| ((|Boolean|) $)) (SIGNATURE |cons| ($ |#1| $))
(SIGNATURE |append| ($ $ $))
(IF (|has| |#1| (|SetCategory|))
(PROGN
(SIGNATURE |setUnion| ($ $ $))
(SIGNATURE |setIntersection| ($ $ $))
(SIGNATURE |setDifference| ($ $ $)))
|noBranch|)
(IF (|has| |#1| (|OpenMath|)) (ATTRIBUTE (|OpenMath|)) |noBranch|)))
(|Type|))
> where <ctor> is the name of the constructor you want, e.g. 'List,
> 'Integer, etc. You get the target type by
No:
(1) -> )boot getConstructorSignature('List).source
(EVAL-WHEN (EVAL LOAD)
(PROG () (RETURN (|getConstructorSignature| (CDR '|List|)))))
>> System error:
The value |List| is not of type LIST.
(at least in FriCAS)
> )boot getConstructorSignature(ctor).target
No:
(1) -> )boot getConstructorSignature('List).target
(EVAL-WHEN (EVAL LOAD)
(PROG () (RETURN (|getConstructorSignature| (CAR '|List|)))))
>> System error:
The value |List| is not of type LIST.
(I have tried to replace 'List by LIST, 'LIST etc but that fails too)
> | For example in OpenAxiom you have a Maybe domain presumably modeled
> | after Haskell (or perhaps modeled after whatever the Haskell Maybe
> | type is modeled after). In Haskell Maybe is an example of a monad.
Do I understand that you have implemented the Maybe 'monad' in OpenAxiom, and
that:
i) Maybe is implemented in BOOT
ii) constructors like List are also coded in BOOT, and there is no
(know to me, you, any?)
way to do this in SPAD
In this case, one should possibly try to implement Monad in a similar
way in BOOT, not
in SPAD, as such constructions as List, Fraction etc. Unfortunately I
don't know anything
about BOOT (Lisp anyhow)....
Cheers
BF.
--
% PD Dr Bertfried Fauser
% Research Fellow, School of Computer Science, Univ. of Birmingham
% Honorary Associate, University of Tasmania
% Privat Docent: University of Konstanz, Physics Dept
<http://www.uni-konstanz.de>
% contact |-> URL : http://www.cs.bham.ac.uk/~fauserb/
% Phone : +44-121-41-42795
Ralf Hemmecke
> ii) constructors like List are also coded in BOOT, and there is no
> (know to me, you, any?)
> way to do this in SPAD
At least for Aldor that is simple, but I believe for SPAD there is no
difference in this case.
http://svn.origo.ethz.ch/wsvn/algebraist/trunk/aldor/lib/aldor/src/base/sal_partial.as
http://svn.origo.ethz.ch/wsvn/algebraist/trunk/aldor/lib/aldor/src/datastruc/sal_list.as
Partial (which corresponds to Maybe) and List are completely
library-defined in libaldor.
And you probably see that the unit in Partial is a simple coerce
function. In List, it is not available, because it seems to be
uninteresting, to just produce a one-element list. But it can, of
course, easily be implemented via unit(t:T): % == cons(t,empty).
The join or mult operation is not available with a signature
M M A -> M A. The reason is simply that you cannot express this
signature when you are inside List or Partial. The closest one can get
would be
List(%) -> % or Partial(%) -> %.
That, however should work, even if one has to explicitly refer to the
name of the domain that one is going to define. It's just that you
cannot define it with an anonymous "add" structure.
But all that only implements the functionalities of monads. It doesn't
make the concept of a monad available in Aldor/SPAD, such that one could
inherit the signatures from that (coded) concept.
Ralf
Martin Baker
> Bill Page <bill...@newsynthesis.org> writes:
> | 1) Does this code (in principle) capture the notion of Monad?
>
> For me, it is just a set of signatures; I should NOT be the person
> being asked to reverse engineer what you wrote! :-)
>
> | 2) If yes, is it useful? How to use it?
>
> I do not know how useful it is until you've shown concrete examples
> (Spad) illustrating why you wrote it in the first place and what it is
> useful for.
endofunctor equipped with two natural transformations like this:
mult: M M A -> M A
like this:
class Functor m => MyMonad m
where
eta :: a -> m a
mu :: m (m a) -> m a
However it is only in each implementation of this typeclass that the
axioms for a monad are enforced. So, even in Haskell, we don't have
one single construct that encapsulates all the properties of a monad,
I find it hard to imagine how any language could encode the axioms for
a monad in such a way that they are automatically enforced in all its
implementations. Perhaps it could be done by introspection of the code
(I am guessing that is why Bertfried is looking at the Lisp/Boot
code?)
I guess that the same with other SPAD categories: that the axioms are
only enforced in its implementations.
Given the importance of the monad concept in both mathematics and
computer science, it would be good if SPAD had, at least, as much
support for this concept as Haskell has.
Martin
Gabriel Dos Reis
[...]
| > where <ctor> is the name of the constructor you want, e.g. 'List,
| > 'Integer, etc. You get the target type by
| No:
| (1) -> )boot getConstructorSignature('List).source
| (EVAL-WHEN (EVAL LOAD)
| (PROG () (RETURN (|getConstructorSignature| (CDR '|List|)))))
|
| >> System error:
| The value |List| is not of type LIST.
| (at least in FriCAS)
well, that is a "bug" in FriCAS's Boot parser (and I suspect in other AXIOMs)
that parses
f(x).t
as
f(x.t)
OpenAxiom's Boot parser parses f(x).t the same way that the Spad
compiler and the interperter do.
So, a workaround that but would be to write
)boot (getConstructorSignature('List)).source
| > )boot getConstructorSignature(ctor).target
| No:
| (1) -> )boot getConstructorSignature('List).target
| (EVAL-WHEN (EVAL LOAD)
| (PROG () (RETURN (|getConstructorSignature| (CAR '|List|)))))
|
| >> System error:
| The value |List| is not of type LIST.
|
| (I have tried to replace 'List by LIST, 'LIST etc but that fails too)
Same remark here as above.
| > | For example in OpenAxiom you have a Maybe domain presumably modeled
| > | after Haskell (or perhaps modeled after whatever the Haskell Maybe
| > | type is modeled after). In Haskell Maybe is an example of a monad.
|
| Do I understand that you have implemented the Maybe 'monad' in OpenAxiom, and
| that:
| i) Maybe is implemented in BOOT
Maybe is a functor in the OpenAxiom library, implemented in Spad. See
the definition here:
| ii) constructors like List are also coded in BOOT, and there is no
| (know to me, you, any?)
| way to do this in SPAD
I would not say that a constructor like List is coded in Boot.
They are implemented in Spad, with help of some intrinsic functions.
| In this case, one should possibly try to implement Monad in a similar
| way in BOOT, not
| in SPAD, as such constructions as List, Fraction etc. Unfortunately I
| don't know anything
| about BOOT (Lisp anyhow)....
Hmm, I am still unsure the issue has to do with Boot versus Spad.
The real issue has to do with how to interpret type forms at the Spad
level. There is an underlying assumption in the current semantics (and
in all AXIOM compilers) that at Spad level a domain form that is not a
variable is introduced by instantiating a constructor.
You are right that since Boot is very low level, one would not face
that issue. One would face a different one: how to connect that
semantics with the higher level Spad semantics.
I suspect that would have just displaced the issue, without actually
solving it. N
Notice that having a functor Monad is just a tiny fraction of what is
being discussed. Once one has a Monad what does one do with it? As it
was found very quickly, one gets into some peculiar programming style
(which is not at all obviously better than what one currently has in
Spad). To solve that peculiar problem, the "do"-notation was introduced.
-- Gaby
Gabriel Dos Reis
[...]
| Partial (which corresponds to Maybe) and List are completely
| library-defined in libaldor.
The same is true in OpenAxiom -- I would suspect in FriCAS too.
-- Gaby
Waldek Hebisch
>
> Do you think we should be allowed to write something like the
> following in the OpenAxiom compiler (SPAD)?
>
> (X:Domain):Domain+->List X
>
> i.e. define a function that takes a domain as an argument and returns
> a domain? Could we use such a thing in a statically typed language? I
> suppose not.
>
In FriCAS there is no Domain, but code like this should work in
the compiler. In experimantal version of factoring code I have
(or had):
extField : FiniteAlgebraicExtensionField(F) := get_extension(n)
do_factor(p, n, extField)
and in do_factor there was loop coercing coefficients of p to
extField and calling factor(p)$extField (actually, and internal
factoring function).
The point is that get_extension tried to choose most efficient
extension and returend it. The rest of code just uses extField
only caring about its category, and not how it was choosen and
which particular extension it is.
Or look at simplifyCoeffs in pfo.spad.pamphlet. Here nR is
given by literal constructor, but parameter to this constructor
is only known at runtime. Equally well nR could have been
computed via a separate function. There is several places
in algebra where we compute new domains or packages at
runtime and than call functions from them. Due to limitation
of old Axiom compiler new domains are computed by inline
code. But in FriCAS they can by computed by functions.
Note that all that is statically known about such computed
domain is its category. If that category is Type than
there is litte which you can do with such domain. But
once you have more specific category, then such computed
domains have many uses.
Note: that is reason why categories are not first class.
With first class categories code using first class domains
would be impossible to check statically.
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Gabriel Dos Reis
| Sorry. This is not an attempt to solve any specific problem.
Ah! Maybe I should refrain from trying to answer questions then :-/
| The goals
| were specified earlier in this thread. See also message in related
| thread LazyList by Martin Baker.
|
| On Wed, Nov 9, 2011 at 3:08 PM, Gabriel Dos Reis wrote:
| > Bill Page <bill...@newsynthesis.org> writes:
| >
| > | 2) If yes, is it useful? How to use it?
| >
| > I do not know how useful it is until you've shown concrete examples
| > (Spad) illustrating why you wrote it in the first place and what it is
| > useful for.
|
| An example usage was already given earlier in this same thread which
| you omitted when you quoted.
then, do not hesitate to present it again. There are too many things
going on and I am trying to focus on one problem at a time, otherwise it
is total chaos. It is highly nontrivial to triage between what is valid
assumption, what is invalid, what is just bug, and what is plain
misunderstanding.
| > IMList(): Monad(Integer,List) == add
| > unit ( x:Integer ): List Integer == list x
| > mult ( x: List List Integer ): List Integer = concat x
|
| Note especially the 2nd argument to Monad.
In OpenAxiom, the second argument does not match the expected type.
| >
| > | 3) Why doesn't this compile? (Discussion of function versus functor.)
| >
| > It compiles in OpenAxiom. I do not see a fundamental reason why it
| > should not compile in other AXIOM flavours.
| >
|
| I presume you mean:
|
| Monad(A: SetCategory, M: SetCategory -> SetCategory): Category == with
| unit: A -> M A
| mult: M M A -> M A
|
| Yes that does compile.
Great!
| Is M compiled as a function or as a functor?
In OpenAxiom, it is elabporated as a parameter with function type --
which is also what I read from your code. Also, remember that a
category definition is barely type checked. You can smuggle in there
just about anything and we have seen that in the past.
| If function what does M A mean in the signatures for unit and mult ?
In OpenAxiom, M A is an expression designating a domain that satisfies
SetCategory. Did you have a different expectaion?
| The code that does not compile is when we try to use it.
In OpenAxiom, the category definition is just fine. It is just a
category definition; there is no high hope there.
However, the instantiation with arguments Integer and List is not type
correct, because the functor List does not have the type expected by Monad.
| See above or
|
| http://axiom-wiki.newsynthesis.org/SandBoxMonads#msg20111109...@axiom-wiki.newsynthesis.org
|
| > | 4) Is there another way to write it that does compile and that would
| > | be a useful way to represent a monad-like construction in Axiom?
| >
| > It compiles; I have no idea how you wanted to use it, so I cannot tell
| > you whether it is useful.
| >
| > | 5) What would have to change (if anything) in Axiom to allow it or
| > | something similar to compile?
| >
| > At the moment, the definition you gave (when properly written in Spad
| > syntax) compiles. That alone does not say much to me, because I do not
| > know exactly how you are using it. So far it is just a category!
| >
|
| Is it really a category?
Yes, it is. Is there any indication that it should not?
| Can you show example code that uses it successfully?
No, I did not conceive of it in the first place! I honestly to not have
an idea of what problem you are trying to solve.
While looking at this, I realize there is a bug in the OpenAxiom
compiler where a conversion of constructor to a general function type is
not compiled correctly. Fixed. See example here:
The handling in the interpreter is a completely different story.
| > | 6) Should we be able to pass functors as arguments, store them in
| > | variables, etc. the way we do with functions (and as implied in the
| > | original Axiom literature)?
| >
| > Which functors do you want to pass? Example of code.
| >
|
| I am sorry you missed the example I gave earlier in this thread.
Thanks.
| > | 7) What type (if any) should be associated with a functor?
| >
| > Every functor in AXIOM has a type. You get it by executing
| >
| > )boot getConstructorSignature ctor
| >
| > where <ctor> is the name of the constructor you want, e.g. 'List,
| > 'Integer, etc.
|
| In FriCAS I get with Complex for example:
|
| )boot getConstructorSignature 'Complex
|
| (|getConstructorSignature| '|Complex|)
| Value = ((|Join| (|ComplexCategory| |#1|)
| (CATEGORY |package|
| (IF (|has| |#1| (|OpenMath|))
| (ATTRIBUTE (|OpenMath|))
| |noBranch|)))
| (|CommutativeRing|))
|
| --
|
| How would I write that type in an argument list in SPAD?
That expression is not closed -- it mentions the free variable #1.
Assuming it is in scope, it is just
ComplexCategory #1 with
if #1 has OpenMath then OpenMath
CommutativeRing
| Really this issue is: Can I pass a functor as a parameter?
Yes.
| If so, how can I write it's type?
In Spad (library), in a way that respect type expectations.
See the example in the OpenAxiom repo above.
-- Gaby
Bill Page
> Bill Page writes:
>
> | > IMList(): Monad(Integer,List) == add
> | > unit ( x:Integer ): List Integer == list x
> | > mult ( x: List List Integer ): List Integer = concat x
> |
> | Note especially the 2nd argument to Monad.
>
> In OpenAxiom, the second argument does not match the expected type.
>
That is clear. Hence my question concerning the type of 'List'.
> |
> | Monad(A: SetCategory, M: SetCategory -> SetCategory): Category == with
> | unit: A -> M A
> | mult: M M A -> M A
> |
> | Yes that does compile.
>
> Great!
>
> | Is M compiled as a function or as a functor?
>
> In OpenAxiom, it is elaborated as a parameter with function type --
> which is also what I read from your code. Also, remember that a
> category definition is barely type checked. You can smuggle in there
> just about anything and we have seen that in the past.
>
So 'List' is not of type 'SetCategory->SetCategory', but you are going
to tell me that it *is* a function of type 'Type->Type', 'Type' being
the top of the category hierarchy with no exports. All domains satisfy
'Type' by definition. It just so happens that the actual type of
'List' is '(R:Type) -> Join(ListAggregate(R), ... )'.
As written, 'List' is not an endofunctor but it can be considered as
such if we are willing to forget about what it exports.
> | If function what does M A mean in the signatures for unit and mult ?
>
> In OpenAxiom, M A is an expression designating a domain that satisfies
> SetCategory. Did you have a different expectation?
>
This is my confusion.
It did not occur to me that I could simply use a function where a
domain is expected. I find it difficult to keep in mind that the
difference between a function and functor is in only in how they are
evaluated, therefore I (incorrectly) assumed that a function and a
functor necessarily had different types. But what you are telling me
is that any expression that evaluates as a domain is acceptable here.
> | The code that does not compile is when we try to use it.
>
> In OpenAxiom, the category definition is just fine. It is just a
> category definition; there is no high hope there.
> However, the instantiation with arguments Integer and List is not type
> correct, because the functor List does not have the type expected by Monad.
>
Yes. Thank you for the explanation. Therefore if I expected to pass
'List' as an argument of Monad I must have:
Monad(A: Type, M: Type -> Type): Category == with
unit: A -> M A
mult: M M A -> M A
> ...
> While looking at this, I realize there is a bug in the OpenAxiom
> compiler where a conversion of constructor to a general function type is
> not compiled correctly. Fixed. See example here:
>
> http://svn.open-axiom.org/viewvc/open-axiom/1.4.x/src/testsuite/compiler/ctor-mapping.spad?revision=2459&view=markup
>
> The handling in the interpreter is a completely different story.
>
> | > | 7) What type (if any) should be associated with a functor?
> | >
> | > Every functor in AXIOM has a type. You get it by executing
> | >
> | > )boot getConstructorSignature ctor
> | >
> | > where <ctor> is the name of the constructor you want, e.g. 'List,
> | > 'Integer, etc.
> |
> | In FriCAS I get with Complex for example:
> |
> | )boot getConstructorSignature 'Complex
> |
> | (|getConstructorSignature| '|Complex|)
> | Value = ((|Join| (|ComplexCategory| |#1|)
> | (CATEGORY |package|
> | (IF (|has| |#1| (|OpenMath|))
> | (ATTRIBUTE (|OpenMath|))
> | |noBranch|)))
> | (|CommutativeRing|))
> |
> | --
> |
> | How would I write that type in an argument list in SPAD?
>
> That expression is not closed -- it mentions the free variable #1.
> Assuming it is in scope, it is just
>
> ComplexCategory #1 with
> if #1 has OpenMath then OpenMath
> CommutativeRing
>
No, I think that must be wrong. Properly prettyprinting the output
getConstructorSignature gives:
(
(|Join| (|ComplexCategory| |#1|)
(CATEGORY |package|
(IF (|has| |#1| (|OpenMath|))
(ATTRIBUTE (|OpenMath|))
|noBranch|
)
)
)
(|CommutativeRing|)
)
CommutativeRing is the source in the type of Complex. The Target is
ComplexCategory #1 with
if #1 has OpenMath then OpenMath
So it's type must be written something like
(R:CommutativeRing) -> ComplexCategory R with
if R has OpenMath then OpenMath
If I wanted to write a domain that only took functors of this type in
a parameter, could I write the above expression in the parameter list?
> | Really this issue is: Can I pass a functor as a parameter?
>
> Yes.
>
> | If so, how can I write it's type?
>
> In Spad (library), in a way that respect type expectations.
> See the example in the OpenAxiom repo above.
>
Thanks. That was quite helpful. I was able to compile and use the following:
)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)
See: http://axiom-wiki.newsynthesis.org/SandBoxMonads#msg20111109...@axiom-wiki.newsynthesis.org
Regards,
Bill Page.
Gabriel Dos Reis
[...]
| > | Monad(A: SetCategory, M: SetCategory -> SetCategory): Category == with
| > | unit: A -> M A
| > | mult: M M A -> M A
| > |
| > | Yes that does compile.
| >
| > Great!
| >
| > | Is M compiled as a function or as a functor?
| >
| > In OpenAxiom, it is elaborated as a parameter with function type --
| > which is also what I read from your code. Also, remember that a
| > category definition is barely type checked. You can smuggle in there
| > just about anything and we have seen that in the past.
| >
|
| So 'List' is not of type 'SetCategory->SetCategory',
That is correct. A subsidiary question is whether it can be *coerced*
to that type. See below.
| but you are going to tell me that it *is* a function of type 'Type->Type',
More precisely, the constructor List can be coerced to a function of
type Type -> Type. Since the coercion does not incur any runtime
computation, we just "pretend" that that function is also List.
In addition, note that the type Type -> Type, mirrors more closely what
you have in Haskell (which, if I understand correctly, sparked the
debate; correct me if I am wrong). In Haskell you have * -> * where *
is the kind (i.e. type) of all types.
| 'Type' being the top of the category hierarchy with no exports. All
| domains satisfy 'Type' by definition. It just so happens that the
| actual type of 'List' is '(R:Type) -> Join(ListAggregate(R), ... )'.
Yes, that is correct. The type of the contructor List (and in general,
that of any constructor in AXIOM) is slightly more complicated than the
types of most ordinary functions. It is a dependent type, i.e. the
target type can mention (abstract) values of the parameters.
To this date, no AXIOM flavour has a general support for dependent
types. For constructors, howver, dependent types are important.
So a special handling is done for them. Formal parameters are named #i
where <i> is the position of the parameter in the parameter list,
starting from 1. With that, the rest of elaboration (and type checking)
is not as if in a conventional type system without dependent types.
It works well almost all the time -- except when it does not, in which
case you get some "surprises", but it is important to understand the
current model (I am not justifying them, just explaining things.)
| As written, 'List' is not an endofunctor but it can be considered as
| such if we are willing to forget about what it exports.
Well, the contructor List *is* an endofunctor -- you certainly can
iterate it. An endofunctor is not required to be surjective, so it is
OK if its range has more properties than its input, as long as the range
is included in the input -- which is the case here.
| > | If function what does M A mean in the signatures for unit and mult ?
| >
| > In OpenAxiom, M A is an expression designating a domain that satisfies
| > SetCategory. Did you have a different expectation?
| >
|
| This is my confusion.
|
| It did not occur to me that I could simply use a function where a
| domain is expected. I find it difficult to keep in mind that the
| difference between a function and functor is in only in how they are
| evaluated,
That is why they are called "constructors" :-)
Constructors are very special -- the systems know about them in very
intimate ways. Furthermore, formal systems also know about them -- you
must, at least if you want to distinguish values from general expressions.
| therefore I (incorrectly) assumed that a function and a
| functor necessarily had different types. But what you are telling me
| is that any expression that evaluates as a domain is acceptable here.
That is correct. There are situations where the system needs to know
whether something is a constructor or just a general function --
e.g. when to decide equality of types.
| > | The code that does not compile is when we try to use it.
| >
| > In OpenAxiom, the category definition is just fine. It is just a
| > category definition; there is no high hope there.
| > However, the instantiation with arguments Integer and List is not type
| > correct, because the functor List does not have the type expected by Monad.
| >
|
| Yes. Thank you for the explanation. Therefore if I expected to pass
| 'List' as an argument of Monad I must have:
|
| Monad(A: Type, M: Type -> Type): Category == with
| unit: A -> M A
| mult: M M A -> M A
Yes, at least until the systems understand dependent types or at the
very least dependent contravariant type coercions.
You are right. Thank you; I was confused by the formatting.
| If I wanted to write a domain that only took functors of this type in
| a parameter, could I write the above expression in the parameter list?
If the function does not have dependent types (like above), yes --
see examples in the library, e.g. defaults.spad.pamphlet and many other
places. For types that are dependent, you have to wait till someone
implement dependent contravariant type checking :-)
Note that in general AXIOM compilers do not implement contravariant
coercions for all functions -- keeping with the tradition that only
"trivial" coercions are available in libraries. However, for
constructors the situation is special because of the conditionals in
exports.
| > | Really this issue is: Can I pass a functor as a parameter?
| >
| > Yes.
| >
| > | If so, how can I write it's type?
| >
| > In Spad (library), in a way that respect type expectations.
| > See the example in the OpenAxiom repo above.
| >
|
| Thanks. That was quite helpful. I was able to compile and use the following:
|
| )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)
|
| See: http://axiom-wiki.newsynthesis.org/SandBoxMonads#msg20111109...@axiom-wiki.newsynthesis.org
Great!
-- Gaby
Martin Baker
> See:
> http://axiom-wiki.newsynthesis.org/SandBoxMonads#msg20111109124013-0800@ax iom-wiki.newsynthesis.org
Good stuff, well done,
I'm having some difficulty with the following, I would just like to
check out the axioms at the top of the page, which are:
mu o T mu = mu o mu T
mu o T eta = mu o eta T = 1
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:
concat[concat T2a,concat T2b] = concat(concat[T2a,T2b])
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:
(1) -> Outer := join([[[1,2],[3,4]],[[5,6]]])$MonadList(List Integer)
(1) [[1,2],[3,4],[5,6]]
Type: List(List(Integer))
Then we can join the rest:
(2) -> join(Outer)$MonadList(Integer)
(2) [1,2,3,4,5,6]
Type: List(Integer)
I'm not sure how we can concatenate the inner list first?
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
Bertfried Fauser
the monad stuff starts looking very exciting. However, when I try to
do the following
I fail to compile it (in FriCAS).
I prepared the file monad.input as
-------- Begin monad.input ---------
)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
-------- End monad.input -----------
This is just by copy and past from your sandbox
Then I issur the )read command, which produces the following error
code, which I have
not seen before:
(1) -> )read monad.input
)abbrev category MONADC MonadCat
MONADC abbreviates category 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
Internal Error
Unexpected error in call to system function pf2Sex1
What do I miss here, what is pf2Sex1 ( a lisp call?)
Martin Baker
> I fail to compile it (in FriCAS).
and then compiled them with:
)co monad.spad
)co monadl.spad
That seems to work,
Martin
Bertfried Fauser
yes its embarassin, I made a ,mistake just to read it not compile it..
Bill Page
I am glad you are trying to use the axiom-wiki. I will try to help as
much as I can. I will comment on the substantive part of your email
when I have more time. In the mean time you might want to take a look
an example I am still working on here:
http://axiom-wiki.newsynthesis.org/SandBoxMonad
The problem "OSError" that you report below indicates that something
the wiki is trying to do is being rejected by the operating system. I
am not sure of the specific cause but my usual quick cure is to
restart the zope server program that runs the wiki code (which I have
just done). I have a monitor program that is supposed to detect this
situation and do the restart automatically but it does not always
work. If you get this message again just let me know and I will
restart is as soon as possible.
One possible cause might be unexpected input. The integration of
Axiom with the wiki code was never much more than a hack and it is
certainly possible to confuse it. Perhaps it is even your attempt to
modify a page or comment on a page that is triggering the failure. (I
don't mean this as "blame" -- only an explanation.
Perhaps you do not understand that on the axiom-wiki website Axiom,
FriCAS, OpenAxiom, Maxima, Reduce and Sage are *live*. Commands
embedded in the wiki page text inside appropriate markers are executed
by the associated programs and the output is subsituted for the
commands when you click Preview or Save. In addition Save generates
email notices to pages subscribers.
So if you write the following in the wiki page text or in a comment
attached to the page:
\begin{spad}
concat[concat T2a,concat T2b] = concat(concat[T2a,T2b])
\end{spad}
you are actually asking FriCAS (or OpenAxiom or Axiom) to compile file
-- file: xxx.spad
concat[concat T2a,concat T2b] = concat(concat[T2a,T2b])
--
using the commpand
)compile xxx.spad
where 'xxx.spad' is an internally generated file name. The output of
the compiler is inserted after the displayed code.
But of course in this case what you are trying to compile is not valid
SPAD code. This might cause FriCAS to do unpredictable things that
ultimately tie up operating system resources thus necessitating a
restart.
But you input is not the only possible cause. Anyone (in the world)
can be editing these pages and sometimes even someone's poorly
designed or malicious web spider program can trigger this sort of
failures.
If you haven't already done so, you should read about the axiom-wiki at:
http://axiom-wiki.newsynthesis.org/AxiomTutorial
http://axiom-wiki.newsynthesis.org/MathAction
http://axiom-wiki.newsynthesis.org/AxiomWiki
Unfortunately a wiki is only as good as the amount of time people have
to maintain it and over the years I kind of lost most of my original
incentive. Soime people however still do maintain some part of the
information contained in axiom-wiki. As a relatively new user of Axiom
and the axiom-wiki I would not be too surprised if you found this
confusing.
I expect that what you intended to write was something like this:
<pre>
concat[concat T2a,concat T2b] = concat(concat[T2a,T2b])
</pre>
You can use HTML markup like <pre> ... </pre> or something called
"StructuredText":
http://axiom-wiki.newsynthesis.org/StructuredText
So the text contents of a wiki page can be quite a confusing mixture
of computer algebra commands, standard HTML markup, embeded LaTeX code
(rendered as an image) or RestructuredText.
Someday (maybe) this will all be re-designed and made pretty. There is
better wiki software available and better ways to integrate computer
algebra into a web page. But it wont be done by me. These days I want
very much to spend my available time actually using Axiom and not
fiddling with things intended to build a larger more active user
community.
Regards,
Bill Page.
On Mon, Nov 14, 2011 at 9:23 AM, Martin Baker <ax8...@martinb.com> wrote:
> Bill,
>
> I tried to include the following at the end of:
> http://axiom-wiki.newsynthesis.org/SandBoxMonads#msg20111109124013-0800@axiom-
> wiki.newsynthesis.org
>
> But only part of it got posted because I keep getting errors like:
>
> Site Error
>
> An error was encountered while publishing this resource.
>
> OSError
> Sorry, a site error occurred.
>
> Traceback (innermost last):
>
> Module ZPublisher.Publish, line 202, in publish_module_standard
> Module ZPublisher.Publish, line 150, in publish
> Module plone.app.linkintegrity.monkey, line 21, in
> zpublisher_exception_hook_wrapper
> Module Zope2.App.startup, line 221, in zpublisher_exception_hook
> Module ZPublisher.Publish, line 119, in publish
> Module ZPublisher.mapply, line 88, in mapply
> Module ZPublisher.Publish, line 42, in call_object
> Module Products.ZWiki.Editing, line 194, in edit
> Module Products.ZWiki.Editing, line 339, in handleEditText
> Module Products.ZWiki.Editing, line 754, in setText
> Module Products.ZWiki.ZWikiPage, line 257, in preRender
> Module Products.ZWiki.plugins.mathaction.pagetypes, line 205, in preRender
> Module Products.ZWiki.plugins.mathaction.ReplaceInlineLatex, line 76, in
> replaceInlineLatex
> Module Products.ZWiki.plugins.mathaction.ReplaceInlineAxiom, line 147, in
> replaceInlineAxiom
> Module Products.ZWiki.plugins.mathaction.axiomWrapper, line 106, in
> renderAxiom
> Module Products.ZWiki.plugins.mathaction.axiomWrapper, line 132, in
> runAxiom
> Module Products.ZWiki.plugins.mathaction.axiomWrapper, line 117, in
> runCommand
> Module subprocess, line 544, in __init__
> Module subprocess, line 908, in _execute_child
>
> OSError
>
> What I was trying to add to the page was this:
> ----------------------------------------------------------------
>
> 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:
>
> \begin{spad}
> concat[concat T2a,concat T2b] = concat(concat[T2a,T2b])
> \end{spad}
>
> 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:
> \begin{axiom}
> Outer := join([[[1,2],[3,4]],[[5,6]]])$MonadList(List Integer)
> \end{axiom}
> Then we can join the rest:
> \begin{axiom}
> join(Outer)$MonadList(Integer)
> \end{axiom}
>
> I'm not sure how we can concatenate the inner list first?
>
> So I guess that if for 'mu' we work with
> \begin{spad}
> join()$MonadList(Integer)
> \end{spad}
> and for 'T mu' we work with
> \begin{spad}
> join()$MonadList(List Integer)
> \end{spad}
Martin Baker
> Martin,
>
> I am glad you are trying to use the axiom-wiki. I will try to help as
> much as I can. I will comment on the substantive part of your email
> when I have more time. In the mean time you might want to take a look
> an example I am still working on here:
>
> http://axiom-wiki.newsynthesis.org/SandBoxMonad
to have all the relevant information and issues in one place. In a few
months time people may have forgotten the thread on this forum and
unless they happen to use the right search term, they may never find
the topic.
In that spirit I think it would be good if the page had more
information about the relationship between 'functors' and 'type
constructors' and the practical issues involved with this (to capture
the information discussed on this thread before it gets lost in the
mist of time). For instance, List-monad is relatively easy to
implement because the List type already exists, but if someone wanted
to implement a specific monad it would be useful to have information
for defining an appropriate type.
Martin
Bill Page
I had to reboot the virtual machine at U. Washington because something
ate all of the available swap space. Now axiom-wiki seems to be
running properly again.
I also added the text you wanted at the end (with a few minor formatting edits).
Regards,
Bill Page.
On Tue, Nov 15, 2011 at 4:57 AM, Martin Baker <ax8...@martinb.com> wrote:
> On Tuesday 15 Nov 2011 02:22:44 you wrote:
>> So if you write the following in the wiki page text or in a comment
>> attached to the page:
>>
>> \begin{spad}
>> concat[concat T2a,concat T2b] = concat(concat[T2a,T2b])
>> \end{spad}
>
> Its not just this, I am getting the OSError even if I try to add plain text.
>
> I think I intended to write:
>
> \begin{axiom}
> concat[concat T2a,concat T2b] = concat(concat[T2a,T2b])
> \end{axiom}
>
> I assumed that would work because T2a and T2b are defined further up the page?
>
> Martin
>
Bill Page
I would be glad if you could add "more information about the
relationship between 'functors' and 'type constructors'.
In general I find long complicated pages difficult to follow. It
might be better to create more pages on specific related issues and
link from one to another.
The prefix SandBox... in the name is supposed to act like a kind of
"draft". Most subscribers do not follow edits to SandBox... pages so
one can edit and save these pages freely without generating a lot of
email traffic or RSS feed noise. Once a SandBox... page is fairly
stable it can be renamed and it's place in the Topic hierachy can be
changed so navigation is more intuitive.
Now we have both SandBoxMonad and SandBoxMonads and of course this
does not make much sense in the long run. I re-used the page
SandBoxMonad for my play with monads in Aldor since the previous
contents of that page where not of much use. When I get more time to
work on this I will eventually rename it appropriately.
Actually there is quite a lot of stuff in SandBox... pages now that
should be either deleted or tidied up and put somewhere else on the
wiki if it is still of some use. In retrospect I still think the
axiom wiki was a good idea but I did not appreciate how much time
would eventually be required for editing content to keep it useful.
Actually It seems like that with most wiki's I visit. :(
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...@googlegroups.com.
> To unsubscribe from this group, send email to fricas-devel...@googlegroups.com.
> For more options, visit this group at http://groups.google.com/group/fricas-devel?hl=en.
>
>
Martin Baker
> Martin,
>
> relationship between 'functors' and 'type constructors'.
I really don't feel qualified to do this, as I will try to explain by
demonstrating my ignorance:
What I had in mind was an explanation starting with a mathematical
approach. That is in the same way that morphisms compare certain
concrete categories (preserve certain elements of structure) then
functors generalise this to allow us to compare different categories.
When we try to implement this in SPAD then all sorts of issues start
to arise:
1) Are we representing a category-theoretic-category with a SPAD-
category and what are the conditions for doing that?
2) How do we relate the concepts of category, type and domain?
At some stage we appear to move from functors comparing categories to
functors 'generating' one category from another:
3) Is this valid? That is might there be some elements of structure
that are not related by the structure?
4) If we generate an SPAD-category in code then I assume that domain
will also have to be generated in code?
I get the impression that we are not modelling functors in general
here but only specific endofunctors which 'generate' hierarchical
types. So in the case of list-monad we start with built-in List rather
than generating it? So if a SPAD programmer wants to implement their
own monad then I assume they would have to start by defining an
inductively defined type? I think there need to be advise to potential
users on how to go about this.
Once all this is clarified then I think it would be good to preserve
all the Nuggets of information in the conversations between Bill, Gaby
and Waldek on this topic. I certainly would not dare to attempt that.
There is something else I would like to ask here. When Googling this
subject there is masses of stuff around monads and Haskell. I get the
impression that Haskell monads are not derived from functors but
people seem to think they should be (and in some libraries they are).
Haskell also seems to have the concept of 'applicative functors' which
are half way between functors and monads. I have only seen these terms
defined in a Haskell context by giving examples. Has anyone come
across the terms:
1) Applicative functor
2) Generative functor
3) Generative type
in this more general context? Would they be useful here? How would you
define them?
It seems to me that, if this code is ever going to go into the SPAD
library then this type of information need to be available for end
users and maintainers of the code - otherwise its no use to anyone, so
why not do it now while it is clearer in your mind? As I think I have
demonstrated above I am not really qualified to do it. I'm prepared to
do my share but I'm not looking for the role of chief documenter.
Martin
Bill Page
On Tue, Nov 15, 2011 at 11:16 AM, you wrote:
> On Tuesday 15 Nov 2011 13:37:04 Bill Page wrote:
>> Martin,
>>
>> I would be glad if you could add "more information about the
>> relationship between 'functors' and 'type constructors'.
>
> Bill,
>
> I really don't feel qualified to do this, as I will try to explain by
> demonstrating my ignorance:
>
On the contrary, the standard response is that "It is the ignorant who
are most qualified". :)
> What I had in mind was an explanation starting with a mathematical
> approach. That is in the same way that morphisms compare certain
> concrete categories (preserve certain elements of structure) then
> functors generalise this to allow us to compare different categories.
>
Ok.
> When we try to implement this in SPAD then all sorts of issues start
> to arise:
> 1) Are we representing a category-theoretic-category with a SPAD-
> category and what are the conditions for doing that?
I would say Yes, but I am not sure what you have in mind for "conditions".
> 2) How do we relate the concepts of category, type and domain?
>
As recommended by several other people who have studied Axiom and
category theory
http://axiom-wiki.newsynthesis.org/CategoryTheoryAndAxiom
I think we should follow the same approach as:
http://en.wikibooks.org/wiki/Haskell/Category_theory
This means that Axiom categories are sub-categories of the "Axiom
Category". We can give it a name if you like, say: Ax (written
boldface). In Axiom this would be just called 'Type'.
Domains are objects in some (sub)-category.
> At some stage we appear to move from functors comparing categories to
> functors 'generating' one category from another:
> 3) Is this valid? That is might there be some elements of structure
> that are not related by the structure?
Most category theory is constructive.
> 4) If we generate an SPAD-category in code then I assume that domain
> will also have to be generated in code?
>
I don't understand this question.
> I get the impression that we are not modelling functors in general
> here but only specific endofunctors which 'generate' hierarchical
> types.
I don't think so.
> So in the case of list-monad we start with built-in List rather
> than generating it? So if a SPAD programmer wants to implement their
> own monad then I assume they would have to start by defining an
> inductively defined type? I think there need to be advise to potential
> users on how to go about this.
>
That is exactly what we are trying to learn to do here. I don't think
we are there yet. There may still be something hidden or missing in
Axiom that we don't know about.
> Once all this is clarified then I think it would be good to preserve
> all the Nuggets of information in the conversations between Bill, Gaby
> and Waldek on this topic. I certainly would not dare to attempt that.
>
Great.
> There is something else I would like to ask here. When Googling this
> subject there is masses of stuff around monads and Haskell. I get the
> impression that Haskell monads are not derived from functors but
> people seem to think they should be (and in some libraries they are).
Certainly the design of monads in Haskell was at least in part
motivated by category theory. Haskell was designed at a time that the
importance of category theory in computer science was becoming widely
recognized.
> Haskell also seems to have the concept of 'applicative functors' which
> are half way between functors and monads. I have only seen these terms
> defined in a Haskell context by giving examples. Has anyone come
> across the terms:
> 1) Applicative functor
> 2) Generative functor
> 3) Generative type
> in this more general context? Would they be useful here? How would you
> define them?
>
I do not have a complete answer. I think it is reasonable to claim
that all functors in Axiom are "applicative".
One thing to keep in mind is that what is called a "functor" in Axiom
might not be exactly what is called a functor in mathematics. In
particular there is no specific requirement in Axiom that a functor
actually be functorial, i.e. that it export a suitable 'map'
operation.
> It seems to me that, if this code is ever going to go into the SPAD
> library then this type of information need to be available for end
> users and maintainers of the code - otherwise its no use to anyone, so
> why not do it now while it is clearer in your mind? As I think I have
> demonstrated above I am not really qualified to do it. I'm prepared to
> do my share but I'm not looking for the role of chief documenter.
>
It is not clear in my mind. :(
Regards.
Bill Page.
Martin Baker
> > 4) If we generate an SPAD-category in code then I assume that domain
> > will also have to be generated in code?
>
> I don't understand this question.
at is if:
B is some base class
T is an endofunctor
(in category theoretic terms)
Then this 'generates' a sequence of categories:
T B, T^2 B, T^3 B ...
If we now swap to SPAD terminology, when we implement a monad, do we
extend the above category sequence or do we create the implementation
independently like:
List Integer, List List Integer, List List List Integer ...
or using your program:
MonadList(Integer),MonadList(List Integer), MonadList(List List
Integer)...
Actually I think it should really be:
MonadList(Integer),MonadList(MonadList(Integer)),
MonadList(MonadList(MonadList( Integer)))...
So, thinking about it again, its not an issue, because the individual
domains extend the individual categories. So the infinite sequence of
domains extends the infinite sequence of categories.
So I think I've answered my own question?
Martin