"A Little Taste of Dependent Types" by David Christiansen
37,244
Published 2018-10-16
The essential beauty of dependent types can sometimes be hard to find under layers of powerful automatic tools. The Little Typer is an upcoming book on dependent types in the tradition of the The Little Schemer that features a tiny dependently typed language called Pie. We will demonstrate a proof in Pie that is also a program.
Come get a taste of Pie, and see for yourself where dependent types can take us.
Speaker: David Christiansen
All Comments (15)
-
"Why recursion is not an option?" "Because recursion is not an option!" xD
-
On the incredibly odd chance someone gets just as confused as I was for a few seconds, at 31:44, when he says "that's because _ curries all of its arguments just like Haskell", the _ he means is "Pie" (the language they created), not Pi (i.e. Π) the dependent type thing he is confusingly in the middle of explaining. (So all functions in that language get curried, not that Π is somehow doing something special to that lambda function)
-
“…ending up with the actual systems that you could sit down and use and type things in” I see what you did there.
-
This was my favorite talk from Strangeloop 2018! Thanks David for the amazing presentation, slides, and a book too!
-
"Programs that evaluate to themselves are not the most fun of programs, we will get to some more fun ..ctional programs later"
-
What an awesome introduction to dependent types. David is such a great presenter!
-
Nice talk. I'm looking forward to reading the book and playing with Pie.
-
Watched this for literally 5 times, mind-blowing and really nice job!
-
so read this book before the little MLer ..? (have read schemer and plan on reading seasoned and reasoned before I go for this)
-
Interesting to see type theory in action....
-
Per Martin Lof Intuitionistic type theory.
-
The "programs" here are used to prove mathematical statements, eg. that a number is either odd or even. If I write a program to calculate the Fibonacci numbers, what is the mathematical statement that this program proved?
-
What is the IDE/editor you used for the talk?
-
I don't understand why we avoid negative integers. I've been experimenting with refinement types and I keep seeing negative numbers being excluded. Why would a refinement library give me the ability to ensure for example 2 < x < 10 but not -3 < x < 0?
