🚀 go-pugleaf

In article <815@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>In article  <L-2A3G2@xds13.ferranti.com> Peter da Silva writes:
>
>]But if you don't know that y is complex, you don't know if "y <= 0" is
>]legal or not...
>
>If you don't know the length of A, you don't know whether "A[i]" is
>legal or not.  So?  You should know the length of A and you should
>know the type of y.  In someone elses code, if you see "y <= 0",
>then you can assume that y is not complex.  In you own code, if you
>know that y is not complex you can write "y <= 0".  There is no
>ambiguity.
>
>]with this in mathematics is everyone has had a bunch of Fortran-style'
>]default typing rules programmed into their head in college.
>
>No, the reason you can get away with this in math is that everyone who
>has a clue knows that you can't compare magnitudes of complex numbers,
>so if you are comparing magnitudes, the numbers must not be compex.
>This is a trivial logical inference:
>

I believe that clarifying notation and type theory has been the subject
of an enormous body of mathematical research over the last century. 
The "type" of an object is often quite unobvious. For example, 
when we write ax = bx -> a=b we are assuming that the "type" of
a,b, and x and the type of the operation has the cancellation property.
If we are working within semigroup theory, this assertion is false. 
Similarly, it is well known that  if x = y - z + z' we can get an
equivalent assertion by rewriting to x = y + -1(z - z')  but if we apply
this rule to the equation x = 1 -1 +1 -1 +1 ... (infinite), we can
prove that 1=0 --- the type of the infinite sequence 1-1 +1 ....
is not "number", so the rules we have invoked cannot be applied. 

I'm not at all sure that type determination is always something that one
can entrust to a compiler.