# So many data types, so little time

I find my mathematics and programming background$$^*$$ do not endow me with much understanding of type theory as it pertains to proof assistants. To remedy this shortcoming I don't expect a Royal Road to understanding, and my strategy is mixed.

I ordered Type Theory and Formal Proof -- An Introduction by Nederpelt and Geuvers (2014), a real hardcover book which Barendregt's Foreword claims to provide "a gentle, yet profound, introduction to systems of types and their inhabiting lambda-terms." Although the book stretches out to some four hundred pages, it gets there in chapters of twenty to forty pages, each capped by exercises to assess ones comprehension.

I'm also installing Lean 4 and pursuing as a tutorial Mathematics in Lean hoping to see the hierarchy of types in a familiar enough perspective.

This is me "hitting it high, hitting it low". I'm interested in other approaches and ways to expedite learning.

• My math background includes formal logic, algebra, combinatorics, category theory and a good bit of numerical methods, and my programming skills are weighted toward object-oriented procedural languages (C++), Prolog, and database stuff.
• If you would like a really down-to-the-earth route, I would recommend The Little Typer from MIT Press (IIRC), which strips type theory of all the fancy stuff so you can concentrate on the core.
– Trebor
Mar 2, 2022 at 4:29
• I think you just need to think of propositions as sets of their proofs, and start to do some math in Lean 4. Mar 2, 2022 at 6:03
• "Software Foundations" is also a really good introduction. Mar 2, 2022 at 6:41
• If you have a more mathematical background, I think the first section of the "Homotopy Type Theory" book (freely available on line) is excellent. That section is just about dependent type theory, and one can stop before meeting the "homotopy" part. Mar 6, 2022 at 5:48
• If you want a minimal, hands on introduction I recommend Agda + plfa.github.io . Agda is more like a programming language than most other type systems. While other systems build a lot of stuff on-top of their types theories, Agda does not. Agda really lets the underling system shine through. Apr 6, 2022 at 18:39

I find my mathematics and programming background do not endow me with much understanding of type theory as it pertains to proof assistants.

So many data types, so little time

Oregon Programming Languages Summer School — July 16-28, 2012

The program consists of 80 minute lectures presented by internationally recognized leaders in programming languages and formal reasoning research.

(ref) - Free access to all of the videos of the lectures.

Technical Lectures

As noted in a comment by Albert ten Napel

Software Foundations

The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software.

The principal novelty of the series is that every detail is one hundred percent formalized and machine-checked: the entire text of each volume, including the exercises, is literally a "proof script" for the Coq proof assistant.

(ref)

Types and Programming Languages
by Benjamin C. Pierce
(WorldCat) (Site)

Most of the type theories derive from Lambda Calculus. This is book is Lambda Calculus on steroids.

List of types from the book

