[Axiom-developer] [Tuples Products And Records] I think we agree

[Bill Page]

Changes 
http://page.axiom-developer.org/zope/mathaction/TuplesProductsAndRecords/diff
--
William Sit wrote:

> Bill Page wrote:
>
> > there is no reason why (A,B) where A and B are domains should not denote 
> > this product.
>
> Exactly, so why are you still insisting on calling it Product(A,B)? 

I am sorry. I must have mislead you somehow into thinking that I was
concerned with the name or the specific Axiom domain called Product.
I am not.

All I want is something that is semantically just the Cartesian product
or better: the product in some category such as CCC. I want the expression
'(A,B)' in the mapping 'f:(A,B)->C' to *be* such a product, complete with
it's projections. I don't want 'Mapping(C,A,B)'. I want it to be
'Mapping(C,(A,B))' where '(A,B)' denotes this product. If you prefer the
notation 'Mapping(C,A x B)' then that is fine with me also. This is not
an issue of "syntactic sugar". That's why I say that the notation
'Mapping(C,Record(a:A,b:B))' is also acceptible - it just provides
specific names for the projections.

> (A,B) need be only the vanilla Cartesian product.

I agree. That is exactly what I am trying to say.

> Would you say that
>
>   f:DirectProduct(5, INT)->INT
>
> has arity 5 then? 

No. The only thing to the left of the $\rightarrow$ that has arity more than
1 is whatever we decide represents the "the vanilla Cartesian product".
Arity is just the size of that product. Of course we have to admit
n-ary products where n is some non-negative integer. $()$ denotes
the "terminal" object (the identity for the product constructor)
and $(A)$ denotes just the object $A$.

I am not sure what you mean by not implementing:

> external interfaces for the projection maps in a Cartesian product

To me, a product is *defined* by it's projections. You can hide
other details of the implementation of a product if you wish,
but not the projections. If you did, then it is mathematically
speaking no longer a product. I think we agree that the "vanilla
Cartesian product" (A,B) necessarily has projections, right?
That is all I want. I am not arguing against encapsulation or
information hiding in the case of the representations of other
constructed domains. So I think that we agree! :)

> But the arity of $h$ is one, not two, despite your use of $h[1,2]$,
> which is really parsed as $h([1,2])$ in Axiom.

**If** we agreed to call 'Record(a:A,b:B)' Axiom's equivalent of
the type of categorical product that I am looking for, *then* I
would say that the arity of $h$ is equal to the size of the Record
object. It is the number of prjection maps. I agree that $h[1,2]$
is parsed like $h([1,2])$. In fact, the best I can determine in
this context '[1,2]' it is really:
\begin{axiom}
construct(1,2)$Record(a:INT,b:INT)
)show Record(a:INT,b:INT)
\end{axiom}

but 'construct' seems to be treated in a rather special way by the
interpreter since when I try to add a 'construct' function to the
'Product' domain, Axiom aborts.

Otherwise "arity" as you have been describing it, is a peculiar
thing in Axiom. It is the number of inputs to the Mapping
constructor minus 1. In my case I want the function Mapping
constructor to be the exponential object in a CCC and of course
that has exactly two inputs.
--
forwarded from http://page.axiom-developer.org/zope/mathaction/address@hidden