Path: utzoo!news-server.csri.toronto.edu!cs.utexas.edu!sdd.hp.com!caen!news.cs.indiana.edu!arizona.edu!arizona!gudeman
From: gudeman@cs.arizona.edu (David Gudeman)
Newsgroups: comp.lang.misc
Subject: RE: Dynamic typing (part 3)
Message-ID: <651@optima.cs.arizona.edu>
Date: 15 Mar 91 08:21:58 GMT
Sender: news@cs.arizona.edu
Lines: 104

In article  <1991Mar14.183323.27020@engage.enet.dec.com> grier@marx.enet.dec.com writes:
]In article <626@optima.cs.arizona.edu>, gudeman@cs.arizona.edu (David
]Gudeman) writes:
]
]   ...If you consider a proof to have some static notion of
]correctness (which is exactly what they are,) this kind of error is
]absolutely wong in a formal exhibition of the proof.

It depends on your mathematical tradition.  There are lots of people
who don't worry about that stuff (although the current vogue may tend
toward the picky side).

]|> In the first place, the read() only produced ints and floats, and the
]|> return value was used in a context where either was a legal value.  In
]|> the second place, if the read() function were defined to return other
]|> sorts of values and you wrote "x + read()" the problem would be in the
]|> program, not in the definition of "read()".
]
]   Where is this knowledge known?  Your arguments so far have been to
]not explicitly state the type of value accepted by or returned by an
]operator.  And it still doesn't help when "Read()" is extended in the
]future to return strings, cats and dogs.

No, I often explicitely state the types used by operators, I just
don't tell the computer.  The documentation for a function should give
any relevant type restrictions.  Whenever you change the way a fuction
behaves, you (in general) have to check all the places it is used to
make sure the change is OK.  All static type checking provides is a
compile-time warning if (1) you have missed any uses _and_ and (2) the
function change was of the rare sort that changes the types.  It
doesn't seem very significant for that.

]|> Then you are going to need types "positive int" and "positive float"...
]
]   That's silly.  I'm arguing this in the light of subtyping, so you could
]have some sort of abstract subtype called "Algebraic" or "Number" where
]it has the "usual" operations defined.

The point is the essential arbitrariness of type declarations.  There
is no good verification-based reason to distinguish between ints and
floats and not distinguish between natural and integer, or between
non-zero and with-zero.

]   ReadNumber() would return a "Number" to permit at least type-safety.
]This is a case where the compiler would not have a choice but defer the
]binding of the operation invocation to actual code/methods until run-time,
]but it's still working in a statically typed type-safe environment.

No, the environment is type-safe, but it isn't statically typed.
There are now expressions whose types can't be uniquely determined at
compile time.  Dynamically typed languages are type safe, they just
have less of the type checking done at compile time.

]   She doesn't.  That's why I argue for subtyping/inheritance/genericity/etc.
]
]   The language is the framework and syntax to work in.  It should be
]minimal and formal.

Thank you for brightening my evening.  I got a good chuckle out of
that.  Asking for subtyping, inheritence, genericity and etc. in a
"minimal" language.  What a card.

]   Actually, formal proof is the only known way to ensure any measure of
]static correctness.

Please stop.  You're killing me.  Where did you get this bizarre sense
of humor?

]   Once you've built up a large type library, the chances that any one
]person has a detailed gestalt of the whole thing is very unlikely.  Therefore,
]unless you explicitly restrict the type of a value you receive, you can only
]assume that it's any type.

(Whew.  Back to serious stuff.)  You generally don't build up large
type libraries like that with dynamically typed languages.  There are
a few generic aggregate types that serve for most data structuring
purposes.  You don't have to implement stacks, hash tables,
concatenatable arrays or other things.

]   Again, one more time, with feeling, my concern is with large software
]systems.

Again, I don't believe that required static typing is in any sense, in
any software system, more reliable than dynamic typing.

]... I'm responding largely to the claims that
]some testing by (a) people who know the system or (b) people who are
]likely to only push the buttons that the (a) folks told them to are going to
]ensure anything.

Absolute correctness no.  But the level of security you get from
testing is so far above any you might get from static typing, that the
static typing is insignificant.

]   Yup, and it's going to cost when we have to maintain those
]systems for the next 5-20 years.

On the contrary, that's where the advantages of dynamically typed
languages really shine.  The programs are much more maintainable and
"evolvable".
--
					David Gudeman
gudeman@cs.arizona.edu
noao!arizona!gudeman