Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/14876
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
Source: 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.
URI: http://scholarbank.nus.edu.sg/handle/10635/14876
Appears in Collections:Master's Theses (Open)

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

OPEN

NoneView/Download

Page view(s)

196
checked on Jan 19, 2018

Download(s)

150
checked on Jan 19, 2018

Google ScholarTM

Check


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