The Ur/Web Tutorial
Chapter 1: Introduction
Chapter 2: Type-Level Computation