[Prev][Next][Index][Thread]
Static typing disciplines
-
To: Greg Morrisett <jgm@cs.cornell.edu>
-
Subject: Static typing disciplines
-
From: Corky Cartwright <cork@rice.edu>
-
Date: Sat, 1 Jan 2000 19:23:18 -0600 (CST)
-
Cc: types@cis.upenn.edu
-
In-Reply-To: <200001011542.KAA01878@localhost.localdomain>
-
References: <200001011542.KAA01878@localhost.localdomain>
Greg,
>And of course any static typing discipline will be
>incomplete. This does not make them unattractive or
>useless, rather a hard area that must carefully balance
>user-interface, technical, and esthetic issues (what kinds
>of type information will programmers write, what can be
>inferred, what kinds of error messages make sense,
>how is programming methodology influenced, what are
>resaonable notions of "bad", etc.) And
>this is why it's been such an active area of research
>for the past 10-15 years (as opposed to S-expressions.)
I agree. But note that your opening sentence really is
a paraphrase of Matthias's critique of Milner's seminal paper on
ML "type safety". If static typing disciplines are incomplete, then
Well-typed programs CAN go wrong!
Static typing systems only rule out a particular subset of run-time
errors. More sophisticated type systems rule out more errors at the
cost of complicating the definition of what constitutes a legal
program. (BTW, I agree that S-expressions are boring, but isn't it
interesting that the parenthetically-challenged have reinvented
S-expressions under the rubric of XML and think it is big deal?)
>Both you and Matthias seem to want to throw out
>static typing because it will never be complete.
I didn't notice any comment in Matthias's postings to this list that
suggested he thought static typing was useless, but I'll let him speak
for himself.
I have no antipathy toward static typing discplines, only toward false
statements made on their behalf.
-- Corky