[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 20:14:27 +0200
User-agent: Thunderbird (X11/20070326)

Hi Bill,

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
      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, ...);


reply via email to

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