Type advocacy
Ken Shan
I am preparing a three-minute talk to tell incoming graduate students
at my school about types. Mine is a computer science department where
people come to do all sorts of research -- network protocols, natural
language processing, cryptography, etc. This is not a joke.
My goal is not to get people to become type system researchers or
switch to a new programming language overnight. My goal is to
introduce them to tools and ways of thinking they may not be
previously aware of that may help them understand problems better and
produce better code -- some of which may even be applicable to C.
The following is my current outline/slide-draft. I am seeking advice
on all aspects of this presentation; I may even be convinced that it
is impossible to achieve my goal in three minutes.
Before implementing a solution, first understand what the problem
is and what constitutes a solution.
If your program crashes, it is not a solution.
If your program produces the number "foo", it is not a solution.
If your program takes 200 years to run, it is not a solution.
==> These fundamental necessities are called _safety properties_.
Types are proofs of safety that machines can manipulate.
- Machines can easily check and infer types.
- Humans can easily read and write types.
- Types help both humans and machines understand code.
Types can eliminate memory leaks and segmentation faults.
Types can preserve the integrity of data representations.
Types can annotate programs with their resource requirements.
==> Mistakes that can be automatically located, should be.
I want to add a final section of "pointers" -- things that the
intrigued should look into: programming languages, techniques, even
papers. What pointers should I give?
- Programming languages: Cyclone, ML, Haskell?
- Programming techniques: _Effective C++_, _Writing Solid Code_,
what else?
- Papers: I can't find Daniel Wang's "Why I Like Types" paper
anymore -- where is it? Anything else?
Thanks in advance.
--
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
Siegfried Gonzi
> If your program crashes, it is not a solution.
> If your program produces the number "foo", it is not a solution.
> If your program takes 200 years to run, it is not a solution.
> ==> These fundamental necessities are called _safety properties_.
I think you should re-design the third point. It is not really clear
what speed and types have both in common. Yes I know e.g. when one gives
Clean the strictness (type) information, then this helps the compiler to
infer more quicklier the right types.
But the Scheme compiler "Stalin" (no, there is not a counter Scheme
compiler called Hitler) is a counter-example. Stalin infers the types
without declarations (but I am not really sure here) and shows a decent
and effective code generations.
> - Programming languages: Cyclone, ML, Haskell?
Not to forget Clean here. Especially when you discuss speed and native
code generation.
S. Gonzi
Garry Hodgson
> I want to add a final section of "pointers" -- things that the
> intrigued should look into: programming languages, techniques, even
> papers. What pointers should I give?
>
> - Programming languages: Cyclone, ML, Haskell?
> - Programming techniques: _Effective C++_, _Writing Solid Code_,
> what else?
two great books that may or not be appropriate to your audience:
"Pragmatic Programmer" is full of useful advice for the journeyman
programmer.
"The Unix Programming Environment" for teaching how to use tools to
build tools.
--
Garry Hodgson One way or another
Senior Hacker One way or another
Software Innovation Services One way or another
AT&T Labs This darkness got to give...
ga...@sage.att.com
Matthias Blume
>
> Ken Shan wrote:
>
>
> > If your program crashes, it is not a solution.
> > If your program produces the number "foo", it is not a solution.
> > If your program takes 200 years to run, it is not a solution.
> > ==> These fundamental necessities are called _safety properties_.
>
> I think you should re-design the third point. It is not really clear
> what speed and types have both in common. Yes I know e.g. when one gives
> Clean the strictness (type) information, then this helps the compiler to
> infer more quicklier the right types.
There might be type systems that track time resources, but I am currently
not aware of any. (It would not be a surprise, though. There _are_ type
systems -- witness "region inference" -- that deal with other resoures like
memory.)
> But the Scheme compiler "Stalin" (no, there is not a counter Scheme
> compiler called Hitler) is a counter-example. Stalin infers the types
> without declarations (but I am not really sure here) and shows a decent
> and effective code generations.
How is this a "counterexample"? Looks more like a perfectly valid example
in favor of types. ML compilers also infer types at compile time and do not
require the programmer to specify them. Stalin is (slightly) different in
that it does this for a language where types do not play such a central role
in its formal definition. But it shows that in real-world programs types
are always there and don't "get in your way".
Matthias
Siegfried Gonzi
> How is this a "counterexample"?
I meant counterexample to "not to have to declare types explicitely, for
gaining maximum speed" as compared to Clean.
S. Gonzi
Daniel C. Wang
Rough draft of something I should finish one day...
(Why I like types...)
http://www.cs.princeton.edu/~danwang/wilt.ps
The big point I was trying to make was that types let you encode static
program invariants.
Invariants are very useful. They act as documentation, hints to the
compiler/optimizer, and a notation with which to think about programming
problems.
I also try to draw the line between typed/and untyped languages in a careful
way that avoids confusion.
Luca Cardelli's chapter on the "Type Systems" in the CRC Handbook of Computer
Science is also a good read. (There's a draft copy on his web page if you
don't have the CRC book on hand...)
Peter G. Hancock
Siegfried> Ken Shan wrote:
>> If your program crashes, it is not a solution. If your program
>> produces the number "foo", it is not a solution. If your
>> program takes 200 years to run, it is not a solution. ==>
>> These fundamental necessities are called _safety properties_.
Siegfried> I think you should re-design the third point. It is not
Siegfried> really clear what speed and types have both in
Siegfried> common.
But (hard) realtime constraints _are_ safety properties.
One of Ken's points seems to be that types are safety properties
you can check and infer. As "sound-bites" go, this seems pretty fair.
There is by the way theoretical work on typesystems for polynomial
time. See for example the fourth paper on the following page, and
the references in it.
http://www.mathematik.uni-muenchen.de/~schwicht/
--
Peter Hancock
Jonathan G Campbell
Maybe the connection between memory leaks, seg. faults, and types is a
bit remote?
Could you introduce specification, e.g. of a procedure -- design by
contract would be an accessible metaphor; then types as the first line
of defense in checking validity of parameter values; see Bertrand
Meyer's Object-oriented Software Construction.
A good analogy for types in parameter lists would be electrical plugs
and sockets -- you don't want to pass 110 volts AC when the device is
expecting 6v DC. Also, the different shaped connectors on computers and
electronic instrumentation.
If you had the time, you could mention the fact that, deep down in the
computer's memory, all data, are mere bundles of numbers -- how to
indicate which is a big number, which small, which a text character,
etc.
Tony Hoare stated somewhere that he judged his advocacy of type checking
to be his chief contribution to computer science; I've searched high and
low, including Google and a reasonable collection of his works, but
cannot find the source.
Best regards,
Jon C.
--
Jonathan G Campbell BT48 7PG jg.ca...@ntlworld.com 028 7126 6125
http://homepage.ntlworld.com/jg.campbell/
Joachim Durchholz
> Maybe the connection between memory leaks, seg. faults, and types
> is a bit remote?
>
> Could you introduce specification, e.g. of a procedure -- design
> by contract would be an accessible metaphor; then types as the
> first line of defense in checking validity of parameter values;
> see Bertrand Meyer's Object-oriented Software Construction.
Note that BM's writings don't mention that parameter types are a form of
contract. He doesn't discuss this connection, probably because it's
incompatible with covariance (which he fiercely defends in the book even
though it makes the type system unsound - not that his reasoning on the
relevance of covariance were invalid, it's a real dilemma).
Regards,
Joachim
--
This is not an official statement from my employer.
Ashley Yakeley
<k...@digitas.harvard.edu> wrote:
> I am preparing a three-minute talk to tell incoming graduate students
> at my school about types.
Oh like that's going to work. You'd be better off selling T-shirts that
say "WHAT PART OF" (and then the Hindley-Milner prinicipal-type
algorithm) "DON'T YOU UNDERSTAND?".
If anyone gives you any lip, ask them how to find the square-root of a
string. Everything else follows on from that.
> What pointers should I give?
Safe ones.
--
Ashley Yakeley, Seattle WA