Maguire S. Thinking with Types

Sandy Maguire, 2019. — 249 p.This book aims to be the comprehensive manual for type-level programming. It's about getting you from here to there — from a competent Haskell programmer to one who convinces the compiler to do their work for them.Fundamentals
The Algebra Behind Types
Isomorphisms and Cardinalities
Sum, Product and Exponential Types
Example: Tic-Tac-Toe
The Curry--Howard Isomorphism
Canonical Representations
Terms, Types and Kinds
The Kind System
The Kind of "Types"
Arrow Kinds
Constraint Kinds
Data Kinds
Promotion of Built-In Types
Symbols
Natural Numbers
Lists
Tuples
Type-Level Functions
VarianceLifting Restrictions
Working with Types
Type Scoping
Type Applications
Ambiguous Types and Non-Injectivity
Constraints and GADTsGADTs
Heterogeneous Lists
Rank-N TypesRanks
The Nitty Gritty Details
The Continuation Monad
Existential Types
Existential Types and Eliminators
Dynamic Types
Generalized Constraint Kinded Existentials
Scoping Information with Existentials
Roles
Coercions
RolesComputing at the Type-Level
Associated Type Families
Building Types from a Schema
Generating Associated Terms
First Class Families
Defunctionalization
Type-Level Defunctionalization
Working with First Class Families
Ad-Hoc Polymorphism
Extensible DataOpen Sums
Open Products
Overloaded Labels
Custom Type Errors
Generics
Generic Representations
Deriving Structural Polymorphism
Using Generic Metadata
Performance
Kan Extensions
Indexed Monads
Definition and Necessary Machinery
Linear Allocations
Dependent TypesOverviewAd-Hoc Implementation
Generalized Machinery
The Singletons Package
Dependent Pairs
Structured LoggingSolutions