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

[Ralf Hemmecke]

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 -> %);
} == add {
        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
> 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.

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
> semantics of Aldor and Spad.

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