This episode begins Chapter 11 of the podcast, on Relational Type Theory.  This is a new approach to type theory that I am developing.  The idea is to design a type system based on the binary relational semantics for types, which we considered in Chapter 10.  This episode recalls some of that semantics.

In this episode I discuss one of the greatest papers in the history of Programming Language's research, namely "Types, Abstraction, and Parametric Polymorphism" by the great John C. Reynolds.  I summarize the two interconnected semantics for polymorphic types proposed by Reynolds: one which interprets types as sets and programs as members of those sets, and another which interprets types as relations on the sets from the first interpretation.  Listen and you will get to hear my aha moment as I understand live on air what the Identity Extension Lemma really means.   See also this blog post on the same topic.

Today I discuss the construction of relational models of typed lambda calculus (say, System F), that support the idea of representation independence.  This is a feature of a type theory where different implementations of the same interface can be proved equivalent, and used interchangeably in the theory.  Only in the past couple years have researchers proposed theories like this, but the semantic ideas underlying such theories have been around since Reynolds's seminal paper "Types, Abstraction, and Parametric Polymorphism".

I continue discussing the approach to HOAS from my paper "A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille", 2019, available from my web page. 

I start explaining an idea from my paper "A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille", 2019, available from my web page.  The goal is to encode a datatype (including its constructors, which we saw were troublesome for higher-order signatures generally in the previous episode) for application-free lambda terms, which I submit is the simplest higher-order datatype possible.  I just explain some of the setup, and will attempt wading through the details next time.

I discuss the problem of term models for higher-order signatures, following a prelude about the Edinburgh Logical Framework (LF) and higher-order datatypes.

Discussion of definitions in "Pre-logical relations" by Honsell and Sannella, particularly the notion of a lambda applicative structure (similar to a definition in John C. Mitchell's book "Foundations for Programming Languages').  In short, lambda abstractions get interpreted in combinatory algebras by compiling away the lambda abstractions in favor of S and K combinators, which are then interpreted by the combinatory algebra.  I complain about the fact that the definition of a lambda applicative structure is required to come with an interpretation function for terms (hence tying the semantics to the syntax).

Also known as the Fundamental Property, this is a theorem stating that for every well-typed term t : T, and every logical relation R between algebraic structures A and B, the meaning of t in A is related by R to the meaning of t in B.  I view it as a straightforward semantic soundness property, but where the semantics of types is this somewhat interesting one that interprets types as binary relations on structures A and B.  I muse on these matters a bit in the episode.

In this episode, I talk through a small (but intricate) example from a paper titled "Pre-logical relations" by Honsell and Sannella, showing that the set of logical relations is not closed under composition.  That is, you can have a logical relation between structure A and structure B, and one between B and C, but the composition (while a relation) is not a logical relation between A and C.  This took me three takes to get to where I wasn't tripping over my tongue, so enjoy.

Logical relations are the relational generalization of the algebraic concept of a homomorphism -- but they go further in extending the notion of structure-preservation to higher-order structures.  We discuss the basic definition in this episode.