The talk is to be on April 13.

I've decided the talk is to be about types in programming languages. This log is intended to serve (for our grad students, primarily) as an example of how I develop a professional level talk on some topic.

Previous to 9 Feb

I have borrowed four or five books from the library to read in preparation for this talk, as well as perhaps a dozen papers. I've scanned the books and papers and am thinking about how to structure the talk, and about what kind of depth is appropriate. This is a huge topic, so I can't go into much depth in any one area, especially since these are topics that are not really covered in any undergraduate course here.

9 Feb

I've decided to structure the talk in parallel to the "Divine Comedy" of Dante - no particular reason except that I think it will provide some nice images and a kind of cool visual map. I'll start with the Inferno and put early languages (Fortran, Cobol...) in Limbo, then just peer over the edge into the abyss occupied by C and assembler (forth?). Then ascend to the Purgatorio of most languages, talk about both dynamic and static typing and why each is good and bad. I'll mention holes in type systems, generics and how they help (and hurt), and oddnesses in OO languages (specifically Java and C++) as well as a bit of co/in/contravariance. Then climb further to the Paradiso and Haskell (Scala?) and then peer into the heavens containing serious formal/mathematical efforts to define types, including the lambda calculus and a mention of Category Theory. A few specific topics (this is mostly a reminder to myself in lieu of doing this on paper) :

• singleton classes, in particular things like implementing Zero as a special object of type "Integer"
• How constructors interfere with this - consider the Integer.valueOf(126) vs new Integer(126) and the caching implemented by autoboxing
• Generics: is ArrayList<Integer> a subclass of ArrayList<Object>? The other way around? In java, instanceof doesn't work on generics.
• in Java null is not an instance of anything and yet null is a legal value in any class.
  
• Generics as functors and variance aspects
• A quick intro to the lambda calculus - specifically relating to type questions - but reductions and reduction order is probably too much.
• Type inference in Haskell
• Category Theory, obviously can't do much with it, but can at least write down some commutative diagrams and show how it relates to ML style functors.
• Partially Ordered Sets and types

11 Feb

Don't forget smalltalk. Both for Boolean/True/False and for multiple dispatch. Also, non class based languages (Self, IO etc)   Also, where does Ruby fit in - mixins are interesting (derived from CLOS).  Ah, and multiple vs single inheritance. 

18 Feb

I keep reading that C++ templates are Turing Complete, so no only is type equivalence in such a framework going to be undecidable, a template construction may not even terminate.   But what about restricting templates - you lose all of the compile time specialization, but may gain in clarity for type construction.    Also, I'm increasingly dubious that either categories or the lambda calculus is going to be managable in any reasonable time frame, so perhaps toss in just a reference to that.   Categories are equally hard to get a handle on, but a couple of commutative diagrams to illustrate things like  a -> f(a) and [a] -> [f(a)] as a map/categorical construction might be useful and convenient.   Also a cutesy (perhaps too much so) idea popped up.   If a type system is large enough to give you some good things (kittens) it is probably also large enough to give you bad things (tigers).   Could be a cute slide.

12 March

So many papers and so much information.   A nice notion that keeps popping up is that a programming language is a proof language (and that thence a program is a proof).   The talk may be cut down to 30 minutes, in which case I may revisit the idea of doing the lambda calculus and category theory - not in any complete form, just enough to be able to point out the utility of understanding the basic ideas.   Also ran into "anubis", a language supposedly based on category theory (and I think from scanning the documentation,  topos theory).   This whole topic could easily be a (hard) graduate course. 

 

 

 30 March

Lots of reading later and I have a pretty good idea of what the talk will look like.  A preliminary outline can be found here. 

5 April

A first draft of the slides (actually open office presentation) here.  Not quite complete.

8 April

A second draft now here.   This is probably essentially complete.   Over the next few days I'll be proofing the slides and perhaps changing things to add a point here, delete one there.   Indeed, I'm likely to have the presentation open on my desktop more often than not.  This will also help me to mentally rehearse the flow of the talk.