A few off-topic topics

I saw that the great science-fiction writer Stanislaw Lem died this morning at the age of 84. Lem is probably best known for writing Solaris, which was adapted into a movie in 1972 by Tarkovsky and again in 2002 by Steven Soderbergh (starring George Clooney), but he's got a great many great novels to his name. I've only read five or six, but I've enjoyed every one I've read — in particular I think The Cyberiad might be my favorite book of any genre at all.

In happier news, congratulations to my dad, John Matthews, who on Friday became Dr. John Matthews when he successfully defended his dissertation on public policy. Dad worked for various city and county governments for many years, then took an early retirement and went back to school to get his PhD. Just think, he gave me a gigantic head start and still finished his PhD before I did! Oh well. Congratulations to him.

Quartz Composer: the world's most widely-used functional-reactive programming language

A couple days ago, Apple held a "Technology Update Briefing" here at University of Chicago. A "Technology Update Briefing," as it turns out, is where they send a developer around to demo all the cool new developer toys they've hidden away in Tiger, mostly in the XCode package you installed because you wanted GCC.

Our developer, Steve Hayman, pointed out a bunch of neat toys. He started out by pointing out a couple things I'm sure most developers who use Macs already know: for one thing, OS X has Unix inside and so you can use pipes if you want; and for another, the new Automator tool is a lot like a GUI's notion of piping (the robot is actually holding a pipe in reference to that). So far the talk was entertaining but didn't tell me anything I didn't already know.

But the next thing he pointed out was really new and totally cool: Quartz Composer. Quartz Composer is an application that comes with XCode on Tiger, so you've probably already got it installed (I did, anyway). What it does is allow you to build QuickTime objects, like movies and so on, by gluing together "patches" to create a pipeline, purely declaratively. Of course as far as Apple is concerned, it's a "visual programming environment" where you make graphical programs "without writing a single line of code", but of course that's not really where the sysmem's power comes from — you don't type in a single line of code, but as far as I'm concerned drawing lines between boxes on the screen and the other visual manipulation you do is just an incidental difference.

The real power of Quartz Composer is that it's purely declarative. If you want a bouncing ball, you don't write a loop that update's the ball's Y-coordinate once every however-many fractions of a second; you attach the ball's Y-coordinate input to the output of a low-frequency oscillator whose value depends on the time. If you want this morning's headlines from the BBC to show up on the screen, you make a text displayer and attach its text input to the output of an RSS feed monitor. If you want that text to follow your mouse around the screen, you attach its X- and Y-coordinates to monitors of your mouse's X and Y positions.

They never say it, but what they've implemented is functional-reactive programming, and by virtue of the fact that it's shipped with Tiger I'm willing to bet that it's the world's most widely-used FRP implementation. Furthermore, the Quartz Composer programs you can find online (for instance here) demonstrate that the approach scales way up.

Scheme semantics in Maude

I just stumbled on some work that's related to the R5RS operational semantics paper I wrote recently. Right at about the same time I was doing that, some folks on the Maude team did a Maude-based rewriting semantics for Scheme also, and wrote a paper about it for the Brazilian Symposium on Programming Languages called "An Equational Specification for the Scheme Language" (source code). It looks like they didn't model the two things that gave me the most trouble (unspecified order-of-evaluation and multiple values). Also, they're excited about the fact that their model of call/cc is so small, but that's because their entire system is in CPS style ...

Anyway, it's interesting to compare their system to ours and see how our different priorities led to different systems. For instance they've got an entire section on performance metrics. Performance was explicitly a non-goal for us. If our paper had a section on performance, it would read something like: "We were able to compute (fib 7) in, like, an hour or so."

Olin Shivers' SRE notation

I just got pointed at Olin Shivers' SRE regular-expression notation design document. Not only is it a really neat, elegantly-designed library that I'm a little surprised we haven't all adopted yet, but it's also got a pretty great preamble that's worth reading just by itself.

... [L]et's take the case of someone who wants to do web hacking in Scheme. His Scheme system doesn't have a sockets interface, so he sits down and hacks one up for his particular Scheme implementation. Now, socket API's are not what this programmer is interested in ... So he does a quick 80% job, which is adequate to get him up and running, and then he's on to his orignal goal.

