Iowa Type Theory Commute

Where relational semantics for parametric polymorphism often includes a lemma called Identity Extension (discussed in Episode 10, on the paper "Types, Abstraction, and Parametric Polymorphism"), RelTT instead has a refinement of this called Identity Inclusion.  Instead of saying that the interpretation of every closed type is the identity relation (Identity Extension), the Identity Inclu...

I give a brief glimpse at Phil Wadler's important paper "The Girard-Reynolds Isomorphism", which is quite relevant for Relational Type Theory as it shows that relational semantics for the usual type for Church-encoded natural numbers implies induction.  RelTT uses a generalization of these ideas to derive induction for any positive type family.

I talk through a proof I just completed that the type of relationally inductive naturals and the type of parametric naturals are equivalent.  This is similar to proofs one can find in a paper of Philip Wadler's titled "The Girard-Reynolds Isomorphism", which I plan to discuss in the next episode.

I discuss how to define internalized relational typings, implicit products, and two forms of natural number types, in RelTT.

In this episode, I discuss the semantics of the proposed six type constructors of RelTT.

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.

This episode continues the introduction of RelTT by presenting the types of the language.  Because the system is based on binary relational semantics, we can include binary relational operators like composition and converse as type constructs!  Strange.  The language also promotes terms to relations, by viewing them as functions and then taking their graphs as the relational meaning.

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

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. 

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

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

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

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

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

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.

Start of Chapter 10, on logical relations and parametricity.  Basic idea of logical relation as the relational generalization of the algebraic idea of homomorphism.  This is also the start of Season 2, as the fall academic year is just beginning here in Iowa.

The simplified version of Lamping's algorithm for optimal beta-reduction is discussed.  We have duplicators which eat their way through lambda graphs.  When copying a lambda abstraction, we send one duplicator down the variable port, and another down the body port.  When they meet, they cancel each other and the duplication is done.  But duplication can get paused waiting for a value to come...

I discuss some examples posted on my blog, QA9, which show that executables produced by ghc (the main implementation of Haskell) can exhibit non-optimal beta-reduction.  Thanks to Victor Maia for major help with these.

In this episode I talk about how to represent lambda terms as graphs with duplicator nodes for splitting edges corresponding to bound variables.  I also start discussing the beginning of Lampings' abstract algorithm for optimal beta-reduction, in particular how we need to push duplicators inside lambda abstractions to initiate a lazy duplication.

We discussed last time how with a graph-sharing implementation of untyped lambda calculus, it can happen that you are forced to break sharing and copy a lambda abstraction.  We discuss in this episode the central issue with doing that, namely copying redexes and copying applications which could turn into redexes following other beta reductions.  The high-level idea of the proposed solution is also...

Some background on optimal beta reduction: Levy, Lamping.  The main problem to overcome is duplicating a lambda abstraction that is used in two different places in your term.  The solution is to try to duplicate it incrementally.

Many termination checkers support lexicographic (structural) recursion.  The lexicographic combination of orderings on sets A and B is an ordering on A x B where a pair decreases if the A component does (and then the B component can increase unboundedly) or else the A component stays the same and the B component decreases.  Connections with nested recursion and ordinals discussed.

Well-founded recursion is a technique to turn recursion which decreases along a well-founded ordering into a structural recursion.

Another type-based approach to termination-checking for recursive functions over inductive datatypes is to use so-called Mendler-style iteration.  On this approach, we write recursive functions by coding against a certain interface that features an abstract type R, which abstracts the datatype over which we are recursing; and a function from R to the result type of the recursion.  Subdata of the i...