Foundations for structured programming with GADTs
Johann, Patricia and Ghani, Neil (2008) Foundations for structured programming with GADTs. In: Proceedings of the 35th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL 2008. ACM Press, pp. 297308. ISBN 9781595936899

PDF
ghani_popl08.pdf  Draft Version Download (333kB)  Preview 
Abstract
GADTs are at the cutting edge of functional programming and become more widely used every day. Nevertheless, the semantic foundations underlying GADTs are not well understood. In this paper we solve this problem by showing that the standard theory of data types as carriers of initial algebras of functors can be extended from algebraic and nested data types to GADTs. We then use this observation to derive an initial algebra semantics for GADTs, thus ensuring that all of the accumulated knowledge about initial algebras can be brought to bear on them. Next, we use our initial algebra semantics for GADTs to derive expressive and principled tools — analogous to the wellknown and widelyused ones for algebraic and nested data types — for reasoning about, programming with, and improving the performance of programs involving, GADTs; we christen such a collection of tools for a GADT an initial algebra package. Along the way, we give a constructive demonstration that every GADT can be reduced to one which uses only the equality GADT and existential quantification. Although other such reductions exist in the literature, ours is entirely local, is independent of any particular syntactic presentation of GADTs, and can be implemented in the host language, rather than existing solely as a metatheoretical artifact. The main technical ideas underlying our approach are (i) to modify the notion of a higherorder functor so that GADTs can be seen as carriers of initial algebras of higherorder functors, and (ii) to use left Kan extensions to trade arbitrary GADTs for simplerbutequivalent ones for which initial algebra semantics can be derived
Item type:  Book Section 

ID code:  33726 
Keywords:  software engineering, programming language, data types, GADTs, Electronic computers. Computer science, Electronic information resources, Computer Science (miscellaneous) 
Subjects:  Science > Mathematics > Electronic computers. Computer science Bibliography. Library Science. Information Resources > Information resources > Electronic information resources 
Department:  Faculty of Science > Computer and Information Sciences 
Depositing user:  Pure Administrator 
Date Deposited:  20 Oct 2011 15:42 
Last modified:  08 May 2016 17:48 
URI:  http://strathprints.strath.ac.uk/id/eprint/33726 