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

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

[Chris Hecker]

The list has had a lot of discussions about type theory behind the module 
system, tuples, and the like lately.  Most of it has been over my head, 
which is fun, because it presents a challenge to try to figure out what 
people are saying.  I am wondering how much of it is useful for actually 
writing "regular" code (as opposed to compilers or theorem provers).  Are 
there books (or survey papers) on this stuff that are meant to educate 
working programmers, as opposed to language researchers?  For example, 
where should I go to learn what this means, and whether I care (just a 
randomly chosen sentence representative of stuff that's currently over my 
head from the past few days on the list):

"That functor is essentially the polymorphic identity functor, while the 
other variation was a polymorphic eta-expansion of the abstraction operator."

or another example:

"In this encoding, modules are only records, so module types are ordinary 
types, and there is no distinction between ordinary abstract types 
(introduced by explicit polymorphic abstraction) and ``abstract 
signatures''. There is, as far as I can tell, no need for kind polymorphism."

I started using caml to find out if a "higher level" language could make a 
difference in my programming productivity (writing video games).  As I 
continue with that experiment, I'm curious to know whether understanding 
this high end type theory stuff would help make me a better programmer, or 
just more able to understand the list lately.  Either is fine, but both 
would obviously be great.  :)

Chris

-------------------
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

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

[Michael Vanier]

I highly recommend Benjamin Pierce's new book "Types in Programming
Languages" from MIT press.  It's very well-written, covers much of the
material you describe, and includes implementations in ocaml ;-)

Mike


> Date: Thu, 02 May 2002 17:49:25 -0700
> From: Chris Hecker <checker@d6.com>
> 
> The list has had a lot of discussions about type theory behind the module 
> system, tuples, and the like lately.  Most of it has been over my head, 
> which is fun, because it presents a challenge to try to figure out what 
> people are saying.  I am wondering how much of it is useful for actually 
> writing "regular" code (as opposed to compilers or theorem provers).  Are 
> there books (or survey papers) on this stuff that are meant to educate 
> working programmers, as opposed to language researchers?  For example, 
> where should I go to learn what this means, and whether I care (just a 
> randomly chosen sentence representative of stuff that's currently over my 
> head from the past few days on the list):
> 
> "That functor is essentially the polymorphic identity functor, while the 
> other variation was a polymorphic eta-expansion of the abstraction operator."
> 
> or another example:
> 
> "In this encoding, modules are only records, so module types are ordinary 
> types, and there is no distinction between ordinary abstract types 
> (introduced by explicit polymorphic abstraction) and ``abstract 
> signatures''. There is, as far as I can tell, no need for kind polymorphism."
> 
> I started using caml to find out if a "higher level" language could make a 
> difference in my programming productivity (writing video games).  As I 
> continue with that experiment, I'm curious to know whether understanding 
> this high end type theory stuff would help make me a better programmer, or 
> just more able to understand the list lately.  Either is fine, but both 
> would obviously be great.  :)
> 
> Chris
> 
-------------------
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

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

[Will Benton]

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

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

[Krishnaswami, Neel]

Michael Vanier [mailto:mvanier@cs.caltech.edu] wrote:
> 
> I highly recommend Benjamin Pierce's new book "Types in Programming
> Languages" from MIT press.  It's very well-written, covers much of the
> material you describe, and includes implementations in ocaml ;-)

Let me second this recommendation. It's a great book. I'm a regular
programmer and I found it extremely useful. 

I think that Olivier Danvy's "Functional Unparsing" paper is one
of the best illustrations of why this stuff is useful for regular
programming. There's nothing more practical in the world than 
printing text, and here he uses continuation-passing style, combinators,
higher-order functions, and all that stuff to derive a blisteringly
fast statically-typed printf. It's amazing. (And you can make the
library nearly perfect to use if you use labels and optional arguments.)

This technique is apparently an instance of a more general technique
that Zhe Yang describes in his paper "Encoding Types in ML-like
Languages", at <http://citeseer.nj.nec.com/53925.html>.

--
Neel Krishnaswami
neelk@cswcasa.com
-------------------
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