Iowa Type Theory Commute

Latest Episodes:

Intersection Types Preserved Under Beta-Expansion Feb 15, 2021

Show notes

Type systems usually have the type preservation property: if a typable term beta-reduces, then the resulting term is still typable. So typing is closed under beta-reduction. With intersection typing, typing is also closed under beta-expansion, which is a critical step in showing that intersection typing is complete for normalizing terms: any normalizing term can be typed with intersection types (and simple function types).

Introduction to Intersection Types Feb 08, 2021

Show notes

In a type system with intersection types, a term t that has type A and also has type B can be assigned the type 'A intersect B'. This episode begins Chapter 12 of the podcast on intersection types.

Deriving disjointness of constructor ranges in RelTT Feb 02, 2021

Show notes

Responding to an email question from a listener, I explain how to derive a form of inconsistency from the assumption that True is related to False at type Bool.

Software Design and Intrinsic Identity Jan 20, 2021

Show notes

I muse about the hopeless prospect of a single intrinsic conceptual decomposition of a problem domain in software engineering, and relate this to the idea of intrinsic identity we discussed recently for Relational Type Theory.

Identity Inclusion in Relational Type Theory Jan 18, 2021

Show notes

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 Inclusion lemma identifies certain types whose relational meaning is included in the identity relation, and certain types which include the identity relation. So there are two subset relations, going in opposite directions. The two classes of types are first, the ones where all quantifiers occur only positively, and second, where they occur only negatively. Using Identity Inclusion, we can derive transitivity for forall-positive types, which is needed to derive induction following the natural generalization of the scheme in Wadler's paper (last episode).

On the paper "The Girard-Reynolds Isomorphism" by Philip Wadler Jan 18, 2021

Show notes

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.

Equivalence of inductive and parametric naturals in RelTT Dec 28, 2020

Show notes

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.

Examples in Relational Type Theory Dec 23, 2020

Show notes

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

The Semantics of Relational Types Dec 22, 2020

Show notes

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

The Types of Relational Type Theory Dec 14, 2020

Show notes

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.

Our TOPPODCAST Picks

Follow Us

Stay Connected

Related Podcasts

Links

Stay Connected

Our TOPPODCAST Picks

Follow Us

Stay Connected

Iowa Type Theory Commute

Related Podcasts

1

2

3

4

5

6