Iowa Type Theory Commute

Latest Episodes:

Modular datatypes: introducing Swierstra's paper "Datatypes à la Carte" Jun 24, 2021

Show notes

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) it is trying to solve. Modular datatypes are a different form of modularity that I would like to consider in the context of the discussion of module systems we have been engaged in now for a while in Chapter 13 of the podcast.

Modules for Mathematical Theories (MMT) Jun 08, 2021

Show notes

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!

Some thoughts on module systems so far May 18, 2021

Show notes

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.

A look at Agda's module system May 12, 2021

Show notes

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

Standard ML: the Newmar King-Aire of module systems May 10, 2021

Show notes

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

A look at Haskell's module system Apr 26, 2021

Show notes

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

Let's talk about modules! Apr 20, 2021

Show notes

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.

Church-style Typing and Intersection Types: Glimpses of Benjamin Pierce's Dissertation Apr 12, 2021

Show notes

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.

Intersections and Unions in Practice; Failure of Type Preservation with Unions Mar 22, 2021

Show notes

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.

Normal terms are typable with intersection types Mar 05, 2021

Show notes

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

Our TOPPODCAST Picks

Follow Us

Stay Connected

Related Podcasts

Links

Stay Connected