Path: utzoo!news-server.csri.toronto.edu!cs.utexas.edu!sdd.hp.com!decwrl!pa.dec.com!rust.zso.dec.com!shlump.nac.dec.com!engage!marx.enet.dec.com!grier
From: grier@marx.enet.dec.com
Newsgroups: comp.lang.misc
Subject: RE: Dynamic typing (part 3)
Message-ID: <1991Mar15.062756.3781@engage.enet.dec.com>
Date: 15 Mar 91 06:27:56 GMT
References: <602@optima.cs.arizona.edu> <YR+9VUB@xds13.ferranti.com> <1991Mar13.010946.4536@engage.enet.dec.com> <13MAR91.00251986@uc780.umd.edu> <1991Mar13.163629.12630@engage.enet.dec.com> <14MAR91.22372006@uc780.umd.edu>
Sender: news@engage.enet.dec.com (USENET News System)
Reply-To: grier@marx.enet.dec.com ()
Organization: Digital Equipment Corporation
Lines: 299

In article <14MAR91.22372006@uc780.umd.edu>, cs450a03@uc780.umd.edu writes:
|> 
|> Hmm... so what is the correct way of finding if x is a member of set
|> y?  What is the domain of a function which selects the first 5 from
|> an ordered sequence?  What is the domain of = (test-if-equal)?  What
|> is the domain of encapsulation (obtain-a-pointer-to)?  What is the 
|> domain of search (look-up-in-table)?

   I don't see what point you're trying to make.  If these aren't
take a look at most any object-oriented system designed in the last
decade or so with strong typing and parametrized types.  Or even outside
the OO world per se., in perhaps CLU.

   (In direct answer, picking a syntax, perhaps "contains(y, x)",
"select_first_n(seq, 5)", "Object", huh?  let's keep pointers out of this..,
assuming that the Table type is parametrized ala "Table[KeyType,
ValueType]", it's the type specified for KeyType when the particular
Table value instance was created.)

|> 
|> Why should I limit assignment (name-association) based on the domain
|> of, for instance, addition?

   I don't know, why should you?  I think you're trying to twist what I'm
saying somehow but I don't see your point.  Perhaps it's your terminology.
I'll spell it out.

   If in some scope you have a variable, let's call it X, which is
declared to be of type "Number" (presuming all the types with
algebraic-type operations fall under there for the sake of argument,)
the compiler should ensure that any value I attempt to bind
X to is compatible with the type of X.  (I.e. you can assign 5, pi,
e, 27, 42, 0.00000001, maybe even 2+3i to X.  But you couldn't
assign "my car", "the red firetruck" or "The Soviet Union" to X.
Insert appropriate type-checking rules for generics/parametrized
types.)

|> 
|> > ...
|> >  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.
|> 
|> And which of those types is the domain of log() ?  Can you think of a
|> good reason to not have runtime type-checking for log?
|> 

   I can think of a better reason not to have runtime type checking for
log: if I'm doing it quite a bit, the runtime costs are high.  Wasn't that
part of the whole original premise or why David Gudeman made his
original postings?

   I believe that Ada's model here is correct.  No correct program may
depend on exceptions for its operation.  (Implying that if you have
a correct program, you can turn off all the nice bounds-testing and
such and end up with a nice and *fast* program.  Commercial Ada
compilers from both Rational and Digital do this.)

|> >|> 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.
|> 
|> No this makes you feel safer?  Or no it doesn't make you feel safer?

   Beings I discusses my thoughts on both counts, does it matter other
than you wanting to pick nits?

|> 
|> >   "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.
|> 
|> Sounds like a good reason to avoid testing to me.  (Right folks?)
|> 

   Testing what?

   What does that have to do with placing operations artificially high in
an inheritance/subtyping tree?  This is a design issue more than a
testing one.

   I am most certainly not arguing against testing.  However, if you
haven't had an error reported, it doesn't mean it doesn't exist - it
just means that either the tester hasn't found it or didn't feel like
reporting it that day.

|> 
|> I have no objection to compilers doing their best.  Nor do I claim
|> that testing somehow negates the responsibility of the designer to
|> ensure correctness.  Nor do I claim that the compiler relieves the
|> designer of the responsibility for correctness. 
|> 

   Ok, we're in total agreement here.  I feel that there is/should be
an important synergy between programmer and compiler here.
(Good) compilers can find a great deal more optimizations than
people can on silly things like removing loop invariants, etc.  People
can do much more important optimizations on newer and better
spiffy algorithms.  However, people shouldn't be wasting their
time second-guessing the compiler.  But I digress as usual...

|> On the other hand, I do claim that IF the language lets me, I can
|> write programs which can be verified quite simply.  The technique is
|> very similar to induction.  (Check boundary conditions, check for
|> typical case).  Sometimes you can make your testing into a proof of
|> correctness (given basic assumptions about the correctness of the
|> underlying machinery).  Sometimes not.  
|> 

   Right, for a single program in a single instance.  If you've been
following what I've been saying, my argument has been around the
long term maintenance of large systems.  I could add, subtract and
multiple and even take derivatives and come up with anti-derivatives
long before I understood any of the theory.  Loose induction and
random sampling don't make for proofs.

   Simple programs can be verified simply.  Complex ones are harder.

   This is one of several places where "programs as proofs" falls apart.
