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 20:14:27 +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.


OK, let me give the following definition.

extend Record(T: Tuple Type): with {
product(A: Type, f: MAP(A -> ?)(T)) -> (A -> %);
product(...): A -> % ==
}

Maybe you can guess what I wanted.

You have
product: (A:Type, A->X,A->Y) -> (A->%)
for the bivariate case.


I wanted to put (A->X, A->Y) into a generic tuple. (Which would be constructed by this MAP constructor (wishful thinking) which maps the function U -> (A->U) over the tuple T.

So if T=(X,Y) then MAP(A -> ?)(T) should be the same as (A->X,A->Y).


Unfortunately, Aldor doesn't allow such a constructor. (Or if somebody happens to know how to define MAP, then let me know.) Hence, I cannot extend Record in the above fashion. That is clearly a limitation of Aldor.


You are speaking here about the limit called Product. Of
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.



That is an interesting thought. I wonder if it could be build into a programming language. Then one would could simply say

Sum == Dual(Product).


I guess it's a bit problematic since the projection functions are called "project" and the injection functions "inject". How would "Dual" know how to rename?


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


Unfortunately, Aldor exports

apply: (%, 'a') -> A

by default. If that were

apply: ('a', %) -> A


instead, one should be able to write x: A := a(p) where p is an element of Record(a: A, b: B, ...);


Ralf