Unfortunately, his quickly-built socket interface isn't general. It just covers the bits this particular hacker needed for his applications. So the next guy that comes along and needs a socket interface ... does his *own* 80% implementation. Five hackers later, five different, incompatible, ungeneral implementations had been built. No one can use each others code.

The alternate way systems like this end up going over a cliff is that the initial 80% system gets patched over and over again by subsequent hackers, and what results is 80% bandaids and 20% structured code. When systems evolve organically, it's unsuprising and unavoidable that what one ends up with is a horrible design -- consider the DOS -> Win95 path.

I'm a Rejected Scientist

That was fast. We just heard back on the paper we wrote for Science that I mentioned last week; REJECTED! Not a big surprise at all, of course. Would've been nice, though ...

More on polymorphic contracts

It's remarkable how fragile some results of type theory can be. Last time I wrote about polymorphic contracts, I offhandedly mentioned that in an ML-like language a function of type ∀α.α→α might memorize the first argument that it is provided with at runtime and thereafter always return that value. I was actually thinking of a full System F + state language; I'm pretty sure that it isn't possible to write a function that behaves that way in actual SML. Surprisingly, though, you can get a polymorphic memory function if you're willing to relax the type to ∀α.unit→α→α. Here it is:

let val (f : unit -> 'a -> 'a) =
     fn _ =>
      let val memory = ref NONE in
       fn x =>
          case !memory of
       NONE => (memory := (SOME x); x)
            | (SOME y) => y
      end
    val g'  = f()
    val g'' = f()
in
    (g' 1, g' 2, g'' "hello", g'' "goodbye")
end

This program typechecks in SML and produces the value (1,1,"hello","hello").

So what's going on here? It doesn't seem like taking an additional unit value should affect anything, but clearly it does. Here's why: when you apply a polymorphic function in ML, you're actually doing two things: first, you're supplying the function a value argument, and second, you're implicitly supplying it with concrete types for all its type variables. (You have to do both of these at the same time because of SML's value restriction.) So, if you're writing a function of type ∀α.α→α, then every time you call it with a new value, you're also calling it with a new type. If you have one piece of memory for all of these calls, then you might remember an argument of type α when α = int and then return it when α=string, which would violate ML's safety guarantee.

Now instead let's say you're writing a function with type ∀α.unit→α→α. Now when you call the function for the first time, you're supplying it with the trivial unit value and also a particular choice for α. Now, in the body of that function you can set a cell of memory that only holds values of that particular choice for α, and then a function that consumes and produces a value for that same choice of α. In essence, that first unit argument is just there to hack around the value restriction; it gives us a way to do some computation in between picking the particular type we want to use for α and coughing up a function that consumes and produces αs.

So, what does this have to do with polymorphic contracts? Well, I've got a prototype polymorphic contract implementation working, and this exact issue pops back up but in a form that's a little more annoying. In order to be able to write down ML functions like the one I've posted here and have them typecheck, you pretty much need to understand ML's type system. You simply can't execute a program that doesn't work. Polymorphic contracts, on the other hand — it's easy to write down a program using polymorphic contracts that will definitely cause a contract violation in the right contexts (like if you write a memory function and give it contract ∀α.α→α) and then execute that program, maybe even succeed on lots of inputs, without noticing you've done anything wrong.

More about speed-dating

I'm not sure if I mentioned this before, but the Science paper I mentioned a few days ago isn't the first speed-dating paper I've been involved in. The first was a paper on how to run a speed-dating event for the purpose of studying interpersonal relationships; Eli Finkel, Paul Eastwick and I submitted it to a psychology journal in December.

Today we heard back about it. The editor sent us a very encouraging letter that asked us to revise and resubmit it. Furthermore, the four anonymous reviewers seemed to really really like it, though of course they each had something big they wanted changed. All in all, it hasn't been accepted yet but it's a pretty sure bet that it will be after a round or two of edits. Yay!

I'm a Scientist

As of today, I may officially call myself a Scientist, by the very technical and totally non-common-use definition that I have a paper submitted to the journal Science. It's not about computer science at all; it's about speed-dating. Anyway, as of a couple days from now I'll be able to call myself a Rejected Scientist, but it's fun for now.

Polymorphic contracts

What does it mean for a the ML or Haskell type checker to give your function the type ∀α.α→α? It means that even though you haven't told the compiler what type T you're thinking of, it can prove that your function has type T→T anyway. After a moment's reflection you realize (and after a huge pile of math you can prove) that the only way the type checker could do that is if your function has all of those types simultaneously, so it (a) doesn't do anything to its argument and (b) returns that argument intact. Or maybe it diverges on all inputs, or maybe it remembers prior values it's been given and returns one of those or something like that, but it never makes up new values and returns those.

So, what does it mean if you give a Scheme function the contract ∀α.α→α? One interpretation is that you're asserting that your function satisfies all of the contracts C→C for every C simultaneously. There's only one way you can say that; it's if your function returns its argument intact, or diverges on all inputs, or returns a previously-remembered input value. (That's easy enough to show based on the view of contracts as pairs of projections, incidentally.) It may make first-order observations about its argument, but it cannot do anything to it that would assume any particular contract on it, like seeing that it's a procedure and calling it with an argument. If you do, it's a contract violation because whatever you do there's some contract that your use would be violating. That system almost already implemented in the current PLT Scheme contract library, in the form of anaphoric contracts.

