## Examples of encodings in Pure Type Systems

I am toying with implementing a pure type system (formally described in section 5.2 of "Lambda Calcui with Types"). I've extended the specification to include sum type introduction, formation and elimination. I've written a few examples but I'm looking for a library of example encodings in (minimal) pure type systems. In particular, I'm looking to extend the PTS as little as possible but still want to be able to translate (from a higher level language) constructs such as abstract data types and pattern matching. I read somewhere, maybe something authored by Conor McBride, that some of this is possible, but I lost that reference.
- Anthony

## Comment viewing options

### Most of these encodings are

Most of the encodings of types are typically the Church encodings of various types. For example, sums, products, natural numbers, and existential types are:

1         = ∀α. α → α
A x B     = ∀α. (A → B → α) → α
0         = ∀α. &alpha
A + B     = ∀α. (A → α) → (B → α) → α
Nat       = ∀ α. α → (α → α) → α
∃β. A(β) = ∀α. (∀β. A(β) → α) → α


If you want to elaborate pattern matching, it's a bit more complicated -- you need to define the primitive eliminations for sums and products in terms of the Church encodings, and then translate pattern matching to that. I describe how to do it in a type-theoretic style in my POPL paper from 2009, which sounds like what you want in this case.

There's a TLDI paper from this year by Andreas Rossberg, Claudio Russo, and Derek Dreyer, "F-ing modules", which shows how to elaborate ML-style module systems into uses of ordinary old F-style existentials. Again, it's a translation, and not a notational abbreviation.