Browse thread
[Caml-list] "high end" type theory for working programmers?
-
Chris Hecker
- Will Benton
- Michael Vanier
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: | 2002-05-03 (04:54) |
From: | Will Benton <willb@c...> |
Subject: | Re: [Caml-list] "high end" type theory for working programmers? |
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