axiom-developer
[Top][All Lists]

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

 From: Ralf Hemmecke Subject: [Axiom-developer] Re: a little category theory and inductive types Date: Sat, 12 May 2007 10:57:12 +0200 User-agent: Thunderbird 2.0.0.0 (X11/20070326)

Hi Bill,



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.

+: (X,Y) -> %
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.