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