Home » forums » LtU Forum

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.
Thanks in advance,
- Anthony

By guerrilla_thought at 2010-08-31 15:52 | LtU Forum | previous forum topic | next forum topic | other blogs | 5969 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

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.

By neelk at Wed, 2010-09-01 06:10 | login or register to post comments