Name                   Extends/Based on Figure                          Figure                                                   Page
B untyped                                                                3-1 Booleans (B)                                         34
B ℕ (untyped)          Extends 3-1 B                                    3-2 Arithmetic expressions (ℕB)                          41
→ (untyped)                                                             5-3 Untyped lambda-calculus (λ)                           72
B (typed)              Extends 3-1 B                                    8-1 Typing rules for Booleans (B)                        93
B ℕ (typed)            Extends 3-1, 8-1 B                               8-2 Typing rules for numbers (ℕB)                        93
→ (typed)              Based on5-3 λ                                    9-1 Pure simply typed lambda-calculus (λ→)               103
→ Unit                 Extends 9-1 λ→                                   11-2 Unit type                                           119
→ as                   Extends 9-1 λ→                                   11-3 Ascription                                          122
→ let                  Extends 9-1 λ→                                   11-4 let binding                                         124
→ x                    Extends 9-1 λ→                                   11-5 Pairs                                               126
→ {}                   Extends 9-1 λ→                                   11-6 Tuples                                              128
→ {}                   Extends 9-1 λ→                                   11-7 Records                                             129
→ {} let p (untyped)   Extends 11-7, 11-4                               11-8 (Untyped) record patterns                           131
→ +                    Extends 9-1 λ→                                   11-9 Sums                                                132
→ +                    Extends 9-1 λ→                                   11-10 Sums (with unique typing)                          135
→ <>                   Extends 9-1 λ→                                   11-11 Variants                                           136
→ fix                  Extends 9-1 λ→                                   11-12 General recursion                                  144
→ B List               Extends 9-1 λ→ with 8-1 Booleans                 11-13 Lists                                              147
→ Unit Ref             Extends 9-1 λ→ with 11-2 Unit                    13-1 References                                          166
→ error                Extends 9-1 λ→                                   14-1 Errors                                              172
→ error try            Extends 9-1 λ→ with 14-1 Errors                  14-2 Error handling                                      174
→ exceptions           Extends 9-1 λ→                                   14-3 Exceptions carrying values                          175
→ <: Top               Extends 9-1 λ→                                   15-1 Simply typed lambda-calculus with subtyping (λ<:)   186
→ {} <:                Extends 15-1 λ<: and 11-7 Records                15-3 Records and subtyping                               187
→ <: Bot               Extends 15-1 λ<:                                 15-4 Bottom type                                         192
→ <> <:                Extends 15-1 λ<: and 11-11 Simple variant rules  15-5 Variants and subtyping                              197
→ {} <:                Extends 15-1 λ<: and 15-3 Records and subtyping  16-1 Subtype relation with records (compact version)    211
→ {} <:                                                                 16-2 Algorithmic subtyping                               212
→ {} <:                                                                 16-3 Algorithmic typing                                  217
→ u                    Extends 9-1 λ→                                   20-1 Iso-recursive types (λu)                            276
→∀                     Based on 9-1 λ→                                  23-1 Polymorphic lambda-calculus (System F)              343
→∀∃                    Extends 23-1 System F                            24-1 Existential types                                   366
→∀∃ Top                Based on 23-1 System F and 15-1 simple subtyping 26-1 Bounded quantification (kernel F<:)                 392
→∀∃ Top full           Extends 26-1 F<:                                 26-2 "Full" bounded quantification                       395
→∀<: Top ∃             Extends 26-1 F<: and 24-1 unbounded existentials 26-3 Bounded existential quantification (kernel variant) 406
→∀<: Top                                                                28-1 Exposure Algorithm for F<:                          418
→∀<: Top               Extends 16-3 λ<:                                 28-2 Algorithmic typing for F<:                          419
→∀<: Top               Extends 16-2 λ<:                                 28-3 Algorithmic subtyping for kernel F<:                422
→∀<: Top full          Extends 28-3                                     28-4 Algorithmic subtyping for full F<:                  424
-⇒                     Extends 9-1 λ→                                   29-1 Type operators and kinding (λω)                     466
-∀⇒                    Extends 29-1 λω and 23-1 System F                30-1 Higher-order polymorphic lambda-calculus (Fω)       450
-∀∃⇒                   Extends 30-1 Fω and 24-1                         30-2 Higher-order existential types                      452
-∀⇒<: Top              Based on 30-1 Fω and 16-1 kernel F<:             31-1 Higher-order bounded quantification (Fω<:)          470
-∀<: Top {}←           Based on 26-1 F<: with 11-7 records              32-1 Polymorphic update                                  485


Advanced Topics in Types and Programming Languages
Edited by Benjamin c. Pierce
(WorldCat) (Site)

Practical Foundations for Programming Languages Second Edition
by Robert Harper
(WorldCat) (Site)

This text develops a comprehensive theory of programming languages based on type systems and structural operational semantics. (from publisher site)

As noted in a comment by Scott Morrison

If you have a more mathematical background, I think the first section of the "Homotopy Type Theory" book (freely available on line) is excellent. That section is just about dependent type theory, and one can stop before meeting the "homotopy" part.

Homotopy Type Theory - Univalent Foundations of Mathematics
A collaborative effort.

Contents

I Foundations

1. Type theory
2. Homotopy type theory
3. Sets and logic
4. Equivalences
5. Induction
6. Higher inductive types
7. Homotopy n-types

II Mathematics

1. Homotopy theory
2. Category theory
3. Set theory
4. Real numbers

Appendix
A Formal type theory
Index of symbols

(pdf) (LaTeX) (GitHub)

Proofs and Types
by Jean-Yves Girard
(pdf) (WorldCat) (PLS Lab)

Based on a short graduate course on typed lambda-calculus given at the Université Paris VII in the autumn term of 1986-7. (ref)

