Iowa Type Theory Commute

Latest Episodes:

GADTs for programming with representations of types Jan 22, 2020

Show notes

This episode reviews some of the applications of GADTs we have discussed so far, and discusses an example where we want to write a function that consumes a number of inputs that is controlled by an argument to the function.

Using GADTs for typed subsetting of your language Jan 20, 2020

Show notes

One use case for GADTs (as a special case of dependent types) is to form a typed subset of your host language. One creates an EDSL called Expr a, where a is a type of the language (say this language is Haskell). Values of types Expr a are the abstract syntax trees of expressions of type a from your host language. This is just a special case of embedding a typed language into your host language: in this case the typed language is a subset of your host language.

Example of programming with indexed types: binary search trees Jan 16, 2020

Show notes

Using indexed types, we can restrict the form of legal values in some datatype. A nice example is binary search trees, where we can statically enforce the binary search tree property using an indexed type bst l u, where l is a lower bound and u an upper bound on the data stored in the tree.

Programming with indexed types using singletons Jan 16, 2020

Show notes

Basic idea of using singleton types like Nat n where n is a value from the index domain, to connect program expressions and index expressions. The data value of type Nat n is a copy of n, but living in the syntactic category of program expressions. This allows programs to operate on a proxy for n. Singletons library in Haskell mentioned.

Limitations of indexed types that are not truly dependent Jan 14, 2020

Show notes

If indices to types come from a different syntactic category than programs, there are a few things you cannot do. Some initial thoughts on how to work around these.

Programming with Indexed Types Jan 13, 2020

Show notes

Indexed datatypes like vectors, where the indices come from a different syntactic category than program expressions.

Program Termination and the Curry-Howard Isomorphism Jan 10, 2020

Show notes

For programs to make sense as proofs, they need to be terminating (cannot run forever), since otherwise you can write infinite loops that have any type. Under Curry-Howard this means any formula is provable, which is one way to define inconsistency. (And logics have to be consistent to be useful.)

Why Curry-Howard for classical proofs is a bad idea for programming Jan 06, 2020

Show notes

If you have dependent types, classical reasoning, and the Curry-Howard isomorphism, you can write programs that look like they are invoking oracles for undecidable problems -- but they are not, and this is confusing.

Curry-Howard for classical logic Jan 06, 2020

Show notes

CH can be applied to classical logic, too. The seminal paper is <a href="https://www.cl.cam.ac.uk/~tgg22/publications/popl90.pdf">A Formulae-as-Types Notion of Control</a> by Timothy Griffin. I discuss how backtracking implements the law of excluded middle.

Dependent types and design by contract Jan 03, 2020

Show notes

Dependent types are discussed, particularly as used for expressing pre- and post-conditions of functions.