A systematic translation of guarded recursive data types to existential types

Abstract

Guarded recursive data types (GRDTs) are a new language feature which allows to type check the different branches of case expressions under different type assumptions.We show that GRDTs can be translated to type classes with existential types (TCET).The translation to TCET might be problematic in the sense that common implementations such as the Glasgow Haskell Compiler (GHC) fail to accept the translated program. We provide for a refined translation from TCET to existential types (ET) based on a novel proof term construction method. The resulting ET program is accepted by GHC. Our work can be seen as the first formal investigation to relate the concepts of guarded recursive data types and (type classes with) existential types.