Hello Bill,

On 10/31/2007 05:29 PM, Bill Page wrote:
> On 10/31/07, Ralf Hemmecke <[EMAIL PROTECTED]> 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


-------------------------------------------------------------------------
This SF.net email is sponsored by: Splunk Inc.
Still grepping through log files to find problems?  Stop.
Now Search log events and configuration files using AJAX and a browser.
Download your FREE copy of Splunk now >> http://get.splunk.com/
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel

Reply via email to