🚀 go-pugleaf

In article <13MAR91.00251986@uc780.umd.edu>, cs450a03@uc780.umd.edu writes:

|> My own, biased, observation is that keeping information and control
|> May I humbly suggest, if you really think this (static typing) is a
|> useful approach, that you spend a little time reviewing completeness
|> and consistency?  (Ask your favorite mathematician)  Who knows, maybe
|> you'll be able to solve the knapsack problem.

   Well, my favorite mathematician is about a hundred miles away right now,
but I studied under him for a few years, so I might speak up here.

   In mathematics, symbols bear more relation to unbound variables in
lambda calculus (well, they bear a LOT of relation :-) 

   In mathematics, it makes NO sense to talk about applying a function
or operation to a symbol unless the symbol is known to be in the
domain of the operation/function.  I.e. writing something like "for all
x, exp(x) is greater than zero" is nonsense.  exp's domain is commonly
the reals, and may be extended to bigger domains like the complexes, but
that doesn't mean it applies to the empty set, or the tree outside my
house's door.  The correct way to write that would be, "for all x, if
x is a real number, exp(x) is greater than zero."

   That's a type-case.  I fully expect to make complete knowledge of the
type of a symbol when I apply an operation to it, and any proof where
applying an operation which might not be valid to a value is incorrect.
(And programs are proofs of algorithms.)

   Now, that's the hard stance.  Following this philosophy, if x is in the
set of integers, x is also NOT in the set of reals (a nice copy of it and the
rest of the integers are embedded there.)  So, it's not uncommon to
sleaze through your typing when there is a clear an unambiguous
conversion implied.

|> 
|> 
|> Finally, to Mr. Grier, who posed the rhetorical problem about trusting
|> software in critical systems which might have latent bugs:  would you
|> really trust such software if it had never been tested?  Would it make
|> you feel safer if each type of data required seperate chunks of code,
|> with the associated tests and branches and variant storage mechanisms?

   Yes and no.  No first.

   "No", because that's why I think that subtyping and inheritance is
so wonderful.  If there's an obvious way to specialize an operation to a
subtype, it *is* clearer and still absolutely statically correct to apply the
supertype's operation to a value of the subtype.

   "Yes", because otherwise you end up putting operations up artifically
high in the tree.  The one which comes to mind and really burns me is 
when there's a "Shape" type, and because people want to have values of
type "Shape" and want to apply the "diameter()" operation to them.  Shapes
don't all have diameters!  At least if they do, it's not with the implicit
meaning implied by the C++ folks who want to define a diameter()
virtual member function for Shape.

   When the operations which can be performed by subtypes of a given
variable's type differ from the operations valid for the type, that's
where "Yes" comes into play.  In David Gudeman's example, I most
certainly don't want some "read()" operation which can return ANY
type of value to allow my code to blindly attempt to apply the "+" or
"Log()" operator to it.  My code should have some reason to believe
that "Log()" makes sense when applied to the value.  Statically checked,
before allowing me or anyone else to run it.

   My motivation is that I believe that compilers should try to do their
best to ensure correctness of a program implementation before allowing 
it to be executed.  If you don't believe in that, well, we differ and
that's life. I just wouldn't do my banking or trust my life to software which
relies on extensive testing rather than some level of ensurred correctness.

   (I don't claim that compilers will ever be able to prove correctness
of the semantics of an algorithm, but I'd like them to at least ensure the
correctness of the proof/implementation.)

   In addition, it's a little late now, but in my original posting, I conceded
that this sort of feature would be appropriate for research and/or
prototyping.

   Type checking is something like a spelling checker.  If you're in a burst
of creativity, it's a pain in the ass, so you turn it off - the flow of
information and ideas is much more important than the static
correctness of the spellings.  However, for producing real reports or
papers or books, you want to ensure not only that the ideas are
generally correct, but that the "i"s are dotted and the "t"s are crossed.
That's what strong static typing is.

   Heck, there's an even more direct parallel.  Syntax checking!  Next thing,
why don't we have languages where they "try" to interpret commands and
do what their best guess to the requested operations are!

   I don't WANT a smart computer, I don't WANT a computer which can
misinterpret ambiguous commands, I don't WANT a computer which
can forget.  (machine checks/hardware failures don't count.)

   I want a computer which does EXACTLY what I tell it, really fast.  If what
I tell it to do doesn't or might not make sense, I want it to let me know
so I can clear up any ambiguity as early as possible, rather than letting it
find it out later (rush hour at a busy airport, suddenly over 256 planes are
in the airspace, and some program writes past the end of an array, blasting
away the stack, crashing the ATC computer,) or make some guess (it's fiction,
but my fav. example is from a book by <forget first name> Hogan, _The Two
Faces of Tomorrow_, where a semi-intelligent computer misinterprets an
ambiguously worded command and ends up demolishing things...)

   (I also want to be able to build up a large library of things that I've
already told the computer how to do and now either want to refine or
use again.  I also want it to tell me if I'm using something
incorrectly, and/or
if I  change an existing component if it breaks other existing
components
which I may or may not know about.)

   This is tiring.  If you don't agree with me, that's OK, but I hope you
stay in the research world rather than producing software which people
pay for and expect to work reliably.  But if you're going to claim that
this approach of dynamic typing increases {productivity, quality, 
performance, correctness, robustness}, I'll continue to differ with you.

|> 
|> Raul Rockwell
|> 
------------------------------------------------------------------------
I'm saying this, not Digital.  Don't hold them responsibile for it!

Michael J. Grier                           Digital Equipment Corporation
(508) 496-8417                             grier@leno.dec.com
Littleton, Mass, USA                       Mailstop OGO1-1/R6