Types as Program Specifications: A Intro to Type-Level Programming in Haskell
summary
Argues that types serve as executable specifications and shows how to embed invariants in GHC using language extensions: GADTs, DataKinds, TypeFamilies (plus KindSignatures, multi‑param type classes, phantom types). Builds a typed AST evaluator that cannot express ill‑formed programs, length‑indexed lists with append and head/tail, and Peano naturals with type‑level add/multiply; many exercises (1–5) guide the steps. Compilation and reductions happen at compile time, some solutions need UndecidableInstances and careful kind polymorphism to avoid gnarly type errors.
AI-written summary · about
chapters (30)
- 0:00Start
- 3:24Overview
- 4:05First Class Type Families
- 4:35What Is the Specification
- 5:11What Is the Type
- 5:51Values Types and Kinds
- 7:08Prerequisite Knowledge
- 7:20Static versus Dynamic Type Systems
- 8:11What Haskell Is
- 9:13Language Extensions
- 13:16Type Constructors
- 16:26Kind Signatures
- 20:47A Phantom Type
- 24:39Conversion Function
- 27:46Type Signature
- 30:13Generalized Algebraic Data Types
- 30:30Algebraic Data Types
- 36:51Motivation for Generalized Andrei Data Types
- 1:01:10Solution
- 1:05:34Type Families
- 1:10:49Or Type Family
- 1:17:54Kind Inference
- 1:26:17Peano Axioms
- 1:27:14Type Level Natural Numbers
- 1:37:37Type Operators
- 1:45:45Length Index Lists
- 1:46:44Live Coding
- 1:48:13Base Case
- 1:50:07Append Two Lists
- 1:52:16Append To List
