Iowa Type Theory Commute

Latest Episodes:

Introduction to type safety Mar 02, 2020

Show notes

Type safety is a basic property of both statically typed programming languages and type theories. It has traditionally (past few decades) been decomposed into type preservation and progress. Type preservation says that if a program expression e has some type T, then running e a bit will give a result that still has type T (and type preservation would apply again to that result, to preserve the type T indefinitely along the execution of e). Progress says that well-typed expressions cannot get stuck computationally: they cannot reduce to a form where the operational semantics is then undefined. This is how we model the idea that the type system is preventing certain kinds of failures: make those failures correspond to undefined behavior.

Introduction to metatheory Feb 28, 2020

Show notes

Metatheory is concerned with proving properties about theories, in this case type theories or programming languages.

Definition of the Mendler encoding Feb 26, 2020

Show notes

We consider using Mendler's technique of abstracting out problematic types with new type variables, and how this can yield a lambda encoding where the programmer is in charge of when to make recursive calls (rather than in the Church encoding, where the data present the programmer's combining function with the results of all possible recursive calls on immediate subdata).

The Mendler encoding and the problem of explicit recursion Feb 25, 2020

Show notes

The Church encoding allows definition of certain recursive functions, but all the recursive calls are implicit. The encoding simply presents you with the results of recursion for all immediate subdata. Using a technique due to Mendler, an encoding is possible where recursions are explicitly made by the combining functions given to the data.

The Scott encoding Feb 24, 2020

Show notes

In this episode we briefly review the Church and Parigot encodings (discussed previously in Chapter 6 of this podcast) and then consider the Scott encoding, where combining functions receive only the immediate subdata of the data.

More on the Parigot encoding Feb 21, 2020

Show notes

The Parigot encoding has exponential-size normal forms: but don't panic! With a decent graph-sharing implementation of lambda calculus, they take linear space in memory.

Introduction to the Parigot encoding Feb 18, 2020

Show notes

The Parigot encoding solves the Church encoding's problem of inefficient predecessor. It can be typed using positive-recursive types, which preserve normalization of the type theory.

Church-encoding natural numbers Feb 17, 2020

Show notes

What is fold-right for a natural number? How do we define addition with this? The problem of inefficient predecessor.

Church encoding of lists Feb 14, 2020

Show notes

We consider fold-right for lists, and its static type. The Church encoding for lists makes them into their own fold-right functions

Church encoding of the booleans Feb 14, 2020

Show notes

The Church encoding represents data as their own fold-right functions. For booleans, this means they become their own if-then-else expressions. We consider the polymorphic type for these, which is forall X. X -> X -> X.

Our TOPPODCAST Picks

Follow Us

Stay Connected

Related Podcasts

Links

Stay Connected

Our TOPPODCAST Picks

Follow Us

Stay Connected

Iowa Type Theory Commute

Related Podcasts

1

2

3

4

5

6