I spent some time last night looking more closely at Carette and Uszkey's new paper on species, as mentioned recently on Lambda the Ultimate. I mostly concentrated on the first few sections and the Haskell bit at the end. They say many tantalizing things, and I had kind of hoped the punchline would be something like "here is how you can write code in a beautifully functional style over graphs and cyclic structures" (assuming I understood the potential of species correctly).  Perhaps in a follow up paper.

I also found it interesting that their dot product operator sounds more like the traditional Cartesian product type (one of each type), and their Cartesian product type sounds much more like an intersection type (the value is a structure having both types). Perhaps it is a notational holdover from previous work on species. It also seem to make for some nice concrete examples of the "locative" aspects of Girard's Ludics.

Now back to reviewing journal and ICFP papers...

Yesterday, I discovered that most (if not all) of Hermann Zapf's Manuale Typographicum is available online. I am not sure about the legality of the site, but given the limited availability of hard-copies, it gives some people an opportunity that they might not otherwise have.

One of the things that will show up in the imminently forthcoming Scala 2.7.1 release candidate, is the addition of traits for representing equivalence relations, partial orderings, and total orderings. Previously, the trait Ordered was used for representing totally ordered things:

trait Ordered[A] {
def compare(that: A): Int
def <  (that: A): Boolean = (this compare that) <  0
def >  (that: A): Boolean = (this compare that) >  0
def <= (that: A): Boolean = (this compare that) <= 0
def >= (that: A): Boolean = (this compare that) >= 0
def compareTo(that: A): Int = compare(that)
}

However, the Ordered trait does not provide a representation of a total ordering. Therefore, the new trait Ordering:

 
trait Ordering[T] extends PartialOrdering[T] {
  def compare(x: T, y: T): Int
  override def lteq(x: T, y: T): Boolean = compare(x, y) <= 0
  override def gteq(x: T, y: T): Boolean = compare(x, y) >= 0
  override def lt(x: T, y: T): Boolean = compare(x, y) < 0
  override def gt(x: T, y: T): Boolean = compare(x, y) > 0
  override def equiv(x: T, y: T): Boolean = compare(x, y) == 0
}
 

The tricky part however, was writing description of the properties required of something that implements the Ordering trait. When one normally thinks of a total ordering one thinks of a relation that is

• anti-symmetric,
• transitive,
• and total.

The problem is that Ordering is not defined in terms of a binary relation, but a binary function producing integers (compare). If the first argument is less than the second the function returns a negative integer, if they are equal in the ordering the function returns zero, and if the second argument is less than the first the function returns a positive integer. Therefore, it is not straightforward to express these same properties. The best I could come up with was

• compare(x, x) == 0, for any x of type T.
• compare(x, y) == z and compare(y, x) == w then Math.signum(z) == -Math.signum(w), for any x and y of type T and z and w of type Int.
• if compare(x, y) == z and lteq(y, w) == v and Math.signum(z) >= 0 and Math.signum(v) >= 0 then
  compare(x, w) == u and Math.signum(z + v) == Math.signum(u),
  for any x, y, and w of type T and z, v, and u of type Int.

Where Math.signum returns -1 if its input is negative, 0 if its input is 0, and 1 if its input is positive.

The first property is clearly reflexivity. I call the third property transitivity. I am not sure what to call the second property. I do not think a notion of totality is required because it is assumed you will always get an integer back from compare rather than it throwing an exception or going into an infinite loop.

It would probably be a good exercise to prove that given these properties on compare hold if and only if lteq (defined above in terms of compare) has all the normal properties of a total ordering.

The problem with being a programming languages researcher is that you can wind up like a blacksmith who spends all of his time tweaking his hammer and anvil, instead of producing less esoteric artifacts.

With the ICFP deadline out of the way, I've finally put up a new version of my academic website, now hosted at EPFL: http://lamp.epfl.ch/~washburn/.

This website includes a link to a draft of my ICFP submission, "InforML: Scrapping your boilerplate with integrity", the previously mentioned draft version of "Generalizing parametricity using information-flow" submitted to LMCS, and a version of Principia Narcissus with the front and back cover included as part of the PDF (for those that would like that sort of thing).

I am a bit worried that my ICFP submission is just too dense to be comprehensible to someone who is not only well-versed in the area of type systems but also information-flow. I will see I guess.

I discovered last night that Appendix B.4 of Fonts & Encodings is almost an exact copy of Appendix B.2, with a couple changes made, but overall the text is not appropriate to the expected content.  Appendix B.2 describes the OFM file format, and Appenidx B.4 the OVF format, but in B.4 most of the time it claims to be explaining OFM.  Given the size of the tome, I was not too surprised that this is not yet in the reported errata.

Despite everything the book covers I have also managed to find that one thing it does not really explain much about is the special font metrics used by TeX for typesetting mathematics.  They are named in the description of the TFM file format, but that seems to be the extent of the coverage.  In some sense this is partly okay, because the various TeX documentation explains what the parameters do.  The trouble is that I have yet to figure out how you can set them for existing fonts, short of hacking the TFM files generated by otftotfm or afm2tfm manually.  You might think this is something you could do with the TeX virtual font mechanism, but Fonts & Encodings specifically says that the metrics in a TFM file must match the virtual font because TeX only reads the TFM.