[Axiom-developer] RE: a little category theory and inductive types

[Bill Page]

Ralf,

On May 12, 2007 4:57 AM you wrote:
> 
> I somehow don't know where to start with my comments. But let
> me first say something about
> 
> http://wiki.axiom-developer.org/SandBoxLimitsAndColimits
> 

Thank you for taking the time to reply.

> What you have actually done is a restricted implementation
> of Record with the addition of the (unique) arrow from
> (A, f:A->X, g:A->Y)  into the product X \times Y.

A categorical "arrow" is just a function. Formally I want to
view Aldor and Spad as working in the category Set or at the
very least the associate Cartesian Closed Category.

You are speaking here about the limit called Product. Of
course similar (dual) comments also follow concerning the
co-limit Sum. Duality is one of the fundamental properties
of this categorical approach - you always get two
constructions for the price of one. In any given situation
you are often in a position of wondering about the meaning
and use of the dual construction.

Concerning Product. Yes, you are right. Product is just an
implementation of Record, or actually I would wish to reverse
that: Record should be an implementation of Product. In fact
from the point of view of category theory (or perhaps I should
say "categorical semantics") it is the existence of this unique
definition for the function 'product(A, f:A->X, g:A->Y)' that
defines what we mean by the domain Product and it's projections.

Really these are just different names for the same things,
respectively. The only real problem is that Record and Union
do not provide the naturally associated universal function.

> 
> I like that implementation of this arrow, but I am not so
> sure about where I would use it. (But that is another
> question.) Ah... now I see it. It's a way to construct an
> element of a product.

Think of the function return by 'product(A,f,g)' as a way to
evaluate both f and g in *parallel* over A. Similarly, the
dual construct 'sum(A,f,g)' is a way to evaluate both f and
g in *series* into A.

> 
> You probably see yourself, that your Product implementation 
> has a number of limitations in contrast to Record.
> 
> 1) Suppose you have A=X=Y=Integer and
>     f(a: A): X == a,
>     g(a: A): X == a+1,
>     Then construct for P ==> Product(Integer, Integer)
>       h: A -> P := product(Integer, f, g)
>     What result do you expect for project(h 0)?
>

Yes that is easily remedied by defining the projections as
'project1', 'project2', ... similarly 'inject1', 'inject2'.
I should have done it this way.
 
>     For Record(a:A,b:B,...) the projection functions are
>     basically
>       apply: (%, 'a') -> A
>       apply: (%, 'b') -> B
>     ...
>     and thus all have different names.
> 

This use of enumerators seem awkward to me when what I really
want is a cross product and disjoint union. I don't really
want to have to specify these sort of "tags". But if the
definition of Record(a:A,b:B, ... ) actually defined a, b,
... as the projections:

  a: Record(a:A,b:B, ...) -> A
  b: Record(a:A,b:B, ...) -> A

then I would have much less complaint. Similarly

  a: A -> Union(a:A,b:B ...)
  b: A -> Union(a:A,b:B ...)

would be the injections (union function) into the Union.
But this would be a substantial change to the syntax and
semantics of Aldor and Spad.

> 2) You have to implement a domain "Product" for each
>    arity. Record allows arbitrary arities.
> 
> In fact, (2) for me is a limitation of the Aldor language.
> One could, perhaps define
> 
> Product(T: Tuple Type): with {...} == add {...}
> 
> but I have no good way to express the projection functions. 
> If someone knows, please tell me.

Yes, I also tried this. Perhaps it can be defined in a
recursive manner, but I got stuck in the details and ran
out of mental energy before seeing the best way to do it.

At least in Aldor it is possible to overload domain
constructors. Spad on the other hand complains if I give
two definitions for 'Product', so I am forced to define
'Product2', 'Product3', etc.

But this would not be a problem for the Spad and Aldor
compilers since they already do this for Record and Union.
Like I said, all that is missing is the associated universal
functions.

> 
> Let me also add a warning to the code on
> 
> http://wiki.axiom-developer.org/SandBoxAldorInductiveTypes
> 
> In your "extend" code you use a definition of "Rep" again.
> 
> extend MkAdd(X:ExprCat,Y:ExprCat): with
>      +: (X,Y) -> %
>    == add
>      Rep==Record(left:X,right:Y)
>      import from Rep
>      ((x:X) + (y:Y)):% == per [x,y]
> 
> That is dangerous! An initial domain definition might live
> in quite another (let's say third party) library. How would
> you "extend" if you don't have the sources of the original
> definition. But even with the sources it is a bad idea to
> mention "Rep" in an "extend". If this is necessary, then
> the original (unextended) definition does not have enough
> functionality.
>

You are absolutely right. My example of the use of extend
is deficient. I like correct this as soon as I get another
hour to spare.

Regards,
Bill Page.
 
> 
> On 05/12/2007 07:58 AM, Bill Page wrote:
> > Ralf,
> > 
> > I have updated my example of one way to write an inductive
> > type (as per our recent discussion with Gaby) so that I hope
> > the structure of the definition is more clear. See:
> > 
> > http://wiki.axiom-developer.org/SandBoxAldorInductiveTypes
> > 
> > In particular I found it convenient to first implement an
> > extension of Aldor's Union type to make it more "categorical",
> > i.e. as a true co-product in the sense of category theory.
> > See
> > 
> > http://wiki.axiom-developer.org/SandBoxLimitsAndColimits
> > 
> > This exercise makes me think that there may be a potential
> > for developing a new library in Aldor and domains in Spad
> > that would provide these and similar categorical constructs.
> > 
> > I would be most interested in your comments on this approach.
> >