An introduction to recursive types

[winterkoninkje]

The past couple weeks I've been teaching about recursive types and their encodings in B522. Here's a short annotated bibliography for followup reading:

• For a basic intro to recursive types, and for the set-theoretic metatheory: see section IV, chapters 20 and 21.
  • Benjamin C. Pierce (2002) Types and Programming Languages. MIT Press.
• The proof of logical inconsistency and non-termination is "well-known". For every type τ we can define a fixed-point combinator and use that to exhibit an inhabitant of the type:
  • fixτ = λf:(τ→τ). let e = λx:(μα.α→τ). f (x (unroll x)) in e (roll(μα.α→τ) e)
  • ⊥τ = fixτ (λx:τ. x)
• A category-theoretic proof that having fixed-points causes inconsistency
  • Hagen Huwig and Axel Poigné (1990) A note on inconsistencies caused by fixpoints in a Cartesian Closed Category. Theoretical Computer Science, 73:101–112.
• The proof of Turing-completeness is "well-known". Here's a translation from the untyped λ-calculus to STLC with fixed-points:
  • (x)* = x
  • (λx. e)* = roll(μα.α→α) (λx:(μα.α→α). e*)
  • (f e)* = unroll (f*) (e*)
• Knaster–Tarski (1955): For any monotone function, f, (a) the least fixed-point of f is the intersection of all f-closed sets, and (b) the greatest fixed-point of f is the union of all f-consistent sets.
  • Alfred Tarski (1955) A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics 5(2):285–309.
  • Bronisław Knaster (1928) Un théorème sur les fonctions d'ensembles. Annales de la Société Polonaise de Mathématique, 6:133–134.
• For a quick introduction to category theory, a good place to start is:
  • Benjamin C. Pierce (1991) Basic Category Theory for Computer Scientists. MIT Press.
• For a more thorough introduction to category theory, consider:
  • Jiří Adámek, Horst Herrlich, and George Strecker (1990) Abstract and Concrete Categories: The Joy of Cats. John Wiley and Sons.
• The Boehm–Berarducci encoding
  • Oleg Kiselyov (2012) Beyond Church encoding: Boehm–Berarducci isomorphism of algebraic data types and polymorphic lambda-terms
  • Corrado Boehm and Alessandro Berarducci (1985) Automatic Synthesis of Typed Lambda-Programs on Term Algebras. Theoretical Computer Science, v39:135–154
• Under βη-equivalence, Church/Boehm–Berarducci encodings are only weakly initial (hence, can define functions by recursion but can't prove properties by induction)
  • Herman Geuvers (1992) Inductive and Coinductive types with Iteration and Recursion. Proceedings of the 1992 Workshop on Types for Proofs and Programs, pp. 193–217
• However, using contextual equivalence, Church/Boehm–Berarducci encodings are (strongly) initial
  • Neel Krishnaswami (2009) mentions in passing [Better citation needed]
• Surjective pairing cannot be encoded in STLC (i.e., the implicational fragment of intuitionistic propositional logic): see p.155
  • Morten H. Sørensen and Paweł Urzyczyn (2006) Lectures on the Curry–Howard isomorphism. Studies in Logic and the Foundations of Mathematics, v.149.
• However, adding it is a conservative extension
  • Roel de Vrijer (1987) Surjective Pairing and Strong Normalization: Two themes in lambda calculus. dissertation, University of Amsterdam.
  • Roel de Vrijer (1989) Extending the lambda calculus with surjective pairing is conservative. 4th LICS, pp.204–215.
  • Kristian Støvring (2005) Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative. BRICS.
• Boehm–Berarducci encoded pairs is not surjective pairing: the η-rule for Boehm–Berarducci encoding of pairs cannot be derived in System F. (The instances for closed terms can be, just not the general rule.)
  • Peter Selinger mentions in passing (p.77) [Better citation needed]
• Compiling data types with Scott encodings
  • Jan Martin Jansen, Pieter Koopman, and Rinus Plasmeijer (200X) Data Types and Pattern Matching by Function Application.
  • Jan Martin Jansen, Pieter Koopman, and Rinus Plasmeijer (2006) Efficient Interpretation by Transforming Data Types and Patterns to Functions. Trends in Functional Programming.
  • Jan Martin Jansen, Rinus Plasmeijer, and Pieter Koopman (2010) Comprehensive Encoding of Data Types and Algorithms in the λ-Calculus. J. Functional Programming.
  • Pieter Koopman, Rinus Plasmeijer, and Jan Martin Jansen (2014) Church encoding of data types considered harmful for implementations. IFL submission
• For more on the difference between Scott and Mogensten–Scott encodings:
  • Aaron Stump (2009) Directly Reflective Meta-Programming. J. Higher Order and Symbolic Computation, 22(2):115–144.
• Parigot encodings
  • M. Parigot (1988) Programming with proofs: A second-order type theory. ESOP, LNCS 300, pp.145–159. Springer.
• Parigot encoding of natural numbers is not canonical (i.e., there exist terms of the correct type which do not represent numbers); though both Church/Boehm–Berarducci and Scott encoded natural numbers are.
  • Herman Geuvers (2014) mentions in passing [Better citation needed]
• For more on catamorphisms, anamorphisms, paramorphisms, and apomorphisms
  • Varmo Vene and Tarmo Uustalu (1998) Functional programming with apomorphisms (corecursion). In Proc. Estonian Acad. Sci. Phys. Math., 47:147–161
  • Erik Meijer, Maarten Fokkinga, and Ross Paterson (1991) Functional Programming with Bananas, Lenses, Envelopes, and Barbed Wire. In Proc. 5th ACM conference on Functional programming languages and computer architecture, pp.124–144
    • A translation of Squiggol into Haskell by Edward Yang.
• build/foldr list fusion
  • Andy Gill, John Launchbury, and Simon Peyton Jones (1993) A short cut to deforestation. In Proc. Functional Programming Languages and Computer Architecture, pp.223–232.
  • Many more links at the bottom of this page
• For another general introduction along the lines of what we covered in class
  • Philip Wadler (1990) Recursive types for free!
• "Iterators" vs "recursors" in Heyting arithmetic and Gödel's System T: see ch.10:
  • Morten H. Sørensen and Paweł Urzyczyn (2006) Lectures on the Curry–Howard isomorphism Studies in Logic and the Foundations of Mathematics, v.149.
• There are a great many more papers by Tarmo Uustalu, Varmo Vene, Ralf Hinze, and Jeremy Gibbons on all this stuff; just google for it.

Twitter Facebook Google+ Tumblr WordPress