Archive for papers

Typographic Style for Computer Scientists

Typographic Style for Computer Scientists is a short article intended to bring computer scientists up to speed on typographical issues. I started writing it several years ago, and then set it aside for other projects. Recently, I decided rather than wait for it to be “complete” and perfect that I should polish it up a little and see if people could benefit from it.

It is probably far from comprehensive, but hopefully some people will find it useful. I had been thinking of perhaps adding some material specifically on inference rules and judgments, but I am not sure what else it might make sense to include.

If you find mistakes please let me know. If you disagree on some of what I have said, let me know and perhaps I can address your concerns.

Comments (8)

Font identification

I've mentioned Identifont in the past, but I was just thinking that I should point out the existence of
WhatTheFont, a tool that will identify a font for you from an image. If failed to identify anything useful for the EPFL logo, but I doubt that corresponds to a real font. From a screen capture, it did correctly identify that the ∃xistential Type header at the top of the page is made from a member of the Warnock Pro family.

WhatTheFont was first brought to my attention on Daring Fireball.

Comments

A new species

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...

Comments (2)

Best quote from a paper this week

Programming in OMeta would be very frustrating if all productions were defined in the same namespace: two grammars might unknowingly use the same name for two productions that have different purposes, and one of them would certainly stop working! (Picture one sword-wielding grammar decapitating another, Highlander-style: “There can be only one!”)

From Warth and Piumarta's OMeta: an Object-Oriented Language for Pattern Matching.

Comments

Research update

I finished a draft of "Generalizing Parametricity Using Information-flow" for LMCS this past weekend. That should leave me with fewer distractions to work on something for ICFP.

My work on Featherweight Scala is moving along, sometimes more slowly than others. Other than the issues with singletons I have already discussed, one problem with the original definition of Featherweight Scala is that it did not truly define a subset of Scala proper – that is, there were many valid Featherweight Scala programs that were not valid Scala programs.

