Lambda the Ultimate

Using Category Theory to Design Implicit Conversions and Generic Operators, John C. Reynolds, 1980. (Try this if the official link doesn't work.)

A generalization of many-sorted algebras, called category-sorted algebras, is defined and applied to the language design problem of avoiding anomalies in the interaction of implicit conversions and generic operators. The definition of a simple imperative language (without any binding mechanisms) is used as an example.

This is an old, but still cute, paper. The basic intuition is that a good design principle for a language with implicit conversions is that whatever order of conversions the language takes, you should get the same result. He then formalizes that by giving a category of types and conversions, and demanding that everything commute properly. And these give just the conditions the language designer has to check to make sure that he or she hasn't screwed anything up.

Someone could probably get a fun little paper by taking this idea and shooting some dependent types into it. (Maybe somebody already has?) If you've got an abstract type, a coercion function, and a proof that it satisfies Reynolds' conditions, now your compiler can silently insert those coercions for you as needed, but you can still be sure that it won't mess up the meaning of your program.

In the context of programming languages, why distinguish types and classes? People seem to use these two terms interchangeably. Is this because there is no or little difference, or this is by mistake?

I am pleased to announce that twenty-one talks from Dan Friedman's 60th birthday festschrift are now on Google Video. You can find links to the talks on the official DanFest home page. Every LtU reader should find at least several talks of interest:

• Andrew Hanson: Welcome to DanFest
• Mitch Wand: Relating models of backtracking
• Lynn Winebarger: Extending Scheme for bottom-up relational programming
• Bil Lewis: Debugging backwards in time
• Steve Ganz: Monadic Encapsulation of State
• Kent Dybvig: The guaranteed optimization clause of the macro-writer's bill of rights
• David Wise: Introduction for Guy Steele's keynote address
• Guy Steele: Dan Friedman: Cool Ideas (Keynote address)
• Olin Shivers: The anatomy of a loop: a story of scope and control
• Kevin Millikin: Obfuscating transformations via abstract interpretation
• Bob Filman: Poetry in programs: A brief examination of software aesthetics, including some observations on the history of programming styles and some speculations on post-object programming
• Gerald Jay Sussman: The role of programming in the formulation of ideas
• Anurag Mendhekar: Aspect-oriented programming in the real world
• Shriram Krishnamurthi: Verification of web programs
• Jim Marshall: Introductory cognitive science course using Scheme
• Rhys Price Jones: DNA analysis
• Oleg Kiselyov: Normal-order syntax-rules and proving the fix-point of call/cc
• Julia Lawall: On designing a target-independent DSL for safe OS process scheduling components
• Kathi Fisler: Aspect verification using model checking
• Jonathan Sobel: Implementing Categorical Semantics
• Matthias Felleisen and Robby Findler: An investigation of contracts as projections

DanFest was previously mentioned on LtU. In fact, Ehud wrote, "I sure wish that [Guy Steele's] keynote was available online somewhere.". Not only will you enjoy the keynote, Ehud, but you might even find a talk given in the style of The Little Schemer. :-)

In addition to watching the talks online, you can download the videos to your computer and watch them at a higher resolution with Google Video Player.

Enjoy!

--Will