View Source Document

Chris Pressey.md

Commentary by Chris Pressey

This work is distributed under a CC-BY-ND-4.0 license, with the following explicit exception: the ratings may be freely used for any purpose with no limitations.

Type Theory

Basic Simple Type Theory

When I first tried to read it, I found it neither basic nor simple.

Type Theory and Functional Programming

.

Programming in Martin-Löf’s Type Theory

.

Recursive Types

Based on Pierce's book on types in programming languages.

Recursive types are at the intersection of type theory and type systems, in the sense that they are useless for the purpose of logic, but they still have a theoretical underpinning.

A recursive type expression represents an infinite regular tree. Plain old inductive methods are not sufficient for proofs about type expressions, because we're talkin' infinite sets of infinite objects here.

Section 4 is mostly giving an algorithm for finding the greatest fixed point.

On Universes in Type Theory

The paper seems primarily concerned with considering the proof-theoretic strength of type theories with universes (or rather, type theories extended with universe-manipulating operators); and proof-theoretic strength doesn't interest me terribly much. However, in so doing, it gives some coverage of the concept of universes, which is useful.

They define "logical framework" as a typed lambda calculus with a dependent function space construction (big-Pi) and a universe of types (called sets). And they point out that LFs are used in modern expositions of type theories but aren't strictly speaking necessary.

Two conceptions of universe: universes as full reflections and universes as uniform constructions. They prefer the latter as it is easier to formalize for transfinite hierarchies (valuable for establishing proof-theoretic strength results). (The construction for full reflections also has issues when extended into the transfinite: you get a universe with infinitely many introduction rules, and formulating a corresponding elimination rule would need some kind of internal indexing of universes.)

If you have a universe formation operator and you close over it (something like taking the least fixpoint, I suppose) you get a "super universe", which is (unsurprisingly) closed over universe formation.

At a Remark at the end of section 4 they note that the proof-theorist's notion of predicativity and the constructivist's notion of predicativity are slightly different.

In section 6 they formulate impredicative theories using universes, noting that such universes have no inductive structure (which seems reasonable).

In section 7 they show that classical (excluded-middle-accepting) logic can be captured in a universe, and describe it, "in a precise sense", as "a (small-)complete boolean algebra with prescribed falsity". This was apparently implemented in the proof assistant ALF and used on "a small program extraction problem" (presumably supporting assertions about the program that were phrased in classical logic?)

The Gentle Art of Levitation

The authors reify the set of inductive types (and then the set of inductive families) in a dependent type theory (a dependently typed language); that is, they devise a way to describe such types as values in the language. Further, these values inhabit a type; and that type, too, can be described as such a value.

They do this for the purpose of supporting generic programming. There are some significant metatheoretic gaps though, mainly that the type of SET is SET. There are ideas about how to stratify the consytruction properly but they seem incomplete. They note that finite "truncations" of the hierarachy have been formalized in Agda, and claim that it is "clear that some such system can be made to work, or else that other, longer-standing tools are troubled". Which is sufficient for practical work, I suppose, but really unsatisfying on the theoretical side of things.

Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega

.

A lean specification for GADTs: system F with first-class equality proofs

This paper was surprisingly easy to read. While implementing GADTs in Utrect's Haskell compiler, the authors wanted a clean basis for their specification; and finding existing approaches too implementation-based, came up with one.

This helped make it clearer to me "how GADTs work": they need a proof of equality between types. In Haskell, such a proof is constructed automatically. This complicates type inference, because inferring the type "across the equality proof" makes it more ambiguous.

The embedding of the equality proof in System F is a little unspectacular. It seems like you could just as easily embed anything other kind of proof there in the same way. Not that that's bad.

(Also: the difference between destructorizers and the Church encoding of ADTs is that in the Church encoding, the value itself is the destructorizer.)

Observational Equality, Now!

Observational Type Theory (OTT): it's intensional, but it identifies values up to observational equivalence (like final algebra semantics), which the authors claim make it "just as powerful for reasoning" as extensional theories.

Type Theory (Stanford Encyclopedia of Philosophy)

future-rating: 2.5

Intuitionistic Type Theory (Stanford Encyclopedia of Philosophy)

future-rating: 2.5

computability - Does there exist a Turing complete typed lambda calculus? - Computer Science Stack Exchange

.

Characterization of lambda-terms that have union types - Computer Science Stack Exchange

.

Type Theory and Mathematical Logic \| artagnon.com

.

Typed Combinators

.

Recursive Types for Free! (Philip Wadler)

.

Computational type theory - Scholarpedia

.