🚀 go-pugleaf

In article <878@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>In article  <28149@dime.cs.umass.edu> victor yodaiken writes:
>]
>]I'm not at all sure that type determination is always something that one
>]can entrust to a compiler. 
>
>I wasn't advocating that.  In most dynamically typed languages the
>compiler has no idea what the type of anything is.  The programmer
>knows the types and, where it isn't obvious, he should document the
>types.  There is no reason (other than efficiency) that he should be
>required to specify the type to the compiler.
>
>The same applies to math.  Mathematical notation should be such that
>the types of variables are clear.  But there is no reason why the
>notation should include formal "declarations" when there are other
>easy ways for a human to tell what the types are.  Mathematics is

Mathematical literature is full of statements of the form
"let X be a finite set", let $f: S x Y -> Z$", "k ranges over
the naturals", etc. etc., these are type declarations.  For example,
here's the Serge Lang in "algebra" (1984, Addison-Wesely)

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

How else are we going to make the types of the variables "clear", except
by type definitions of this kind?
I don't see how one can avoid declarations in either programming or
math, except when the domain is very simple or very stylized.
Here's an example. Suppose we define an encoding of sequences into
integers with a map  element(i,j)$ that picks out the ith element
of the sequence encoded in j. When I write  "if i=j then P" there
is now an ambiguity, do I mean to compare i and j as integers, or as
sequences? Since the same sequence may be encoded by distinct integers
the choice is significant. In a math paper, one might dispell the ambiguity
by using "u" and "v" as sequence variables, while reservng i and j for
integers. So "if u = v then P" could be interpreted without ambiguity
as calling for sequence comparison. But, we can only disambiguate if we
have declared  the types of "u" and"v".


>written for humans to read, not computers.  I claim that programming
>languages should also --as much as possible-- be designed for humans
>to read, not computers.


How can one disagree with this sentiment?