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