Iowa Type Theory Commute Aaron Stump
-
- Technologie
Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
-
Some advanced examples in DCS
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
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
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
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
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 : B by c", where c is a function from A to B. The idea is that the compiler should automatically insert calls to c whenever an expression of type A needs to be converted to one of type B. Subsumptive subtyping says that A : B means that the meaning of A is a subset of the meaning of B. So this kind of subtyping depends on a semantics for types. A simple choice is to interpret a type A as (as least roughly) the set of its inhabitants. So a type like Integer might be interpreted as the set of all integers, etc. Luo argues that subsumptive subtyping does not work for Martin-Loef type theory, where type annotations are inherent parts of terms. For in that situation, A : B does not imply List A : List B, because Nil A is an inhabitant of List A but not of List B (which requires instead Nil B).
Join the telegram group here. -
More on type inference for simple subtypes
I continue the discussion of Mitchell's paper Type Inference with Simple Subtypes. Coming soon: a discussion of semantics of subtyping.