From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id GAA22244; Fri, 3 May 2002 06:54:07 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id GAA22248 for ; Fri, 3 May 2002 06:54:06 +0200 (MET DST) Received: from im2.sec.tds.net ([216.170.230.92]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id g434s5P23293 for ; Fri, 3 May 2002 06:54:05 +0200 (MET DST) Received: from [192.168.1.101] (mdsnwi13-vlan435-63.dsl.tds.net [66.222.29.63]) by im2.sec.tds.net (8.12.3/8.12.3) with ESMTP id g434s4QY007487 for ; Thu, 2 May 2002 23:54:04 -0500 (CDT) Subject: Re: [Caml-list] "high end" type theory for working programmers? From: Will Benton To: "caml-list@inria.fr" In-Reply-To: <4.3.2.7.2.20020502173934.03b73250@mail.d6.com> References: <4.3.2.7.2.20020502173934.03b73250@mail.d6.com> Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Mailer: Ximian Evolution 1.0.4.99 Date: 02 May 2002 23:52:44 -0500 Message-Id: <1020401565.4317.177.camel@ludwig> Mime-Version: 1.0 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk 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=3Den&safe=3Doff&selm=3Dj7vk9d3eh1q.fsf%4= 0new-world.cs.rice.edu&rnum=3D1 The last one in particular is a gem. best, wb --=20 Will Benton | "Die richtige Methode der Philosophie w=E4re eigentlich die:=20 willb@acm.org | Nichts zu sagen, als was sich sagen l=E4=DFt...." **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