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)
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?
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!
"Why recursion is not an option?"
"Because recursion is not an option!"
xD
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!
“…ending up with the actual systems that you could sit down and use and type things in”
I see what you did there.
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"
Interesting to see type theory in action....
so read this book before the little MLer ..?
(have read schemer and plan on reading seasoned and reasoned before I go for this)
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
Per Martin Lof Intuitionistic type theory.
What is the IDE/editor you used for the talk?
Found out it's just "racket gui/main.rkt" in the pie root folder
@@Drumnerd86 Hi. The compilation takes a few minutes. Is there a way to skip it next time and run it from the last compilation?