🚀 go-pugleaf

In article <922@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
> [A quote from Lang]
>]	The collection of all morphisms in a category A will 
>]	bedenoted by AR(A) ("arrows of A"). We shall sometimes use the
>]	symbols "f \in A(A)" to mean that f is a morphism of A ...
>
>That isn't a declaration, it's a comment.  In other words, no formal
>notation is being used to describe the type, an English description is
>being given.  If you want something like a declaration in math, try
>
>  f : A -> B

This I don't understand at all.  Here are two "comments:


comment A: "In the following we use the symbols a,b to denote 
elements of a sequence and u and v to denote sequences"


comment B: "In the following we use the symbols u,v to denote 
elements of a sequence and a and b to denote sequences"


If I write "Comment A" and f(null)= 0, f(av) = h(g(a), f(v))
     I've defined f as a recursive map on sequences
But if I write "Comment B" and  f(null)= 0, f(av) = h(g(a), f(v))
I've defined a quite different function. 
If I precede either with the comment "We use juxtaposition to
indicate iterated multiplication, so that x<y1,.... yn> = 
<xy1,... , xyn>" I could change the meaning of either statment
again by refuting our expectation that av indicates concatenation.

So all these "comments" are really "type declarations" not just comments that
can be stripped from the text without altering the semantics.


Note that I have not had to state what elements can be placed
in a sequence, so both A and B declare only a structural property
If you mean to argue that type declarations in mathematical notation
are generally more concise and more to the point than those offered
by Fortran or C, I'll agree. But it seems as if you are arguing a
larger point.