Skip navigation

Greetings, QA9 reader(s).  It has been a while since I posted, for which I offer the usual excuses.  I have a backlog of interesting technical things I’m hoping to write about sometime pretty soon: failure of subject reduction in lambda2 with eta-contraction, which I learned about maybe a year ago but did not record in a post; also intriguing things I am reading about deep inference, although there the problem is the stuff is, well, deep and I haven’t understood it well enough yet to have too much to say.  I also had high hopes of posting about the super fun summer I had here at U. Iowa working on Cedille with great new U. Iowa graduate students Chad Reynolds, Ananda Guneratne, and Richard Blair; great visiting Indiana doctoral student Matthew Heimerdinger; and inspiring visitors Stéphane Graham-Lengrand, Olivier Hermant, and Vincent St-Amour.  In a perfect world I would have some pictures to post of all this stimulating interaction, but here I am photo-less.

But what impels me to write today is getting bitten again by performance problems with well-founded recursion in Agda.  Just for fun, I will tell you the story.  We are working on this new interactive theorem prover called Cedille based on dependently typed lambda encodings.  You can read about this in the project report we just revised to submit for the TFP 2016 post-proceedings.  Thanks to the determination of Matthew (Heimerdinger), we have a highlighting mode — actually several — for Cedille in our emacs interface.  One funny wrinkle was that we could not highlight comments, because our parser was just dropping them, and we did not want to store information about them in our abstract syntax trees (which would then become very cluttered).  We hit upon a daring (for us, anyway) solution: parse input files a second time, with a different grammar that is recognizing just whitespace and comments.  It is nice to find the whitespace, too, in addition to the comments, since then we can set highlighting to the default for those spans of the text in the emacs mode.  Otherwise, with the way our interaction between emacs frontend and Agda backend works (see that revised project report), if you type in whitespace you will likely get a non-default highlighting color, from the span containing that whitespace.

Ok, so we (Richard) wrote the grammar for this, and we started producing comment and whitespace spans to send to the frontend, only to see some very sluggish performance on a couple longer files.  We misdiagnosed this as coming from doing lots of string appends (with what correspond to slow strings in Haskell; i.e., lists of characters), and I dutifully changed the code to print the spans to a Haskell Handle, rather than computing one big string for all the spans and then printing that.  Distressingly, this optimization, which took maybe an hour or so to implement, with finding the right Haskell stuff to hook up to, did not improve performance.  Well shucks!  Let’s get out our handy Haskell profiler and see what is going wrong.  Now sadly, I am still on Agda 2.4.2.4, which lacks this nifty agda-ghc-names tool that is part of Agda 2.5.1 now.  That tool translates Haskell names that are generated by the Agda compiler, back to names from the Agda source.  But this tool was not needed to see the following:

COST CENTRE MODULE %time %alloc

d179.\.\.\ MAlonzo.Code.QnatZ45Zthms 35.9 18.8
d179.\ MAlonzo.Code.QnatZ45Zthms 11.6 48.8
d191.\ MAlonzo.Code.QnatZ45Zthms 9.6 7.5
d179 MAlonzo.Code.QnatZ45Zthms 5.7 0.0
d191 MAlonzo.Code.QnatZ45Zthms 5.2 0.0
d179.\.\ MAlonzo.Code.QnatZ45Zthms 4.7 11.3

 

Oh pondwater.  Over half the time is being spent in functions in nat-thms.agda in the IAL.  That file contains, as the name suggests, just theorems about the natural numbers — not code I expect to be running intensively during execution of the Cedille backend.  But I have seen this before, as I noted.  These are lemmas getting called again and again during a well-founded recursion, to show that certain less-than facts hold.  Which well-founded recursion was it?  It turns out it was for the function that converts a natural number to a string.  We are doing that operation many times, to print character positions in the input Cedille source file.  Just removing the well-founded recursion and marking the nat-to-string function as needing NO_TERMINATION_CHECK reduced the running time to less than half what it was.

The moral of this story is the same as the moral of the previous story: be wary of well-founded recursion in Agda for code you intend to run (as opposed to just reason about).

Have a blessed start of fall!

Advertisements

2 Comments

  1. Hi, Aaron,
    Thanks for bringing up the issue of eta reduction breaks the subject reduction for System F. I came across a paper “Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism” by Joshua Dunfield and Neelakantan R. Krishnaswami. There they discuss how to achieve typability under eta-reduction. I think they also provide an example where eta reduction breaks the subject reduction.

    Let G = f : Unit -> forall a . a, then we know that G |- \ x . f x : Unit -> Unit. If the subject reduction holds for eta reduction, then we would have G |- f : Unit -> Unit, but this can not be the case under the context G.

    I didn’t realize this is a fundamental problem of System F until I recall your post claiming that.

    Best.
    Frank

  2. Thanks for posting this example! This is nice and simple — maybe the simplest one can think of for this issue.

    Whether or not this is a big problem depends on how important one thinks eta-reduction is, I suppose.

    Aaron


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: