Skip to main content

Translating Generalized Algebraic Data Types to System F

Sulzmann, Martin and Wang, Meng (2005) Translating Generalized Algebraic Data Types to System F. Technical report. National University of Singapore (Unpublished)

Abstract

Generalized algebraic data types (GADTs) extend ordinary algebraic data types by refining the types of constructors with syntactic equality constraints. This is highly useful and allows for novel applications such as strongly-typed evaluators, typed LR parsing etc. To translate GADTs we need to enrich the System F style typed intermediate languages of modern language implementations to capture these equality constraints. We show that GADTs can be translated to a minor extension of System F where type equality proofs are compiled into System F typable proof terms. At run-time proof terms evaluate to the identity. Hence, they can be safely erased before execution of the program. We provide evidence that our approach scales to deal with extensions where equality is not anymore syntactic. The benefit of our method is that type checking of target programs remains as simple as type checking in System F. Thus, we can offer a light-weight approach to integrate GADTs and extensions of it into existing implementations.

Item Type: Monograph (Technical report)
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Meng Wang
Date Deposited: 01 Mar 2015 16:55 UTC
Last Modified: 29 May 2019 14:17 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/47488 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year