"A Little Taste of Dependent Types" by David Christiansen
Ғылым және технология
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
Пікірлер: 22
"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.
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.
"Programs that evaluate to themselves are not the most fun of programs, we will get to some more fun ..ctional programs later"
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....
What is the IDE/editor you used for the talk?
@rodrigostevaux5642
5 жыл бұрын
Found out it's just "racket gui/main.rkt" in the pie root folder
@GeorgWilde
2 жыл бұрын
@@rodrigostevaux5642 Hi. The compilation takes a few minutes. Is there a way to skip it next time and run it from the last compilation?
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?
@mattetis
Жыл бұрын
You would have proved that the Fibonacci numbers exist right? That this is well defined: F0 = 0 F1 = 1 Fn = Fn-1 + Fn-2
Per Martin Lof Intuitionistic type theory.
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?
@lunaphipps-costin8516
3 жыл бұрын
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
@mushchlowastaken
Жыл бұрын
@@lunaphipps-costin8516 with a wrapper datatype, it doesn't have to be gross
@lepidoptera9337
Жыл бұрын
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.
@insertoyouroemail
7 ай бұрын
@@lepidoptera9337 Really? Interesting.