My central argument is in long term management of large software
projects.

|> As an aside, you can test both your understanding of a concept, and
|> its correctness by implementing it and seeing if it works.  Proofs can
|> have bugs in them too, you know.
|> 

   No arguments here! Again your comments make me believe that
you don't understand my stance.  Please re-read my postings if
you have them available.

|> >   (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.)
|> 
|> And how is a compiler supposed to prove that a program fulfills its
|> purpose?  At best, the compiler can prove that the program can be
|> compiled. 
|> 

   Re-read my previous posting today.  (well, yesterday at this
point.)

|> >...
|> >   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 do not believe I was arguing for any of these features.

   (again) Read my posting earlier today.

   I claim that once a type hierarchy grows beyond the immediate and
total understanding of one person at a time, and into a depth of complexity
where the application of the algorithms for operation selection tend
towards guessing/smartness.  (I don't believe in AI per se, but I can
imagine that applying even simple pattern matching rules against a large
enough rule base could possibly maybe someday potentially doubtfully
pass a turing test.  This is exactly the situation when you have a large
projects.  Whether you're dealing with a decent modular language like
Ada or Modula-2, or into the OO world with an Eiffel, Trellis or Modula-3,
you need automated ensurance of type safety.)

   You're sitting on the bridge of the enterprise.  "Sulu, press the red
button".
(Unbeknownst to you, Captain Kirk, a new Red self-destruct button was
installed right next to the Warp Factor 1.0 button which used to be
called red
but might now be considered a dingy maroon.  ka-bam-ooo...  it's a
shame,
there was once a time when you knew that ship from stem to stern.  If
only
Star Fleet had had the sense to make a regulation that only one Red
button
would be on the navigator's console, but nobody thought that such
regulations and checks were necessary...)

   Once again, this is a problem I see in large systems evolving over time.
My motivation isn't so much to prove correctness as to ensure that changes
and growth don't invalidate other algorithms' implementations.  My
extending "Read()" to return baby names in addition to numbers broke
David Gudeman's program which assumes they're numbers, unfortunately.

   I want the system to be able to recognize these problems and prevent
them from being made into a running system.  We all understand that
even in a strongly typed language where type information isn't made
explicitly available, the most specific actual type of an expression
can't always be inferred.  Which means that either (a) we don't do static
checking because we don't want those blasted type error or syntax
error messages anyways, or (b) there are cases where it is impossible
for the compiler to statically type-check the program.

   In the (a) case, well, damn the torpedoes, full speed ahead, and I'll
just make sure I don't fly your airline or do banking with your bank.

   In the (b) case now either you've lost type-safety (which I claim is
good and worthy of our respect,) or you have to start inserting clues
about types of expressions back into your program.  Oh, but wait,
that's sooo difficult, we can't do that.  We'll just let it run... (tick,
tick, tick...)

|> 
|> >   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 ...
|> 
|> A very good reason for runtime type checking.
|> 

   Or proving your algorithms and implementations before putting
them in life-critical situations.

|> >   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.
|> 
|> I must admit that following your line of thought (or attempting to--
|> I'm not sure I succeeded) is tiring for me as well.  I should point
|> out that I am not in the research world, and work very hard to see
|> that what people pay for works well.  And while I disclaim knowledge
|> of what you think dynamic typing is, I do claim that type as a
|> property of DATA as opposed to a property of a NAME does increase
|> productivity, quality, correctness as well as robustness.
|> 
|> In fact, I claim that assigning types to names, independent of the
|> assigned values, is a akin to side-effect driven programming.  I
|> realize that it is necessary at a low level.  I don't see it as a
|> productivity boost.  

   I claim it doesn't.  I also write software for a living that people
depend on running their business.  I've worked with languages
where the programmer has the option of being able
to specify that only certain values are permitted in a given context,
and ones where looser bindings are permitted.  There is no doubt in
my mind that in the environments where the ability to specify the
types of values which can be associated with a given name in a given
scope, the quality of software was higher and the debugging cycle
was shorter than in an environment which had a looser typing scheme
and where I spent a few too many late nights tracking down where
what was eventually an obvious typing error occurred.  The problems
occurred exactly because of the problems I've been outlining, and
they would not/could not have occurred in a language where names
are only permitted to be bound to certain types of values.  The
error would have been reported during compilation with a
hopefully expressive message which would have explained the
difficulty.)

   If you can remember all those details so that when modules
evolve you can feel quite certain that interfaces won't be broken,
I congratulate you.  It's just too bad that you're using an environment
where your skill and expertise are wasted debugging rather than
designing and implementing.

   (I really don't understand the motivation.  Is there some amazing
wonderful power that you get out of dynamic typing?  Other than
being able to ask for bigger hardware and personnel budgets when
you need bigger computers and more people to maintain your
software?  I don't see the costs of static typing being high, and the
benefits are numerous.  I'm trying to see where this claimed
productivity and quality gain came from.  Please enlighten me!)

   Sorry for rambling, it's past my bedtime.

|> 
|> 
|> 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