There's another way to do it, too, though, based on a different interpretation. We could also interpret the contract ∀α.α→α to mean, "for any contract C you give me, I can give you back a function that satisfies the contract C→C." In this interpretation, contracts aren't analagous to for-all types, they're analagous to kinds in the sense of System F_ω. In this system, a function gets to know the contract it's expected to conform to, and it might be able to take special action based on that knowledge. It's more powerful, but also more difficult to use: your function has to explicitly take in a contract, and anywhere you use it you've got to tell it the contract you're thinking of. Furthermore, it's not really a "contract" anymore, since it's not a projection on values directly; it's more a "contract kind."

This system is technically already possible in the PLT Scheme contract system: (->d contract? (lambda (c) (-> c c))) is the contract kind that produces C→C contracts.

[Edit 3.08.06 9:34: "Anaphoric", not "anamorphic" (nor "Anamorphic", and definitely not "Animorphic"). Thanks Dave!]

electronic music in Scheme with impromptu

Here's a neat project that got mentioned over the plt-scheme mailing list at some point: impromptu, a Scheme/OSX-based electronic music environment. I've been casually interested music-specific programming languages for a while, but up until now the best thing I'd found was CSound which doesn't thrill me.

My main reason for being interested is that I think music could be a very natural way to teach students about higher-order functions: a sound is a function from time to frequency, and all sound operations become function composition. Want to make a 5-second sound clip last 10 seconds instead? It's a one-liner. Want to shift the pitch up or down? Just as easy. Want to do both? No problem. I think it's a really natural way to think about sound that leads just as naturally to higher-order functions, and that's pretty cool. It's also the sort of thing I can imagine one or two kids really nerding out over, which is definitely a bonus.

You may not like Tait's Method, but you've got to admit ...

It seems like everything I'm learning these days is coming from unpublished books. For a long time I was reading stuff from Felleisen and Flatt's Programming Languages and Lambda Calculi (google for it); from it I got a foothold on contextual equivalence after quite a bit of struggling. Then, more recently, I discovered Bob Harper's Type Systems for Programming Languages (available from his homepage), which has a great amount of good material and also talks about contextual equivalence in a totally different way from Felleisen and Flatt. (For instance see his discussion of "ciu-equivalence".)

Anyway. Sorry for the lack of updates. Strangely, the more I'm doing the less I can write about, and I've been very busy lately. I've been doing a tremendous amount on my multi-language semantics project recently and I'd love to talk about all of it, but unfortunately all of it is a bit too fresh for me to talk about it here.

What I can do, though, is take this opportunity to publicly praise Derek Dreyer's advanced type theory class for directly helping the research I'm working on now. Derek's class is the first class in which I had to understand the proof that the simply-typed lambda-calculus terminates; I learned how to do that proof about six weeks ago, and this afternoon I adapted it to complete the proof of a very surprising multi-language systems result. Imagine that! Things that I learn in school being relevant to research!