🚀 go-pugleaf

In article <1593@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>Furthermore, when you do use something like a type declaration in
>mathematics, it is to disambiguate or add clarify, and the nature of
>the declarations reflects that.  In statically typed programming
>languages the purpose of the types is to let the compiler generate
>better code, and the nature of the declarations reflects that.  For
>example, you cannot simply declare something as a "number", you have
>to decide whether you want it represented in floating point format or
>integer, and what size you want.  You can't declare that something is
>a set, you have to implement a set using fixed-size memory blocks.
>

Agreeing that the type declarations in classical algol/fortran/c ...
programming languages are hopelessly rigid, I'm not sure that
"dynamic" versus "static" is at the core of the argument. There seems
no reason why we cant have a "static" programming language in which
type declarations are more flexible than current definitions. Thus,
if I declare "x,y" to range over numbers, then "x+y, x*y " are
well defined, but "x/y" is not, because the semantics of /
depends on more than the numberness of the arguments -- i.e.
integer/integer -> integer, float/float -> float, integer/integer ->(q,r)
are all different functions. I sympathize with those who find
it absurd to have to describe variables by storage cell length (
essentially the "c" model) but I still don't see what this has to do
with dynamic "run-time" type checking. Even with function variables,
it seems plausible that one could be forced to provide a proof
that any expression x(y,z) should be type consistent:
(y,z) in Domain(x). Why should this proof be given in temrs of a dyanmic
test, rather than a "compile time" calculation?