Skip to main content
Home

Main navigation

  • Home
  • Series
  • People
  • Depts & Colleges
  • Open Education

Main navigation

  • Home
  • Series
  • People
  • Depts & Colleges
  • Open Education

Theorems for Free for Free: Parametricity, With and Without Types

Series
International Conference on Functional Programming 2017
Video Embed
Amal Ahmed (Northeastern University, USA) gives the first talk in the fourth panel, Integrating Static and Dynamic Typing, on the 3rd day of the ICFP conference.
Co-written by Dustin Jamner (Northeastern University, USA), Jeremy G. Siek (Indiana University, USA), Philip Wadler (University of Edinburgh, UK).

The polymorphic blame calculus integrates static typing, including universal types, with dynamic typing. The primary challenge with this integration is preserving parametricity: even dynamically-typed code should satisfy it once it has been cast to a universal type. Ahmed et al. (2011) employ runtime type generation in the polymorphic blame calculus to preserve parametricity, but a proof that it does so has been elusive. Matthews and Ahmed (2008) gave a proof of parametricity for a closely related system that combines ML and Scheme, but later found a flaw in their proof. In this paper we present an improved version of the polymorphic blame calculus and we prove that it satisfies relational parametricity. The proof relies on a step-indexed Kripke logical relation. The step-indexing is required to make the logical relation well-defined in the case for the dynamic type. The possible worlds include the mapping of generated type names to their types and the mapping of type names to relations. We prove the Fundamental Property of this logical relation and that it is sound with respect to contextual equivalence. To demonstrate the utility of parametricity in the polymorphic blame calculus, we derive two free theorems.

More in this series

View Series
International Conference on Functional Programming 2017

Gradual Session Types

Peter Thiemann (University of Freiburg, Germany) gives the fourth talk in the third panel, Contracts and Sessions, on the 3rd day of the ICFP conference.
Previous
International Conference on Functional Programming 2017

On Polymorphic Gradual Typing

Yuu Igarashi (Kyoto University, Japan) gives the second talk in the fourth panel, Integrating Static and Dynamic Typing, on the 3rd day of the ICFP conference.
Next
Licence
Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK: England & Wales; http://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Episode Information

Series
International Conference on Functional Programming 2017
People
Amal Ahmed
Keywords
technology
programming
computing
Department: Department of Computer Science
Date Added: 22/01/2018
Duration: 00:20:38

Subscribe

Apple Podcast Video Video RSS Feed

Download

Download Video

Footer

  • About
  • Accessibility
  • Contribute
  • Copyright
  • Contact
  • Privacy
'Oxford Podcasts' Twitter Account @oxfordpodcasts | MediaPub Publishing Portal for Oxford Podcast Contributors | Upcoming Talks in Oxford | © 2011-2022 The University of Oxford