The idea that without lambda encodings, the current state of the art forces you to commit to a class of datatypes in the design of your type theory.

A lambda encoding is some way of representing data as functions (lambda abstractions).  Some motivations for this for computer-checked proofs and type theory.

Curry-style typing and realizability make it sensible to allow a top type to type every term, even non-normalizing ones.

Intersection types internalize the idea that a term has two types.  Curry-style typing is generally needed for this to be nontrivial.

In Curry-style typing annotations -- for example, the types of bound variables -- are erased, and not truly (semantically) part of the term.  In Church-style, they are intrinsic to the term and are truly there.  Discussion of some of the practicalities of Curry-style typing, in particular type annotations versus proving typings.

Types are specifications whose semantics is explained in terms of computation, which is thus conceptually prior.  Realizability is a way of explaining the semantics of types.

In which I argue that type information should be erased from programs by the compiler both for final execution and also for reasoning (in a language with dependent types, for example, where we can reason about program execution statically).

GADTs are quite powerful.  Why go all the way to true dependent types?  And should you use the Curry-Howard isomorphism (see Chapter 3 of the podcast) or not?

This episode reviews some of the applications of GADTs we have discussed so far, and discusses an example where we want to write a function that consumes a number of inputs that is controlled by an argument to the function.  

One use case for GADTs (as a special case of dependent types) is to form a typed subset of your host language.  One creates an EDSL called Expr a, where a is a type of the language (say this language is Haskell).  Values of types Expr a are the abstract syntax trees of expressions of type a from your host language.  This is just a special case of embedding a typed language into your host language: in this case the typed language is a subset of your host language.