Iowa Type Theory Commute

In a 2013 journal article titled "A Scalable Module System", Florian Rabe and Michael Kohlhase propose a module system called MMT (Modules for Mathematical Theories) for structuring mathematical knowledge.  The paper has a very interesting general discussion of module systems, from programming languages but also other areas like algebraic specification and theorem proving.  The system is based on a rather small set of concepts which subsume those of, for example, Standard ML's module system.  Thought-provoking!

I look back at the module systems we considered so far (Haskell's, Standard ML's, and Agda's), and consider a few points that are on my mind about these.  I also mention a few other languages' module systems (Clojure, Java 9).  I also ponder names and namespace management.

Agda's module system (beautifully described here) could be seen as intermediate between Haskell's and Standard ML's.  It supports nested parametrized modules with information hiding, but does not go all the way to higher-order functors (as in Standard ML).

SML has arguably the most complicated/powerful module system of any existing programming language.  It is a luxury RV to Haskell's camper van.  I take a high-level look, following a very nice paper by Xavier Leroy, titled "A modular module system".

I briefly survey the main features of Haskell's module system, and reflect a bit on its design.

I start Chapter 13 (in Season 2) of the podcast, on module systems.  Almost all programming languages I know include some kind of scheme for modules, packages, namespaces, or something like this.  I discuss the high-level ideas of namespace management and type abstraction, two main use cases for module systems.  Subsequent episodes will discuss module systems (from papers or documentation) of various languages.

I was reading Benjamin Pierce's dissertation, and learning some intriguing things about intersection types in the context of Church-style typing.  I summarize the parts of this I comprehended so far.

I discuss the perhaps surprising fact that union and intersection types are quite actively used and promoted for languages like TypeScript, also OO languages like Scala.  I also try to explain briefly a counterexample to type preservation with union types, which you can find at the start of Section 2 of Barbanera and Dezani-Ciancaglini's paper "Intersection and Union Types: Syntax and Semantics", where it is attributed to Benjamin Pierce.

I sketch the argument that pure lambda terms in normal form are typable using intersection types.  This completes the argument started in the previous episode, that intersection types are complete for normalizing terms: normal forms are typable, and typing is preserved by beta-expansion.  Hence any normalizing term is typable (since it reduces to a normal form by definition, and from this normal form we can walk typing back to the term).

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

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.

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.

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.

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

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.