So I have been working on trying to get Featherweight Scala to be as close to a subset of Scala proper as is possible without making it far too complicated to be a useful core calculus. Some of this has involved changing the definition of Featherweight Scala. Some of this has involved lobbying for changes to Scala proper to make it more uniform (so far I've succeed with extending traits to allow value declarations to be overridden).

Through the whole process I've also been spending a lot of time typing things into the Scala interpreter to figure out how Scala proper treats them. For better or worse, I've actually managed to uncover a fair number of bugs in Scala proper doing this. I've almost reached the point where I treat it as a bit of a game: can I from thinking about the properties of the Scala type system come up with some corner case that will exhibit an unsoundness in the language (a ClassCastException, a NoSuchMethodException, etc.), or at least crash the compiler?

Last week I came up with a pretty nice one where I used the fact that Scala should not allow inheritance from singleton types to launder types in an unsafe fashion (now fixed in trunk!). Prior to that I came up with something fun where you could trick the compiler into letting you inherit from Nothing (which is supposed to be the bottom of the subtyping hierarchy). Today I got to thinking about Scala's requirements that paths in singleton types must be stable – all components of a path must be immutable. So for example in

  1.  
  2. var x = 3
  3. val y : x.type = x // ill-typed

The path x is not stable because x is a mutable variable. However, Scala does allow lazy value declarations to be stable.

  1.  
  2. var x = 3
  3. lazy val y = x
  4. val z : y.type = y // allowed, at present

Note that y is not evaluated until it is first needed, and in this case its evaluation involves a mutable reference. Furthermore, add into the mix that Scala also provides call-by-name method arguments (lazy values are call-by-need). So I started riffing on the idea of whether I could violate stability by changing the mutable reference between the definition of the lazy value, or a call-by-name argument, and its use. In retrospect, I am leaning at present towards the belief that there is no way this should be exploitable from a theoretical standpoint. That does not mean that the implementation is necessarily in alignment with theory, however. I did manage to hit upon a combination in my experiments that resulted in a NoSuchMethodException, so the exercise was not a complete letdown.

I should point out that these things do not really reflect on the quality of the Scala language as whole. It is a rich language that does not yet have a complete formal model, and as such, in the implementation process it can be easy to overlook some particularly perverse abuses of the language.

Comments

More notes on Featherweight Scala

As I mentioned the other day, Featherweight Scala has a typing rule that allows assigning a path (x.l1...ln) a singleton type:

Γ ⊦ p : T
-------------
Γ ⊦ p : p.type

(I should note that for some stupid reason WordPress seems to prevent MathML from working, making the rather pleasant <mfrac> tag useless). This is essentially the rule that everyone else uses, but in all the other literature I've looked at (other than νObj) the singleton is labeled with T (something like ST(p)) or T must have a specific type (int, base, etc.).

As I pointed out, Featherweight Scala's version of the rule makes it difficult to write meaningful inversion lemmas. Secondly, the naïve subject reduction theorem that could be obtained would be something like:

If Γ ⊦ t : T and t → t' then exists some T' such that Γ ⊦ t' : T'.

Which feels rather unsatisfactory. Given the subsumption rule for singletons

Γ ⊦ p : T
---------------
Γ ⊦ p.type <: T

It is plausible that a variant of the theorem where T is a subtype of T' would hold, but that would run counter to the expectations that reduction will only allow us to more precisely characterize the type of result. Thinking about it I suppose it might be reasonable to state the theorem as

If Γ ⊦ t : T and t → t' then there exists some T' such that Γ ⊦ t' : T' and
if there exists some p such that T = p.type then Γ ⊦ p : T', otherwise Γ ⊦ T' <: T.

Which I am starting to believe is the best that could be proven. This theorem nicely captures the discontinuities in subject reduction introduced by singleton types. You keep making steps getting a more and more precise type, and then suddenly you "jump" from one type to another, followed by some period where the type becomes more refined, then another "jump", and so forth.

These discontinuities are quite a problem, because it means that after taking a step it may not be possible in some cases to put the resulting term back into an evaluation context and remain well-typed.

νObj [1], the predecessor to Featherweight Scala, has nearly the same problem, but the language has been constructed just right so that typing always becomes more precise. The same changes cannot be made to Featherweight Scala and retain the property that the language is a subset of Scala. Aspinall's original work [2] on on singleton types makes use of an erasure predicate, but his singletons are labeled with a type making its definition trivial. Stone and Harper's work on singleton types [3] solves the problem by using a subject reduction theorem that looks roughly like

If Γ ⊦ t : T and t → t' then that Γ ⊦ t = t' : T.

but I am not sure there is a pleasant notion of term equality in Featherweight Scala, because all reductions either consult the heap or extend it. Singletons are also slightly more tractable in their setting because they require any term being used as a singleton type to have the base type "b".

[1] Martin Odersky, Vincent Cremet, Christine Röckl, and Matthias Zenger. A Nominal Theory of Objects with Dependent Types. Tech report 2002.
[2] David Aspinall. Subtyping with singleton types. CSL 1994
[3] Christopher Stone and Robert Harper. Extensional equivalence and singleton types. ACM TOCL 2006.

Comments (1)

Principia Narcissus finished

I just finished the last revisions on it today. If you like, you can purchase a bound copy from Lulu at cost. You can also download a copy from them, but it does not look like it will have the cover (or at least as part of a single download). I am hoping I can put together a PDF that contains the front cover for download.

One of the things that rather surprised me when I was making the final tweaks to the cover was that the width of the printed book Lulu sent me is actually 209mm rather than the 210mm you would expect for A4. However, this did not seem to impact anything, so I will not worry about it. My best guess is that a millimeter or so of the page width is lost due to the binding process. I was surprised to find that I had managed to quite accurately center the large orange text on the cover quite well by eyeballing it.

This final version contains a number of typographical fixes and small wording changes. Chapter 5 received the greatest number of edits as I decided to proofread the entire chapter again. It was the last chapter written and had received the least amount of scrutiny.

I really hope that somehow I did not introduce some kind of terrible printing problem or mistake in the process of fixing all the things I noticed that were wrong with the draft printing I received. If I did, I expect most of the recipients will probably not tell me.

Comments

Draft print of Principia Narcissus from Lulu

It just arrived this morning:

Draft printing of my dissertation

It looks pretty good, but there are definitely a few things I need to fine tune. For example, I need to center the text on the spine a little better.

Update: If you clicked through to Flickr, you would have seen my comment on it, but just in case, I should thank Tim Lindenbaum for kindly permitting me to use his daffodil photograph as the basis for the cover.

Comments (3)

Implementing my dissertation

Okay, I am finally getting around to writing something, as requested, about how I implemented my dissertation.

I used pdfLaTeX for several reasons:

  • I needed to integrate material from existing papers written in LaTeX.
  • Using standard LaTeX means that you need to fiddle dvips/dvipdf so that that they will find the appropriate fonts. Using pdfLaTeX requires some configuration too, but it all happens in a single step.
  • It has support for microtypography, which generally produces better looking text with fewer bad breaks.

I had thought about trying luatex to allow me to automate a few things better, but I decided against it because it might have slowed me down.

I then used the memoir class. I was able to use that with relatively little configuration. The only major change I made from the defaults involved the configuration for the chapter titles. I did however wind up needing to use a slightly modified version of the class file itself. This was necessary so that I could use raised dots (·) instead of periods as separators; there was simply no way to configure this for some parts of the document otherwise.

For the bibliography I used Chung-chieh Shan's McBride BibTeX style. I made a slight change to that so that the three emdashes for repeated authors did not have space in between them.

I use Didier Rémy's mathpartir package for typesetting inference rules.

I used my tool otftofd to generate all the LaTeX infrastructure for the OpenType fonts I used. I hacked up some custom OMakefiles for the TrueType fonts. The bits I used for Dejvu Sans Mono are now part of the package I have made available.

I wrote a small sed script for converting my examples written in InforML with some special markup in comments into a form that could be accepted by LaTeX.  This mostly involved escaping some characters and inserting uses of my macro for highlighting text.

That is everything I can think of from a high level.  If there is something specific I did in my dissertation that you would like to know about, let me know.

Comments

Absolutely done

I am finally absolutely and completely done with my doctorate. There is no doubt that I am now Doctor Washburn. On Tuesday, I deposited my dissertation, which proved to be more of an adventure than I expected.

For reasons I have not bothered investigating, LaTeX numbered the third page in the document as "ii" when it should have been "iii" (the first two pages are unnumbered).  However, this was the only mistake in terms of formatting that the ruler-lady noticed, so I only needed to reprint the pages numbered using lowercase Roman numerals.  She even offered up some of her spare sheets of the required 100% cotton, 20lb (or greater), acid free paper so that I could reprint the needed pages.  However, upon returning to Levine Hall to make the correction (\setcounter{page}{3} on the dedication page) and reprinting, I determined that we must have made an off-by-one error and the ruler-lady had given me one too few sheets.  So then I dashed off to the Penn Bookstore to purchase some more 100% cotton, etc. paper.  But I was able to get it all fixed and was even able to deposit the corrected pages without making a new appointment.

As far as double spacing goes, I went with a \baselinestretch of 1.5 as one of my colleagues said that he did so and it worked for him.  In practice, the ruler-lady did not actually ever lift her ruler from the table – not even to check the margins. She did ask me what size typeface I was using and whether my abstract was double spaced.

I have put a copy of the document that I deposited online.  I'm almost certain that the careful reader will find arbitrarily many typos, but I am also certain that I could expend an arbitrary amount of effort making it a better document and the returns were already diminishing. Still, if you do find any mistakes, please e-mail me so that I can fix them before I print up copies of the "director's cut" version via Lulu.

I am hoping that I will now have a little more time to write here on ∃xistential Type. I have a few non-typography related things that I will probably write up soon, for those of you bored by my endless tweaking of Gentzen Symbol.

Comments (11)

« Previous entries Next Page » Next Page »