Please use this identifier to cite or link to this item:
Title: A systematic translation of guarded recursive data types to existential types
Authors: WANG MENG
Keywords: type systems, type-directed translation, proof-term construction, constraint solving
Issue Date: 15-Sep-2005
Citation: WANG MENG (2005-09-15). A systematic translation of guarded recursive data types to existential types. ScholarBank@NUS Repository.
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.
Appears in Collections:Master's Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
parallel.pdf377.54 kBAdobe PDF



Google ScholarTM


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.