|
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
[Prev in Thread] | Current Thread | [Next in Thread] |