Why Not Lambda Encodings?

A short note on lambda encodings for proof assistants. I got this question a few days ago:

Why don’t we use Church encodings or otherwise to represent inductive datatypes instead of these usual method that declares all the formation, introduction, and elimination rules as additional rules added to the theory?

Essentially, the problem is that you can’t get the right induction principles. Let’s take the Unit type as an example. In any proof assistant, Unit gets the following induction principle:

All is as per usual. Ordinarily with Church encodings the type is defined as the recursion principle, so let’s just generalize that to the induction principle. From that the definition seems extremely simple.

Now we can clearly see the problem – the type is defined negatively in terms of itself! Remember that with the usual inductive types we see in proof assistants, we have the positivity restriction, which means recursive occurances of a type can only appear in positive positions, without which we can easily prove False. Thus this “obvious” way of doing lambda encodings in type theory unfortunately isn’t sound.

However, there is hope! Aaron Stump has done lots of work on designing a type theory in which lambda encodings can be soundly implemented. I haven’t had time to keep up with that line of work, but you can check out this slide deck for an introduction: Slide deck.

Anyway, you might be wondering why strict positivity is necessary, since it’s understandably unintuitive for most. I’ll write up a note on that sometime soon and link it here.