Type Theory Forall #39 Equality, Quotation, Bidirectional Type Checking - David Christiansen
Jun 13, 2024
David Christiansen, former Executive Director of the Haskell Foundation, talks about writing The Little Typer, Equality, Bidirectional Type Checking, and Quotation with the host. They explore the challenges of book reprints, bi-directional type checking, macro implementation, and Lean macros. Technical discourse on content levels and audience interaction, with insights on normalization by evaluation and personal anecdotes.
Chapters
Transcript
Episode notes
1 2 3 4 5 6 7 8 9 10 11
Intro
00:00 • 2min
The Little Typer: Teaching Dependent Types in Programming Languages
02:24 • 11min
Exploring Equality and Judgments in Type Theory
13:33 • 14min
Navigating Book Reprints and the Publishing Process with MIT Press
27:33 • 5min
Bi-Directional Type Checking and its Implementation Challenges
32:23 • 19min
Exploring Quotation and Quasi-Quotation in Programming Languages
51:36 • 12min
Challenges and Solutions in Macro Implementation
01:03:58 • 18min
Exploring Macros, Quotation, and Syntax in Lean
01:21:45 • 20min
Technical Discourse on Content Levels and Audience Interaction
01:41:57 • 2min
Exploring the Intersection of Pi Implementation, Normalization by Evaluation, and Bidirectional Type Checking
01:43:40 • 2min
Exploration of Bidirectional Type Checking and Personal Anecdotes
01:45:49 • 4min