### An introduction to recursive types

2 Apr 2015 04:04 pmThe 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.

- Benjamin C. Pierce (2002)
- 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.

- Hagen Huwig and Axel Poigné (1990)
- 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.

- Alfred Tarski (1955)
- 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.

- Benjamin C. Pierce (1991)
- 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.

- Jiří Adámek, Horst Herrlich, and George Strecker (1990)
- 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

- Oleg Kiselyov (2012)
- 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

- Herman Geuvers (1992)
- 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.

- Morten H. Sørensen and Paweł Urzyczyn (2006)
- 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.

- Roel de Vrijer (1987)
- 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

- Jan Martin Jansen, Pieter Koopman, and Rinus Plasmeijer (200X)
- 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.

- Aaron Stump (2009)
- Parigot encodings
- M. Parigot (1988)
*Programming with proofs: A second-order type theory.*ESOP, LNCS 300, pp.145–159. Springer.

- M. Parigot (1988)
- 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

- Varmo Vene and Tarmo Uustalu (1998)
- 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

- Andy Gill, John Launchbury, and Simon Peyton Jones (1993)
- For another general introduction along the lines of what we covered in class
- Philip Wadler (1990)
*Recursive types for free!*

- Philip Wadler (1990)
- "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.

- Morten H. Sørensen and Paweł Urzyczyn (2006)
- 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.