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