Re: [Caml-list] "high end" type theory for working programmers?

[Will Benton <willb@cs.wisc.edu>]

Chris--

Some great references (that explain these issues fairly clearly) are:

    http://citeseer.nj.nec.com/cardelli97type.html
    http://citeseer.nj.nec.com/cardelli88basic.html
    http://citeseer.nj.nec.com/pierce95foundational.html

The first one (a massive survey that came from a CRC handbook) covers
what is meant by "well-typed" and contains the rules for proving that a
language/construct is well-typed.  The second covers type inference in
the face of polymorphism and other "fun" language features.  The third
covers lambda-calculus, the formal model for all functional (and
otherwise) languages (it also covers pi-calculus, which is a model for
communicating processes).  As a general rule, if you see the greek
letters alpha, beta, or eta in a PL-theory context, you can assume that
it's because someone is talking about the lambda calculus.  :-)

In any case, I think if you read those, you'll be able to follow some of
the more "esoteric" discussions.

If you are really interested in learning about this stuff (types,
l-calculus, and PL theory in general), a great book is _Essentials of
Programming Languages_ by Friedman, Wand, and Haynes.  I have the first
edition, which is supposedly better for self-study (it was my undergrad
PL textbook), but the second edition is supposedly a better textbook
from what I've heard.  I have not seen the 2e, but I know that it has
some newer/improved algorithms for some program transformations.

This stuff *will* make you a better programmer -- you have probably
already observed that the strong typing in OCaml makes it easier to
write working code, and learning about how and why it works is helpful
for a lot of peoples' thought/design processes.  However, other PL
theory topics (ones that might seem esoteric, or only useful for
interpreter/compiler writers) will even make you write better code, as
the following anecdotes indicate:

http://groups.google.com/groups?hl=en&safe=off&selm=j7vk9d3eh1q.fsf%40new-world.cs.rice.edu&rnum=1

The last one in particular is a gem.





best,
wb

-- 
Will Benton      | "Die richtige Methode der Philosophie wäre eigentlich
die: 
willb@acm.org    |  Nichts zu sagen, als was sich sagen läßt...."
**GnuPG public key:  http://www.cs.wisc.edu/~willb/pubkey

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners