\documentclass[ams,llncs,book]{tfp07symp} %include lhs2TeX.fmt %include polycode.fmt \usepackage{amsmath} \usepackage{graphicx} \usepackage{amssymb} \usepackage{polytable} \usepackage{fancyvrb} \usepackage{mainsty} \usepackage[english]{babel} \usepackage{xcolor} \begin{document} \setcounter{chapter}{4} \setcounter{page}{65} \chapter[A Leaner Specification for GADTs]{A Leaner Specification for Generalized Algebraic Data Types} \chapauthors{Arie Middelkoop\footnotemark[1]{}, Atze Dijkstra\footnotemark[1]{}, S. Doaitse Swierstra\footnotemark[1]{} \\ \textit{Category: Research}} \footnotetext[1]{Universiteit Utrecht, The Netherlands; {\tt \{ariem,atze,doaitse\}@@cs.uu.nl}} \newcommand{\Fig}[1]{Figure~\ref{#1}} \newcommand{\Sect}[1]{Section~\ref{#1}} \newcommand{\SystemF}{System $F\,$} \newcommand{\SystemFA}{System $F_A\,$} \newcommand{\SystemFAPrime}{System $F_A'\,$} \newcommand{\SystemFC}{System $F_C\,$} \newcommand{\GADT}{GADT } \newcommand{\GADTs}{GADTs } %%\newcommand{\metacomment}[1] {\begin{quote}\begin{tiny}\begin{color}{blue}\begin{itemize} #1 \end{itemize}\end{color}\end{tiny}\end{quote}} \newcommand{\metacomment}[1] {} %include format.lhs %include rules.lhs \paragraph{Abstract:} The type systems of current approaches for dealing with Generalized Algebraic Data Types (GADTs) tend to be more algorithmic than declarative in nature, and are incomplete in the sense that they deal with specific issues only. When implementing GADTs, this raises the question whether complex type system infrastructure is needed, and secondly, if all requirements were taken into account during implementation. We answer these questions by giving a declarative specification with less demands on infrastructure, and which deals with the key issues related to a GADT implementation. %include introduction.lhs %include related-work.lhs %include motivation.lhs %include typesystem.lhs %include translation.lhs %include conclusion.lhs %if False \appendix %include appendices.lhs %endif \bibliographystyle{abbrv} \bibliography{gadt-paper} \end{document}