axiom-math
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Axiom-math] Re: [open-axiom-devel] [fricas-devel] Re: [fricas-devel] Re


From: Ralf Hemmecke
Subject: [Axiom-math] Re: [open-axiom-devel] [fricas-devel] Re: [fricas-devel] Re: iterators and cartesian product.
Date: Wed, 31 Oct 2007 18:06:20 +0100
User-agent: Thunderbird 2.0.0.6 (X11/20070728)

Hello Bill,

On 10/31/2007 05:29 PM, Bill Page wrote:
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->%)

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.

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

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.

No, of course not. But I would have hidden it in Product(C)(A,B). But also that looks ugly.

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?

All-quantified. In fact, I was thinking that the compiler would silently introduce this "Limit(X)" from 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.

I think I can support this.

Ralf





reply via email to

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