Iowa Type Theory Commute

Curry-style typing and realizability make it sensible to allow a top type to type every term, even non-normalizing ones.

Intersection types internalize the idea that a term has two types.  Curry-style typing is generally needed for this to be nontrivial.

In Curry-style typing annotations -- for example, the types of bound variables -- are erased, and not truly (semantically) part of the term.  In Church-style, they are intrinsic to the term and are truly there.  Discussion of some of the practicalities of Curry-style typing, in particular type annotations versus proving typings.

Types are specifications whose semantics is explained in terms of computation, which is thus conceptually prior.  Realizability is a way of explaining the semantics of types.

In which I argue that type information should be erased from programs by the compiler both for final execution and also for reasoning (in a language with dependent types, for example, where we can reason about program execution statically).

GADTs are quite powerful.  Why go all the way to true dependent types?  And should you use the Curry-Howard isomorphism (see Chapter 3 of the podcast) or not?

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.  

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

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.

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.

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.

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

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

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.

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 are discussed, particularly as used for expressing pre- and post-conditions of functions.

I follow up on some comments I made about Curry-Howard for first-order quantifiers in the previous episode.  Sheard's Omega language also mentioned (see links on <a href = "http://web.cecs.pdx.edu/~sheard/">his web page</a>).  First-order quantifications turn into indexed types where the indices are not program expressions but come from another syntactic domain.

Discussion of the Curry-Howard isomorphism for the connectives of propositional logic (AND, OR, NOT, FALSE, IMPLIES).  Initial consideration of Curry-Howard for first-order and higher-order logic.  Dependent types.

In which I discover why the domino analogy for explaining induction always bothered me!

We consider the basic idea of the Curry-Howard isomorphism, that constructive proofs are essentially programs, and vice versa.  Several simple examples.  Why the law of excluded middle is not a legal constructive proof.

More about the structured recusion scheme known as the catamorphism.  Basic idea of functors.

The basic idea of the Curry-Howard isomorphism, and its connection to the contents of Chapters 1 and 2.  Constructive proof.  A famous nonconstructive proof.

Review of basic application of category theory for functional programming.  Recursion schemes are combinators that let you write point-free recursions.

A few very basic ideas of categories and combinators.  Also, the problem of understanding very concise code.

Relation of point-free functional programming to category theory.