Re: [Axiom-developer] Curiosities with Axiom mathematical structures

[Gabriel Dos Reis]

"Bill Page" <address@hidden> writes:

| On February 27, 2006 11:08 AM Gabriel Dos Reis wrote:
| 
| >...
| >  
| > Ralf Hemmecke <address@hidden> writes:
| > ... 
| > | One reason for having Monoid and AbelianMoniod (one with "*" and
| > | the other with "+") is that neither SPAD nor Aldor allows to
| > | rename functions during inheritance.
| > 
| > yes, that is true for many (all?) object-oriented languages.  I can
| > understand the language limitation, but that is hardly an excuse for
| > chosing in advance that "+" is for Abelian monoid and "*" for
| > non-Abelian ones.
| >
| 
| I don't see why renaming is necessary.

Me neither, but I guess it is a solution.  But a solution that I
think brings greater confusion.

| > | Note that one would have to say something like
| > | 
| > | define Monoid(
| > |    *: (%, %) -> %;
| > |    1: %
| > | ): Category == ...
| > | 
| > | define Group(
| > |    *: (%, %) -> %,
| > |    inv: % -> %,
| > |    1: %
| > | ): Category == ...
| > | 
| > | define Ring(.....): Category == with {
| > |    Monoid(*, 1);
| > |    Group(+, -, 0);
| > | }
| > 
| > Ring should be both Monoid and Group, whether they shoud be 
| > categories, I don't really know.
| >
| 
| In Axiom (SPAD) we can write:
| 
| Monoid(m:Symbol,u:Symbol): Category == with
|        m: (%,%) -> %       ++ returns the product of x and y
|        u: () -> %          ++ unit

The reason I previously said I did not see why Monoid should be a
category is that the operation is already passed in as a parameter, so
there would nothing to implement "inside" in the Monoid.
However, upon discussion with a colleague, it appears that having to
pass in all the required properties (e.g. operation, neutral element,
etc.) will not be practical from software engineering point of view.
Indeed, there would be a redundancy in the system.  The underlying type
and the operation suffice to uniquely define the structure.  So that
means, the other parameters are somehow "function" of the essential
parameters. That implies that indeed Monoid will be a category which
domains will implement by supplying the value for the neutral element.
Same reasoning for Group where the type and the operation suffice to
define the inverse and the neutral element.

[...]

| > I believe this is something solvable -- at least, that can be
| > approximated to a good extent -- in a type system based on
| > predicate system directly available at the programming level.
| > We've been developing such an idea to build a type system for
| > C++ template arguments, see
| > 
| >    http://public.research.att.com/~bs/popl06.pdf
| > 
| > presented at POPL this year.
| 
| I think the predicates here are what Axiom calls "axioms" such as:
| 
|        associative(m)      ++ m(a,m(b,c)) = m(m(a,b),c)
|        identity(u)         ++ m(a,u) = m(u,a) = a
|        inverse(m,inv)      ++ m(inv(a),a) = m(a,inv(a)) = u
|        commutative(m)      ++ m(a,b) = m(b,a)
|        distributes(m,s)    ++ m(a,s(b,c)) = s(m(a,b),m(a,c))
|                            ++ m(s(a,b),c) = s(m(a,c),m(b,c))

The predicate as I use it was in the general sense; for example, in
the system Monoid is be predicate.  That is consistent with the theory
of "qualified types", of which type classes (Haskell) are examplar.
But, I suspect that use of predicate also integrates yours.

| In Axiom right now the only thing we can do with axioms is to
| test them, e.g.
| 
|   R:=Ring(+,-,"0"::Symbol,*,"1"::Symbol)
|   ...
|   if R has commutative(+) then
| 
| but one could easily imagine adding more complex predicates
| which could still be evaluated at compile time. (Remember that
| Axiom and Aldor are intended to be statically typed languages.)

yes, I know Aldor is a statically typed language; in the predicate
system I'm talking about Rin would be a predicate -- it says that a
combination of certain symbols are stated to conform to "Ring"
property.  Again, this is "obvious" from the qualified theory point of
view. 

| > Notice that the "post facto extenstion" of Aldor is a starting
| > point, but it still does not help solving that issue..
| 
| As I understand it, post facto extension allows for the
| iterative definition of a type, i.e. adding and/or refining
| new functions.

Yes!

| I am not sure how this might apply in the
| example of the Ring above, but I think there are more
| interesting types that must be defined by mutual recursion
| and in that case post facto extension seems very natural.
| Could you give some examples of how else you think this can
| be used?

Suppose I started with a monoid M = Monoid(T, foo), then later prove
or discover that it really is Abelian.  When ipso fact extension, I
could say

      M has commutative(operation.M)

the point here is that I do not need to have all properties that M
might have handy before defining it.  I can add those properties on the
go.

| > The make the approach practical for large libraries in
| > Axiom/Aldor I believe some form of deduction of category/domain
| > argument deduction would needed.  However, Axiom/Aldor types
| > being dependent, that be challenging.   Anyway, I have searched
| > the literature for the descirption of Axiom/Adlor type system
| > as implemented, I have found nothing that could assist me.
| > 
| 
| Have you looked at the papers by Erik Poll and Simon Thompson
| such as:

I had read two of the papers you pointed out (that was in 2004).  But
none of them helped me find clarify the problem I was after.  
I'll read the third one.

Thanks!

-- Gaby