Threesomes, with and without blame

Jeremy G. Siek, Philip Wadler

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

How to integrate static and dynamic types? Recent work focuses on casts to mediate between the two. However, adding casts may degrade tail calls into a non-tail calls, increasing space consumption from constant to linear in the depth of calls.

We present a new solution to this old problem, based on the notion of a threesome. A cast is specified by a source and a target type--a twosome. Any twosome factors into a downcast from the source to an intermediate type, followed by an upcast from the intermediate to the target---a threesome. Any chain of threesomes collapses to a single threesome, calculated by taking the greatest lower bound of the intermediate types. We augment this solution with blame labels to map any failure of a threesome back to the offending twosome in the source program.

Herman, Tomb, and Flanagan (2007) solve the space problem by representing casts with the coercion calculus of Henglein (1994). While they provide a theoretical limit on the space overhead, there remains the practical question of how best to implement coercion reduction. The threesomes presented in this paper provide a streamlined data structure and algorithm for representing and normalizing coercions. Furthermore, threesomes provide a typed-based explanation of coercion reduction.
Original languageEnglish
Title of host publicationProceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages (POPL '10)
Place of PublicationNew York, NY, USA
PublisherACM
Pages365-376
Number of pages12
ISBN (Print)978-1-60558-479-9
DOIs
Publication statusPublished - 2010

Keywords

  • blame tracking
  • casts
  • coercions
  • lambda-calculus

Fingerprint

Dive into the research topics of 'Threesomes, with and without blame'. Together they form a unique fingerprint.

Cite this