mgreenblog

While on sabbatical in Cambridge, MA (thanks, Steve!), I had the good fortune to attend my first SPLASH.

I was particularly excited by one paper: Collapsible Contracts: Fixing a Pathology of Gradual Typing by Daniel Feltey, Ben Greenman, Christophe Scholliers, Robby Findler, and Vincent St-Amour. (You can get the PDF from the ACM DL or from Vincent's website.)

Their collapsible contracts are an implementation of the theory in my papers on space-efficient contracts (Space-Efficient Manifest Contracts from POPL 2015 and Space-Efficient Latent Contracts from TFP 2016). They use my merge algorithm to 'collapse' contracts and reduce some pathologically bad overheads. I'm delighted that my theory works with only a few bits of engineering cleverness:

• Racket's contracts are first-class values, which means subtle implementation details can impede detecting duplicates. Racket's contract-stronger? seems to do a good enough job---though it helps that many contracts in Racket are just checking simple types.
• There's an overhead to using the merge strategy in both space and time. You don't want to pay the price on every contract, but only for those that would consume unbounded space. Their implementation waits until something has been wrapped ten times before using the space-efficient algorithms.
• Implication queries can be expensive; they memoize the results of merges.

I am particularly pleased to see the theory/engineering--model/implementation cycle work on such a tight schedule. Very nice!

Have a comment? Send me an email!

This post originally appeared on weaselhat.com.