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

[Bill Page]

On 10/31/07, Ralf Hemmecke <address@hidden> wrote:
> > The main issue has to do with programming style. The for-loop is a
> > construction from imperative-style programming. Operations like
> > 'product' above operate directly on functions and return functions.
> > This is most common in a functional-programming style and might be
> > used for example in conjuction with another operation such as 'map' to
> > produce the same results a a for-loop constrcut:
>
> > map(product(Float,wholePart,sin),[1.1,2.2,3.3])
> >
> > versus
> >
> > [makeprod(wholePart x, sin x)$Product(Integer,Float) for x in [1.1,2.2,3.3]]
>
> Bill,
>
> you probably mean something like
>
>   map(product(wholePart, sin), [1.1,2.2,3.3])
>
> right?
>

No. The signature must include a dependent type, like this:

  product: (A:Type, A->X,A->Y) -> (A->%)

> Let's look at the signatures:
>
>   wholePart: Float -> Integer
>   sin: Float -> Float; -- I don't like Float, by the way... ;-)
>   [1.1,2.2,3.3]: List Float
>
> So we must have
>
>   product: (Float -> Integer, Float -> Float) ->
>            (Float -> Product(Integer, Float))
>
> and a corresponding signature for map. You surely believe that I can
> program exactly that in Aldor.
>

To define 'product' in general (i.e. as a categorical limit) for any
domain Product(A,B) and domain C we must have

   product(C,f,g):C->Product(A,B)

defined for any functions

  f:C->A
  g:C->B

I don't think you can do that without passing the independent domain C.

> But I guesss that is not your point. Your point is (please correct) that
> you want a categorical definition of "Product".
>
> Product(A, B) should automatically export
>
>   product: (A, B) -> %

No, this is not well defined.

>
> as well as
>
>   product: (X -> A, X -> B) -> X -> %.

What is X above?

>
> 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.

> In terms of Aldor, we have Product = Cross and that is a built-in type.
> So it should be possible (and perhaps be reasonable to extend Cross
> through the compiler, ie, give it a few more exports than it has now.
>

Yes exactly, although I am not sure why we need both Cross and Record.

> But maybe your proposal goes further and you want to be able to define
> domains/functors through categorical limit constructions. So, in fact,
> you want to enrich Aldor/SPAD by new keywords "Limit" and "CoLimit" and
> make "Cross" a library defined type.
>

Yes, maybe. What might be even nicer is if it were possible to
implement adjoint functors as described by Saul Youssef as an even
more basic concept in Aldor/SPAD. He shows how to define Limits and
CoLimits in this more fundamental way.

> If that is what you think/want, then I can somehow understand you and
> would even support it. But to my taste that was not clear enough yet in
> all the previous discussions.
>
> (I have no problem if you forward this and/or my previous mail to the
> lists.)
>

Ok, thanks.

Regards,
Bill Page.