1. Sense, Denotation and Semantics
2. Natural Deduction
3. The Curry-Howard Isomorphism
4. The Normalisation Theorem
5. Sequent Calculus
6. Strong Normalisation Theorem
7. Gödel's system T
8. Coherence Spaces
9. Denotational Semantics of T
10. Sums in Natural Deduction
11. System F
12. Coherence Semantics of the Sum
13. Cut Elimination (Hauptsatz)
14. Strong Normalisation for F
15. Representation Theorem

Handbook of Practical Logic and Automated Reasoning
by John Harrison
(Site) (WorldCat) (Code and resources)

HOL Light was written by John Harrison (ref) who also authored "Handbook of Practical Logic and Automated Reasoning". Think of the book as a very detailed introduction to the code for HOL Light. (GitHub)

The book takes one from Boolean Logic all the way up to Interactive theorem proving.

Lectures on the Curry-Howard Isomorphism
by M.H. Sorensen and P. Urzyczyn (WorldCat)

Contents

1. Type-free λ-calculus
2. Intuitionistic logic
3. Simply type λ-calculus
4. The Curry-Howard isomorphism
5. Proofs as combinators
6. Classical logic and control operators
7. Sequent calculus
8. First-order logic
9. First-order arithmetic
10. Gödel's system T
11. Second-order logic and polymorphism
12. Second-order arithmetic
13. Dependent types
14. Pure type systems and the λ-cube

ML for the Working Programmer 2nd Edition
by L.C. Paulson
(WorldCat) (Site)

Most of the book is a standard book for learning a programming language.
Chapter 10 A Tactical Theorem Prover is the icing on the cake.

Handbook of Automated Reasoning
Edited by Alan Robinson and Andrei Voronkov
(WolrdCat) 2 volume set.

Published in 2001, most of it is foundational and still of value today.

As you noted recommended tutorials are worth their weight in gold.

Typing rules of proof assistants

• Lean
"The Type Theory of Lean"
by Mario Carneiro
(pdf)

• Coq
Docs » Core language » Typing rules

Lambda Cube
(Wikipedia)

In mathematical logic and type theory, the λ-cube (also written Lambda Cube) is a framework introduced by Henk Barendregt to investigate the different dimensions in which the calculus of constructions is a generalization of the simply typed λ-calculus. Each dimension of the cube corresponds to a new kind of dependency between terms and types. (from Wikipedia)

If you cover all of that then you can jump into this Q&A.

What are the bases for different Proof Assistants?

Obviously this list can go on an on. My main purpose with this answer was to get one going with their bootstraps.

Bonus section for those who do not have a background in logic.

forall x - An Introduction to Formal Logic
by P.D. Magnus
(pdf) (Site)

forall x is an Open Education Resource (OER) introductory textbook in formal logic. It covers translation, proofs, and formal semantics for sentential and predicate logic. (from homepage)

Since this is an OER there are many follow on books based on this. (Google search)

Bonus section for those who do not have a background in λ-calculus.

The Lambda Calculus
Stanford Encyclopedia of Philosophy

"An Introduction to Functional Programming Through Lambda Calculus" by Greg Michaelson
(WorldCat) (Site)

"The Lambda Calculus Its Syntax and Semantics"
by H.P. Barendregt
(WorldCat) (Site)

Bonus section for those lost in the terminology

Bonus section for those needing the history of types.

Functions and Types in Logic, Language and Computation
by Fairouz Kamareddine
(pdf)

Bonus section of food for thought.

Counterexamples in Type Systems

The "counterexamples" here are programs that go wrong in ways that should be impossible: corrupt memory in Rust, produce a ClassCastException in cast-free Java, segfault in Haskell, and so on. This book is a collection of such counterexamples, each with some explanation of what went wrong and references to the languages or systems in which the problem occurred.

It's intended as a resource for researchers, designers and implementors of static type systems, as well as programmers interested in how type systems fit together (or don't).

Bonus section for Prolog programmers.
Hint: SWI-Prolog

COT5315 Foundations of Programming Languages and Software Systems
by Robert van Engelen and Steven Bronson (ref)

Prolog code that does rules of inference (think typing rules). The code no longer works with the current version of SWI-Prolog but if one knows Prolog it is not hard to update.

Found this today on GitHub and gave it a try. It is a very gentle way to get started with Prolog and natural deduction. As the code is for a bachelor’s project thesis don't expect much but the core prover (system.pl) seems to work. Still have to hand verify the examples.