Tech Talk: The Little Typer With Daniel Friedman and David Thrane Christiansen
CoRecursive: Coding Stories
00:00
The Recursion Operator Is Dependently Typed
The dependently typed version of that takes one additional argument, which is what we call the motive. The motive explains what the type is for in terms of the list that you're recurring over. And then by combining these at each step, you get the relationship between the resulting type and the list th you are looking at right now is maintained appropriately. So i really like the book. M i'm goin, i'm going to keep working on it, like i have found it. It's calledit wel you're talking about induction now? Yes, yes.
Transcript
Play full episode
