We review the metatheoretic property of type safety, decomposed into two properties called type preservation and progress.  Discussion of progress in the context of type theory, where adding axioms can lead to a failure of progress.

Type safety is a basic property of both statically typed programming languages and type theories.  It has traditionally (past few decades) been decomposed into type preservation and progress.  Type preservation says that if a program expression e has some type T, then running e a bit will give a result that still has type T (and type preservation would apply again to that result, to preserve the type T indefinitely along the execution of e).  Progress says that well-typed expressions cannot get stuck computationally: they cannot reduce to a form where the operational semantics is then undefined.  This is how we model the idea that the type system is preventing certain kinds of failures: make those failures correspond to undefined behavior.  

Metatheory is concerned with proving properties about theories, in this case type theories or programming languages.  

We consider using Mendler's technique of abstracting out problematic types with new type variables, and how this can yield a lambda encoding where the programmer is in charge of when to make recursive calls (rather than in the Church encoding, where the data present the programmer's combining function with the results of all possible recursive calls on immediate subdata).

The Church encoding allows definition of certain recursive functions, but all the recursive calls are implicit.  The encoding simply presents you with the results of recursion for all immediate subdata.  Using a technique due to Mendler, an encoding is possible where recursions are explicitly made by the combining functions given to the data.

In this episode we briefly review the Church and Parigot encodings (discussed previously in Chapter 6 of this podcast) and then consider the Scott encoding, where combining functions receive only the immediate subdata of the data.

The Parigot encoding has exponential-size normal forms: but don't panic!  With a decent graph-sharing implementation of lambda calculus, they take linear space in memory.

The Parigot encoding solves the Church encoding's problem of inefficient predecessor.  It can be typed using positive-recursive types, which preserve normalization of the type theory.

What is fold-right for a natural number?  How do we define addition with this?  The problem of inefficient predecessor.

We consider fold-right for lists, and its static type.  The Church encoding for lists makes them into their own fold-right functions