"A Little Taste of Dependent Types" by David Christiansen
Why Hacker News recommends it
Recommended as an approachable introduction to dependent types and a preview of what The Little Typer covers.
What it is
David Christiansen gives a Strange Loop 2018 introduction to dependent types, where one language serves for both compile-time and run-time code and programs unite with proofs. It draws on his book The Little Typer.
Recommended by 2 HN commenters across 2 different months, 2018 to 2023.
What Hacker News said
Recommends adamgordonbell · 2022-10 · on “The Little Typer (2018)”
A very mind-blowing and challenging book about Types. The strange loop talk and my own interview of the authors might give some sense of what it's all about. There is also some interesting work online showing how the language used in the book can be created. [this video] [LINK] [LINK]
Recommends spelunker · 2023-01 · on “Idris: A Language for Type-Driven Development”
Here's an intro to dependent types from David Christiansen, I think it came up during another dependent types discussion: [this video]
Cites espeed · 2018-10 · on “Type-Driven Program Synthesis [video]”
Type-driven development, meta languages, specs, provably correct code, and automatic code generation were some of the big overlapping themes at Strange Loop [1] this year. All the talks posted online this week [2], and I've posted links to some of the related videos below [3]. It's a good indicator that the time has come for an idea when multiple lines of research and projects from disparate domains begin converging on the same idea from different directions. Several facets of the puzzle I've been working the last few years have converged towards this area so it's good to see that it's not just me, maybe that means we're all on the right track. But as 'pron and those who have been working in