Iowa Type Theory Commute

Discussion of a compositional method of termination checking using so-called sized types.  Datatypes are indexed by sizes, and recursive calls can only be made on data of strictly smaller size than the data as input to the recursion.  Since the method is type-based, it is compositional: we can break out helper functions from a recursive function and not upset the termination checker.  A readable a...

Review of need for termination analysis for recursive functions on inductive datatypes.  Discussion of a serious problem with syntactic termination checks, namely noncompositionality.  A function may pass the syntactic termination check, but abstracting part of it out into a helper function may result in code which no longer passes the check.  So we need a compositional termination check, which wi...

Start of Chapter 8 of the podcast, on termination checking in type theory, and strong functional programming.  Discussion of a little history of adding datatypes to the original pure type theory of Coq (called the Calculus of Constructions).  Considering the most basic form of termination checking, which is checking syntactically that recursive calls are only made on subdata of the data input to t...

Discussion of the basic idea of the Tait--Martin-Loef proof of confluence for untyped lambda calculus.  Let me know any requests for what to discuss in Chapter 8!

Start of discussion on how to prove confluence for untyped lambda calculus.  Also some discussion about the research community interested in confluence.

The basic property of confluence of a nondeterministic reduction semantics: if from starting term t you can reach t1 and also t2 (by two finite reduction sequences), then there is some t3 to which t1 and t2 both reduce in a finite number of steps.  The use of confluence for ensuring completeness of the conversion-checking algorithm that tests conversion of t1 and t2 by normalizing both terms and c...

Discussion of the connection between normalization and logical consistency.  One approach is to prove normalization and type preservation, to show (in proof-theoretic terms) that all detours can be eliminated from proofs (this is normalization) and that the resulting proof still proves the same theorem (this is type preservation).  I mention an alternative I use for Cedille, which is to use a real...

Normalization (every term reaches a normal form via some reduction sequence) is needed essentially in type theory due to the Curry-Howard isomorphism: diverging programs become unsound proofs.  Traditionally, type theorists have also desired normalization or even termination (every term reaches a normal form no matter what reduction sequence is explored in a nondeterministic operational semantics)...

Discussion of normalization (there is some way to reach a normal form) versus termination (no matter how you execute the term you reach a normal form).  A little more discussion of strong FP.  For type theory, the need for normalization due to Curry-Howard and due to conversion checking.

Type safety proofs are big confirmations requiring consideration of all your operational and typing rules.  So they rarely contain much deep insight, but are needed to confirm your language's type system is correct.  Looking ahead, this episode also talks about the different between normalization and termination when your language is nondeterministic, and the property of confluence. 

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 t...

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

The Church encoding represents data as their own fold-right functions.  For booleans, this means they become their own if-then-else expressions.  We consider the polymorphic type for these, which is forall X. X -> X -> X.

The Church encoding represents data as their own fold-right functions

Functional encodings take programming language features like pattern-matching and recursion and move them from outside of data to inside of data.

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.