[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[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 (X11/20070326)

Hi Bill,

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

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

In your "extend" code you use a definiton of "Rep" again.

extend MkAdd(X:ExprCat,Y:ExprCat): with
    +: (X,Y) -> %
  == add
    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.


On 05/12/2007 07:58 AM, Bill Page wrote:

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:

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

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.

Bill Page.

reply via email to

[Prev in Thread] Current Thread [Next in Thread]