Lambda the Ultimate

This is the third meeting of SPLS, and its great to see that SPLS has already grown into what it was intended to be: a robust forum for language researchers in Scotland (and beyond). We had in attendance thirty or forty programming language researchers, from U of Edinburgh, Heriot Watt, U of Glasgow, Strathclyde, and St Andrews, as well as speakers from Nottingham and Hertfordshire, both of whom had traveled to Edinburgh just for the occasion.

Greg Michaelson noted that, as it happened, none of the speakers was Scottish. (Richard is English, Anne is French, Conor is Irish, De Lesley is American, and Sven-Bodo is German.) I suggested that we parse the name differently, and say that it is a seminar for work on Scottish Programming Languages. With POP2, SASL, Hope, ML, Haskell, and (soon, I hope) Links, we have quite enough to keep us busy!

We were hosted by the International Centre for Mathematical Sciences, which is located in the house in which James Clerk Maxwell was born. I work in The James Clerk Maxwell Building in the north campus of the University of Edinburgh, affectionately known as JCMB to its inmates (and rather a cheek in naming, as Maxwell's main connection to Edinburgh is that they refused to hire him). It was a pleasure to visit the other JCMB, which is more appealing in appearance. Cheers to Greg and Phil for finding a wonderful venue.

Richard Connor, Strathclyde University
Typed vs Untyped: performing a real experiment?

Put forward the excellent idea that we should actually try to experimentally measure what impact type systems have on programmer productivity and program reliability and maintanability. Unfortunately, I suspect this will fall foul of a symptom I noticed years ago in papers that report experiments on programming languages. If the person who wrote the paper believed that imperative languages were better than functional languages, thenthat is what his experiments proved, and if the person who wrote the paper believed the opposite then his experiments proved the opposite. Richard's experiment consists of comparing untyped and typed variants of Javascript. But his untyped variant supports the undefined value and his typed variant does not, so its not clear whether he'll be measuring the effects of typing or of flexible null values. I can suggest a number of different experiments, which I suspect would yield rather different results: compare Java 1.4 and Java 1.5 (with and without generics -- this has the great advantage that it is working with two real languages), compare Haskell with and without types, compare Scheme with and without types (using the type inferencer in Dr Scheme for the typed version, so again you have two real languages).

Anne Benoit, Edinburgh University
Enhancing the performance of Grid Applications with Skeletons and Process Algebras

Skeletons with performance models applied to automatically choose the best implementation. Seems like nice work. Unfortunately, I'm not very familiar with skeletons, so I would have benefited from some simple, complete examples to convey the basic ideas.

Conor McBride, Nottingham University
Idioms

A few years ago, John Hughes noticed that sometimes a monad is too strong, and he introduced a weaker structure called 'arrows' with many interesting applications. (Every monad is an arrow, but not conversely.) Conor has now noticed that there is another useful structure halfway between arrows and monads, which he calls idioms. (Every monad is an idiom and every idiom is an arrow, but not conversely.)

  class Idiom i where
    k : x -> i x
    s : i (x -> y) -> i x -> i y

(To see why these are called k and s, take i x = a -> x.) It was a Pearl of a talk, and I encourage him to write it up as a pearl for JFP.

DeLesley Hutchins, Edinburgh University
Feature Oriented Programming

An object calculus that is good for "deep mixin" combination. Unlike most typed languages it is not stratified -- objects and their types are considered to be the same sorts of things, with the

Sven-Bodo Sholz, University of Hertfordshire
Using Sub-types and Intersection Types to strike the Balance Between Static and Dynamic Typing

An interesting companion to Richard's talk. Sven-Bodo has a functional language for scientific programming with an optimizing compiler that achieves performance comparable to Fortran. (And a compiler consisting of 500K lines of C.) This talk focussed on the type system, which in effect ranges from highly typed to untyped. He has a hierarchy of types for arrays, ranging from no information to specific information.

  [*]  - any array
  [] - any scalar   [.] - any vector   [.,.] - any matrix
  [3] - vector of length 3, [4] - vector of length 4, [2,3] - matrix with 2 rows and 3 columns, ...

The system makes heavy use of intersection types. It tries to give more precise types (lower down in the hierarchy sketched above), but moves up the hierarchy when it is too hard to give a precise type. (It wasn't clear to me under which circumstances it would move up the hierarchy.) This complements Milner's principle: Well-typed programs can't go wrong. In this system, if a program is not well-typed it will typically move up the hierarchy. Hence. one can't guarantee that well-typed programs won't go wrong (unless one inspects them and determines that all subterms are given precise types rather than imprecise types), but one can guarantee that ill-typed programs must go wrong!

A fine day. My thanks to all those who made it happen! The next meetings are scheduled for Strathclyde in September and St Andrews in January.