Iowa Type Theory Commute

10 Episodes
Subscribe

By: Aaron Stump

Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.

Some advanced examples in DCS
#19
09/25/2023

This episode presents two somewhat more advanced examples in DCS.  They are Harper's continuation-based regular-expression matcher, and Bird's quickmin, which finds the least natural number not in a given list of distinct natural numbers, in linear time.  I explain these examples in detail and then discuss how they are implemented in DCS, which ensures that they are terminating on all inputs.


DCS compared to termination checkers for type theories
#18
09/19/2023

In this episode, I continue introducing DCS by comparing it to termination checkers in constructive type theories like Coq, Agda, and Lean.  I warmly invite ITTC listeners to experiment with the tool themselves.  The repo is here. 


Getting started with DCS
#17
09/10/2023

In this episode, I talk more about the DCS tool, and invite listeners to check it out and possibly contribute!  The repo is here.


Introduction to DCS
#16
09/04/2023

DCS is a new functional programming language I am designing and implementing with Stefan Monnier.  DCS has a pure, terminating core, around which monads will be layered for possibly diverging, impure computation.  In this episode, I talk about this basic design, and its rationale.  


Semantics of subtyping
#15
07/24/2023

I answer a listener's question about the semantics of subtyping, by discussing two different semantics: coercive subtyping and subsumptive subtyping.  The terminology I found in this paper by Zhaohui Luo; see Section 4 of the paper for a comparison of the two kinds of subtyping.  With coercive subtyping, we have subtyping axioms "A


More on type inference for simple subtypes
#14
07/16/2023

I continue the discussion of Mitchell's paper Type Inference with Simple Subtypes.  Coming soon: a discussion of semantics of subtyping.


Subtyping, the golden key
#13
07/09/2023

In this episode, I wax rhapsodic for the potential of subtyping to improve the practice of pure functional programming, in particular by allowing functional programmers to drop various irritating function calls that are needed just to make types work out.  Examples are lifting functions with monad transformers, or even just the pure/return functions for applicative functors/monads.


Type inference with simple subtypes
#12
06/30/2023

In this episode, I begin discussing a paper titled "Type Inference with Simple Subtypes," by John C. Mitchell.  The paper presents algorithms for computing a type and set of subtype constraints for any term of the pure lambda calculus.  I mostly focus here on how subtype constraints allow typing any term (which seems surprising).


Basics of subtyping
#11
06/21/2023

In this episode, I discuss a few of the basics for what we expect from a subtyping relation on types: reflexivity, transitivity, and the variances for arrow types.


Begin chapter on subtyping
#10
06/21/2023

We begin a discussion of subtyping in functional programming.  In this episode, I talk about how subtyping is a neglected feature in implemented functional programming languages (for example, not found in Haskell), and how it could be very useful for writing lighter, more elegant code.  I also talk about how subtyping could help realize a new vision for practical strong functional programming, where the language has a pure, terminating core language, then a monad for pure but possibly diverging computation, and finally a monad for impurity and divergence.