Thinking with Types
Thinking with Types
$24.99
Minimum price
$59.99
Suggested price
Thinking with Types

This book is 100% complete

Completed on 2018-11-12

About the Book

About the Author

Sandy Maguire
Sandy Maguire

Sandy might best be described somewhere between independent researcher and voluntarily-unemployed bum. At the ripe old age of 27 he decided to quit his highly-lucrative engineering job and decide to focus more on living than on grinding for the man. It's what you might call a work in progress.

He regularly writes about Haskell at reasonablypolymorphic.com.

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

The Leanpub 45-day 100% Happiness Guarantee

Within 45 days of purchase you can get a 100% refund on any Leanpub purchase, in two clicks.

See full terms...

Write and Publish on Leanpub

Authors, publishers and universities use Leanpub to publish amazing in-progress and completed books and courses, just like this one. You can use Leanpub to write, publish and sell your book or course as well! Leanpub is a powerful platform for serious authors, combining a simple, elegant writing and publishing workflow with a store focused on selling in-progress ebooks. Leanpub is a magical typewriter for authors: just write in plain text, and to publish your ebook, just click a button. It really is that easy.

Learn more about writing on Leanpub