The Future of Programming with Richard Eisenberg
Signals and Threads
00:00
The Importance of Dependent Types in Programming Languages
A dependent type is a type that can depend on some input that you give into a function, essentially. The output of the function must be a permutation of the input. And then if I've encoded this, my compiler will check that my algorithm actually does sorting and doesn't do some other thing. So when I started grad school, then I saw Haskell and here was a language that had this fancy type system and had all this expressiveness. It didn't quite have dependent types, but it had a lot of that stuff that just got me excited.
Play episode from 01:33
Transcript
