Re: [open-axiom-devel] [fricas-devel] Re: [fricas-devel] Re: iterators and cartesian product.

[Bill P. <bil...@ne...>]

On 10/31/07, Ralf Hemmecke wrote:
> ...
> Of course the A must come from somewhere, but who would like to write a
> cross of two functions in that way?
>
> I would better have something like
>
>   cross: (A: Type) -> (A->X,A->Y) -> (A->%)
>
> later say
>
>   product == cross(Integer)
>
> and then use "product" as I did above.
>

Ok, that's fine.

> And since this A is actually part of the Limit definition there should
> rather be something like (dream dream ...)
>
>   Limit(A: Type): ... {-- this introduces A
>      Product(X: Type, Y: Type): with {...} == add {...}
>   }
>
> within "with {..}" and "add {...}" there would be no need to say
> anything about "product", since it would come through the Limit
> construction.
>
> Oh, that is not well thought of... How would the compile know that the
> function is called "product"? Hmmmmm.....
>

The domain constructor 'Limit', as a generalization of 'Product' needs
to be defined over both a set of domains and some arrows (functions)
involving those domains

  Limit(A,B,C, ... A->B, B->C, ... )

then 'limit', as a generalization of 'product' is the following
uniquely defined exported operation

  limit(X:Type,f:X->A,g:X->B, h:X->C, ... ): X -> %

for any X, f, g, h, ... such that everything commutes. But I am not
sure how best to write the signature of 'Limit'. It requires both a
Tuple(Type) and a Tuple of maps involving (possibly just some of)
those Type. A reasonable general syntax probably requires an extension
of the compiler but special cases can be easily defined, e.g.

  Equalizer(A:Type,B:Type,p:A->B,q:A->B)

  equalizer(X:Type,f:X->A):Union(X->%,"failed")

where "failed" is returned in the case p f ~= q f

http://en.wikipedia.org/wiki/Equalizer_%28mathematics%29
http://en.wikipedia.org/wiki/Limit_(category_theory)

> ...
> >>
> >>   product: (X -> A, X -> B) -> X -> %.
> >
> > What is X above?
>
> All-quantified. In fact, I was thinking that the compiler would silently
> introduce this "Limit(X)" from above.

It might be nice to define such generic operations where any domain X
(or other implicit types required for "unification") is deduced from
context. I guess this would be a natural generalization concept of a
"mode" in the Axiom interpreter where a type place marker can be
denoted by '?', but I am not sure if this belongs in the compiler or
not.

>
> >> You don't want to write down that function definition yourself, right?
>
> > Well, I would actually expect it to be exported by a basic built-in
> > domain like 'Record' since that is what most directly corresponds to
> > categorical Product. If this was made sufficiently general, there
> > would be no need for a separately programmed domain in the library.
>
> I think I can support this.
>

Great. :-)

Regards,
Bill Page.