Version française
Home     About     Download     Resources     Contact us    
Browse thread
[Caml-list] "high end" type theory for working programmers?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Will Benton <willb@c...>
Subject: Re: [Caml-list] "high end" type theory for working programmers?

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

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:

The last one in particular is a gem.


Will Benton      | "Die richtige Methode der Philosophie wäre eigentlich
die:    |  Nichts zu sagen, als was sich sagen läßt...."
**GnuPG public key:

To unsubscribe, mail Archives:
Bug reports: FAQ:
Beginner's list: