Foundations for structured programming with GADTs

ABSTRACT

GADTs are at the cutting edge of functional programming and becomemore 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 derivean 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 well-known and widely-used 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 higher-order functor so that GADTs can be seen as carriers of initial algebras of higher-order functors, and (ii) to use left Kan extensions to trade arbitrary GADTs for simpler-but-equivalent ones for which initial algebra semantics can bederived.

REFERENCES

• 1: E. S. Bainbridge , P. J. Freyd , A. Scedrov , P. J. Scott, Functorial polymorphism, Theoretical Computer Science, v.70 n.1, p.35-64, Jan. 1990 [doi>10.1016/0304-3975(90)90151-7]
• 2: I. Bayley. Generic Operations on Nested Datatypes. Ph.D. Dissertation, Univ. of Oxford, 2001. At http://web.comlab.ox.ac.uk/oucl/research/areas/ap/papers/bayley-thesis.pdf
• 3: P. Blampied. Structured Recursion for Non-uniform Data-types. Ph.D. Dissertation, Univ. of Nottingham, 2000. At http://www.cs.nott.ac.uk/Research/fop/blampied-thesis.pdf
• 4: Richard S. Bird , Lambert G. L. T. Meertens, Nested Datatypes, Proceedings of the Mathematics of Program Construction, p.52-67, June 15-17, 1998
• 5: Richard S. Bird , Ross Paterson, de Bruijn notation as a nested datatype, Journal of Functional Programming, v.9 n.1, p.77-91, January 1999 [doi>10.1017/S0956796899003366]
• 6: R. Bird and R. Paterson. Generalised folds for nested datatypes. Formal Aspects of Computing 11(2) (1999), pp. 200--222.
• 7: J. Cheney and R. Hinze. First-class phantom types. At http://www.informatik.uni-bonn.de/~ralf/publications/Phantom.pdf
• 8: P. Dybjer. Inductive Families. Formal Aspects of Computing 6(4), pp. 440--465, 1994.
• 9: Andrew Gill , John Launchbury , Simon L. Peyton Jones, A short cut to deforestation, Proceedings of the conference on Functional programming languages and computer architecture, p.223-232, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165214]
• 10: Neil Ghani , Patricia Johann , Tarmo Uustalu , Varmo Vene, Monadic augment and generalised short cut fusion, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 11: N. Ghani, T. Uustalu, and V. Vene. Build, augment and destroy. Universally. Proceedings, Asian Symposium on Programming Languages, pp. 327--347, 2003.
• 12: P. Johann and N. Ghani. Initial algebra semantics is enough! Proceedings, Typed Lambda Calculus and Applications, pp. 207--222, 2007.
• 13: P. Johann and N. Ghani. Programming with Nested Types. Submitted, 2007.
• 14: Patricia Johann, A Generalization of Short-Cut Fusion and its Correctness Proof, Higher-Order and Symbolic Computation, v.15 n.4, p.273-300, December 2002 [doi>10.1023/A:1022982420888]
• 15: MacLane, S. Categories for the Working Mathematician. Springer-Verlag, 1971.
• 16: Clare Martin , Jeremy Gibbons , Ian Bayley, Disciplined, efficient, generalised folds for nested datatypes, Formal Aspects of Computing, v.16 n.1, p.19-35, April 2004 [doi>10.1007/s00165-003-0013-6]
• 17: C. McBride. Epigram: Practical programming with dependent types. Proceedings, 5th International Summer School on Advanced Functional Programming, 2004. At http://www.e-pig.org/downloads/epigram-notes.pdf
• 18: The Omega Download Page. http://web.cecs.pdx.edu/~sheard/Omega/index.html
• 19: Frank Pfenning , Christine Paulin-Mohring, Inductively Defined Types in the Calculus of Constructions, Proceedings of the 5th International Conference on Mathematical Foundations of Programming Semantics, p.209-228, March 29-April 01, 1989
• 20: T. Sheard, J. Hook, and N Linger. GADTs + extensible kinds = dependent programming. At http://www.cs.pdx.edu/~sheard/papers/GADT+ExtKinds.ps
• 21: T. Sheard and E. Pasalic. Meta-programming with built-in type equality. Proceedings, Logical Frameworks and Meta-languages, 2004. At http://homepage.mac.com/pasalic/p2/papers/LFM04.pdf
• 22: M. Sulzmann and M. Wang. A systematic translation of guarded recursive data types to existential types. At http://www.comp.nus.edu.sg/~sulzmann/research/ms.html
• 23: M. Sulzmann and M. Wang. Translating generalized algebraic data types to System F. Manuscript, 2005. At http://www.comp.nus.edu.sg/~sulzmann/manuscript/simple-translate-gadts.ps
• 24: Josef Svenningsson, Shortcut fusion for accumulating parameters & zip-like functions, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.124-132, October 04-06, 2002, Pittsburgh, PA, USA
• 25: Akihiko Takano , Erik Meijer, Shortcut deforestation in calculational form, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.306-313, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224221]
• 26: Hongwei Xi , Chiyan Chen , Gang Chen, Guarded recursive datatype constructors, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.224-235, January 15-17, 2003, New Orleans, Louisiana, USA
• 27: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

General Terms:
Languages, Theory

Keywords:
GADTs, initial algebra semantics, program fusion