Free Theorems and Runtime Type Representations

’s abstraction theorem [21], often referred to as the parametricity theorem, can be used to derive properties about functional programs solely from their types. Unfortunately, in the presence of runtime lysis, the abstraction properties of polymorphic programs are no longer valid. However, runtime type analysis can be implemented with term-level representations of types, as in the λR language of Crary et al. [10], where case analysis on these runtime representations introduces type refinement. In this paper, that representation-based analysis is consistent with type abstraction by extending the abstraction theorem to such a language. We also discuss the “free theorems” that result. This work provides a foundation more general problem of extending the abstraction theorem to languages with generalized algebraic datatypes (gadts).

• Type: Journal
• Year: 2007
• Where: ENTCS
• Authors: Dimitrios Vytiniotis, Stephanie Weirich
• Keywords: Abstraction, Abstraction Properties, ENTCS 2007, Runtime Type Analysis