Re: [Axiom-developer] Re: [Axiom-math] Are Fraction and Complex domains.

[Gabriel Dos Reis]

"Page, Bill" <address@hidden> writes:

| On Thursday, May 11, 2006 7:14 PM Gabriel Dos Reis wrote:
| > 
| > Ralf Hemmecke writes:
| > 
| > [...]
| > 
| > | But of course, I could live with that identification if it 
| > | is clearly documented that ()->Cat can be identified with Cat.
| > | Where are our category experts? I believe there is a distinction
| > | here, n'est pas?
| > 
| > From Category Theory point of view, a constant x of type T 
| > is the same as the (unique) morphism x : 1 -> T, where 1 is
| > the one-point set.
| 
| The relevant object here is the initial object 0 in a complete
| Cartesian closed category (CCCC), not the terminal object 1.

Oh well, I should have written 

   x : tartempion -> T.

Now, buy a time machine, go and tell Mac Lane that wikipedia will use
0 for initial objects, so he should not write his units, one-point set
as 1.  :-) :-)

But, yes, you're right that mathematical notation is highly ambiguous,
let alone categorial notation.

[...]

| The definition of initial is that: there exists precisely one
| morphism () → X for each object X. So in a sense any "categorical"
| distinction between the morphism and co-domain object is not
| likely to be of much interest.

Indeed.

[...]

| > Now, I also understand that beyond the name, Aldor's categories
| > are not mathematical categories; so...
| 
| I think that is an over statement. There is a considerable
| similarity between categories in Aldor and mathematical
| categories. 

Quantify "considerable".

| But that is irrelevant. Any "sufficiently complex"
| programming language must have the structure of a complete
| Cartesian closed category.

That, I believe, is a statement I would like to see more evidence for.

| > My practice of functional programming suggests that the
| > identification is useful in many cases, than keeping the
| > artifice.  But YMMV.
| > 
| 
| I think this identification can be justified from a mathematical
| point of view.

Not only from mathematical point of view; from practical point of view
too.  That is the most important aspect for me.  The fact that no one
has given proof that Aldor's type system is sound (it most probably
isn't) does not prevent you from using it to write useful programs.
Sorry if I sound blunt, but I tend to put practice before theory --
yes, and I do value useful theories :-) 

-- Gaby