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

[Ralf Hemmecke]

Hi Bill,

I somehow don't know where to start with my comments. But let me first 
say something about

http://wiki.axiom-developer.org/SandBoxLimitsAndColimits

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.

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 contruct an element of a product.

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)?

   For Record(a:A,b:B,...) the projection functions are basically
   apply: (%, 'a') -> A
   apply: (%, 'b') -> B
   ...
   and thus all have different names.

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.

Let me also add a warning to the code on

http://wiki.axiom-developer.org/SandBoxAldorInductiveTypes

In your "extend" code you use a definiton 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.

Ralf


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.
>
> Regards,
> Bill Page.