Thinking with Types

Table of Contents
Preface
Acknowledgments
Introduction

I Fundamentals
1 - The Algebra Behind Types
1.1 - Isomorphisms and Cardinalities
1.2 - Sum, Product and Exponential Types
1.3 - Example: Tic-Tac-Toe
1.4 - The Curry--Howard Isomorphism
1.5 - Canonical Representations
2 - Terms, Types and Kinds
2.1 - The Kind System
2.1.1 - The Kind of "Types"
2.1.2 - Arrow Kinds
2.1.3 - Constraint Kinds
2.2 - Data Kinds
2.3 - Promotion of Built-In Types
2.3.1 - Symbols
2.3.2 - Natural Numbers
2.3.3 - Lists
2.3.4 - Tuples
2.4 - Type-Level Functions
3 - Variance

II Lifting Restrictions
4 - Working with Types
4.1 - Type Scoping
4.2 - Type Applications
4.3 - Ambiguous Types and Non-Injectivity
5 - Constraints and GADTs
5.1 - Introduction
5.2 - GADTs
5.3 - Heterogeneous Lists
6 - Rank-N Types
6.1 - Introduction
6.2 - Ranks
6.3 - The Nitty Gritty Details
6.4 - The Continuation Monad
7 - Existential Types
7.1 - Existential Types and Eliminators
7.1.1 - Dynamic Types
7.1.2 - Generalized Constraint Kinded Existentials
7.2 - Scoping Information with Existentials
8 - Roles
8.1 - Coercions
8.2 - Roles

III Computing at the Type-Level

9 - Associated Type Families
9.1 - Building Types from a Schema
9.2 - Generating Associated Terms
10 - First Class Families
10.1 - Defunctionalization
10.2 - Type-Level Defunctionalization
10.3 - Working with First Class Families
10.4 - Ad-Hoc Polymorphism
11 - Extensible Data
11.1 - Introduction
11.2 - Open Sums
11.3 - Open Products
11.4 - Overloaded Labels
12 - Custom Type Errors
13 - Generics
13.1 - Generic Representations
13.2 - Deriving Structural Polymorphism
13.3 - Using Generic Metadata
13.4 - Performance
13.5 - Kan Extensions
14 - Indexed Monads
14.1 - Definition and Necessary Machinery
14.2 - Linear Allocations
15 - Dependent Types
15.1 - Overview
15.2 - Ad-Hoc Implementation
15.3 - Generalized Machinery
15.4 - The Singletons Package
15.5 - Dependent Pairs
15.5.1 - Structured Logging

IV Appendices
Glossary
Solutions
Bibliography
About the Author