Last week, my co-supervisor gave me the Steam Boiler Problem. It’s a classical problem for specifications languages. You have a computer monitoring a steam boiler: a giant tank of water with a heat source and a steam pipe at the top. There are water pumps to control—to add more water into the tank—and a series of sensors. Essentially, given complex specifications, you have to get the steam boiler into a functioning state and keep it that way. Sensors can start malfunctioning, too, to make it more difficult.

It’s a good problem because it forced me to look at how Ca is to work with in the flesh, in a complex example. Even though I’m not done, the conclusion is that it needs a lot of syntactic sugar built on top of it.

Some of them are rather superficial, if time-consuming. For example, currently patterns cannot overlap at all in Ca, so something like:

l {
  Cons 5 xs -> ...;
  Cons x xs -> ...;
  _ -> ...;
};

Is not allowed, though it really should be. I had no idea before now how irritating it is not having that feature. There are other minor syntax features like that that need to be addressed.

The more interesting case is what to do with the catamorphisms. Theoretically they work fine, almost. In practice, they’re a bit cumbersome. When I said “almost” before, I meant they worked fine up to Loïc Colson’s famous inférieur (“minimum”) problem. It pertains to primitive recursive schemes like the one I’m working with, were writing the “minimum function”—finding the minimum of two values—has greater time complexity than in an unrestricted computational model.

What this boils down to in my mind is the inability to perform a catamorphism over two objects simultaneously. Or stated in a more Haskell-ish way, there’s no efficient way to write the zip function.

One solution floating in my mind is to make the catamorphism construct explicitly allow zipping. It’s not too bad adding it in. The syntax would be something like so:

(l, n) {
  (Cons x xs, p+1) -> ...;
  (Nil, 0) -> ...;
};

Where l is a list and n is a natural number.

Another possible solution, which I quite like, is the idea of making catamorphisms parametric. So you could do something like so:

{ i ->
  Cons x xs -> i * x + @xs x;
  Nil -> i - 2;
} l 0;

The variable i is a parameter over the catamorphism, initially 0. I like this is as it makes a lot of things more natural and doesn’t add any computational power. The syntax for the catamorphism has to change, but I think this is for the best anyway.

Advertisements