Translating Generalized Algebraic Data Types to System F

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.