Iowa Type Theory Commute

Sequent calculus is a different style in which proof systems can be formulated, where for each connective, we have a left rule for introducing it (in the conclusion of the rule) in the left part of a sequent G => D (i.e., in G), and similarly a right rule for introducing it in the right part (D).  The beauty of sequent calculus is disjunction is handled without any departure from the general fo...

We discuss further inferences in natural deduction, in particular implication introduction and elimination.

We discuss the problem of the or-elimination rule in natural deduction, which does not have the correct form for natural deduction inferences.  It is a research problem to fix this! Don't forget to get in touch with me if you want to do the mini-course over Zoom next month, on normalization.  

This episode begins the discussion of the style of proof known as Natural Deduction, invented by Gerhard Gentzen, a student of Hermann Weyl, himself a student of David Hilbert (sorry, I said incorrectly that Gentzen was Hilbert's own student).  Each logical connective (like OR, AND, IMPLIES, etc.) has introduction rules that let you prove formulas built with that connective; and elimination r...

We continue our gradual entry into proof theory by talking about reflecting meta-logical reasoning into logical rules, and naming the three basic proof systems (Hilbert-style, natural deduction, and sequent calculus). Advertising for the October 3-session Zoom mini-course on normalization continues.  Email me if you are interested!  This is just for ITTC listeners. Finally, if you like the podcast...

I highlight two basic points in this continuing warm-up to proof theory: there are different proof systems for the same logics, and it is customary to separate purely logical rules (dealing with propositional connectives and quantifiers, for example) from rules or axioms for some particular domain (like axioms about arithmetic, or whatever domain is of interest).

This is the start of Season 3 of the podcast.  We are beginning with a new chapter (Chapter 14) on Proof Theory.   This episode gives some basic introduction to the history and broad concerns of proof theory.  There is even music, composed and played by yours truly, chez nous...

In this episode I discuss the paper "Modula-2 and Oberon" by Niklaus Wirth.  Modula-2 introduced (it seems from the paper) the idea of having modules with explicit import and import lists -- something we saw at the start of our look at module systems with Haskell's module system.  I note some interesting historical points raised by the paper.

Analogously to the decomposition of a datatype into a functor (which can be built from other functors to assemble a bigger language from smaller pieces of languages) and a single expression datatype with a sole constructor that builds an Expr from an F Expr (where F is the functor) -- analogously, a recursion can be decomposed into algebras and a fold function that applies the algebra throughout t...

Last episode we discussed how functors can describe a single level of a datatype.  In this episode, we discuss how to put these functors back together into a datatype, using disjoint unions of functors and a fixed-point datatype.  The latter expresses the idea that inductive data is built in any finite number of layers, where each layer is described by the functor for the datatype.

This episode continues the discussion of Swierstra's paper "Datatypes à la Carte", explaining how we can decompose a datatype into the application of a fixed-point type constructor and then a functor.  The functor itself can be assembled from other functors for pieces of the datatype.  This makes modular datatypes possible.

In a really wonderful paper of some few years back, Swierstra introduced the idea of modular datatypes using ideas from universal algebra.  Modular datatypes allow one to assemble a bigger datatype from component datatypes, and combine functions written on the component datatypes in a modular way.   In this episode I introduce the paper and the problem (dubbed the expression problem by Phil Wadler...

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

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

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

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

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

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.