Renaissance Grrrl

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.

Quoth Paul Taylor:

This result is folklore, which is a technical term for a method of publication in category theory. It means that someone sketched it on the back of an envelope, mimeographed it (whatever that means) and showed it to three people in a seminar in Chicago in 1973, except that the only evidence that we have of these events is a comment that was overheard in another seminar at Columbia in 1976. Nevertheless, if some younger person is so presumptuous as to write out a proper proof and attempt to publish it, they will get shot down in flames.

This is a followup to a recent post on Parameterized Monads which I discovered independently, along with everyone else :)

For anyone interested in reading more about them, Oleg Kiselyov also discovered them independently, and developed some Haskell supporting code. Coq supporting code by Matthieu Sozeau is also available. And apparently Robert Atkey investigated them thoroughly in 2006.

If people are interested in more Coq support, I've been working on a Coq library for basic monadic coding in a desperate attempt to make programming (rather than theorem proving) viable in Coq. Eventually I'll post a link to the library which will include parameterized monads as well as traditional monads, applicative functors, and other basic category theoretic goodies. This library along with the Vecs library I never announced stemmed from work last term on proving compiler correctness for a dependently typed language. Hopefully there'll be more news about that this fall.

I've been thinking recently about the free monoid, in particular about why it is what it is. Before you run off in fear of the terminology, read on. The rest of this post is in English, a rare thing for discussions of fundamentals of mathematics. It's that rareness which led me to muse on what all that abstract nonsense actually means.

For those who don't know what a monoid is, it's a triple <S, ⋅, ε> where S is a set, ⋅ is a binary operation over that set which is associative (i.e. (x ⋅ y) ⋅ z == x ⋅ (y ⋅ z)), and ε is the left and right identity of ⋅ (i.e. x ⋅ ε == x == ε ⋅ x). These kinds of functions are incredibly common. Semirings, which are also incredibly common, each have two. For example: addition with 0 and multiplication with 1 over the natural numbers; disjunction with False and conjunction with True over the booleans; union with the empty set and intersection with the universal set over the subsets of some universal set. Given how common they are, sometimes we'd like to construct an arbitrary one for as cheaply as possible, for free.

( Read more... )