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

[Ralf Hemmecke]

On 03/14/2006 01:37 AM, Gabriel Dos Reis wrote:
> Ralf Hemmecke <address@hidden> writes:

> | Integer is a name for a structure with carrier set
> | 
> | {0, 1, -1, 2, -2, ...}
> | 
> | and operations {+, *, 0, 1, ...}.
> | 
> | Integer is certainly not the carrier set alone.

Well, actually, it is a convention what Integer should stand for.
For some people it might just be enough to consider Integer as an 
abbreviation for the multiplicative structure ({0,1,-1,...}, (*, 1)}
for other people (ie in other contexts) it might be the ring structure.
And very common in algebra, the carrier set is often denoted by the same 
symbol as the whole algebraic structure. (I guess the latter it too 
ambiguous to be mapped to a programming language?)

> Indeed. It is a type, e.g. set equipped with minimal operations that
> let us implement abstractions on top of it.  Just an abstract data
> type can be implemented in terms of another one, an algebraic
> structure cane be constructed in terms of another one.

> | How would you mathematically express that the integers belong to the
> | category of monoids? You would probably say that
> | 
> | F(Integer) is an object in the category of monoids
>
> I would do it by assertion.

What does that mean?

> But I will refrain from needlessly emphasizing on the the carrier set
> -- as F(Integer).

Oh, I hope you understood that F was meant to be a (forgetful) functor 
in the categorial sense whose result would be an object in the category 
of monoids.

So, if you like you could say

define MyMonoid: Category == with {*:(%,%)->%;1:%}
  -- axioms still missing :-(
MonoidStructure(T: Type)(binop:(T,T)->T, unit:T): Monoid == T add {
  Rep == T; import from T;
  (x: %) * (y: %): % == per(binop(rep x, rep y);
  1: % == per unit;
}

That IS Aldor syntax and it would compile. So in Aldor term F from above 
would be something like

F = G(binop, unit)

for that to work it should be possible to write G as

MonoidStructure(binop:(T,T)->T, unit:T): (T: Type) -> Monoid ...

where the operations would have to be specified before the type is 
given. I don't think that is possible in a programming language.

HOWEVER, the above code would ALWAYS return something of type Monoid, 
since it is a type constructor in Aldor and not a forgetful functor in 
the mathematical sense. For me the question would be, how could one 
write forgetful functors in Aldor?

Oh, it just came to my mind, we can have forgetful functors.

Let's take Integer. According to what it has been extended it has a 
definite type (some Aldor category). Basically, if one says

MyInteger: with {+: (%, %)->%; 0: %;} == Integer add;

then MyInteger is like Integer (same carrier set) but everything 
forgotten except + and 0.

Well, then now it remains the question how one could match the names
+, 0 with *,1 in Monoid when asking "MyInteger has Monoid".

But there are 2 problems here.

1) How to match + and the binary operation from Monoid?

2) My specification above probably forgets to much. After all it also 
forgets the properties of + and 0. So it could never be a monoid. 
Unfortunately, Axiom/Aldor does not allow axioms (and I would like to 
see arbitrary predicate logic formulas not just declarative syntax).

Ralf