Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!usc!samsung!crackers!m2c!umvlsi!dime!yodaiken
From: yodaiken@chelm.cs.umass.edu (victor yodaiken)
Newsgroups: comp.lang.misc
Subject: Re: Dynamic typing (part 3)
Message-ID: <28959@dime.cs.umass.edu>
Date: 8 Apr 91 14:53:48 GMT
References: <1593@optima.cs.arizona.edu>
Sender: news@dime.cs.umass.edu
Reply-To: yodaiken@chelm.cs.umass.edu (victor yodaiken)
Organization: University of Massachusetts, Amherst
Lines: 29

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?