"A Little Taste of Dependent Types" by David Christiansen
ฝัง
- เผยแพร่เมื่อ 5 ก.ค. 2024
- Dependent types let us use the same programming language for compile-time and run-time code, and are inching their way towards the mainstream from research languages like Coq, Agda and Idris. Dependent types are useful for programming, but they also unite programming and mathematical proofs, allowing us to use the tools and techniques we know from programming to do math.
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 - วิทยาศาสตร์และเทคโนโลยี
"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)
This was my favorite talk from Strangeloop 2018! Thanks David for the amazing presentation, slides, and a book too!
“…ending up with the actual systems that you could sit down and use and type things in”
I see what you did there.
"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!
Watched this for literally 5 times, mind-blowing and really nice job!
Nice talk. I'm looking forward to reading the book and playing with Pie.
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?
You would have proved that the Fibonacci numbers exist right?
That this is well defined:
F0 = 0
F1 = 1
Fn = Fn-1 + Fn-2
What is the IDE/editor you used for the talk?
Found out it's just "racket gui/main.rkt" in the pie root folder
@@rodrigostevaux5642 Hi. The compilation takes a few minutes. Is there a way to skip it next time and run it from the last compilation?
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?
Milligram naturals are defined by recursion to zero (4 is S S S S 0). integers would be Either Nat Nat, which is just a little more annoying
@@lunaphipps-costin8516 with a wrapper datatype, it doesn't have to be gross
In computation? For the same reason we are avoiding the integers. They are not computable, therefor having any kind of type system for them is, at best, a mathematical April's Fools joke.
@@lepidoptera9337 Really? Interesting.