"A Little Taste of Dependent Types" by David Christiansen

[@NoNameAtAll2]

"Why recursion is not an option?" "Because recursion is not an option!" xD

[@JulianWasTaken]

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)

[@andrewsinclair7654]

This was my favorite talk from Strangeloop 2018! Thanks David for the amazing presentation, slides, and a book too!

[@AndersBechMellson]

What an awesome introduction to dependent types. David is such a great presenter!

[@-ion]

“…ending up with the actual systems that you could sit down and use and type things in” I see what you did there.

[@desjajjaden49]

Watched this for literally 5 times, mind-blowing and really nice job!

[@vmguerra]

"Programs that evaluate to themselves are not the most fun of programs, we will get to some more fun ..ctional programs later"

[@oneheckofabanana2016]

Nice talk. I'm looking forward to reading the book and playing with Pie.

[@rossgeography]

so read this book before the little MLer ..? (have read schemer and plan on reading seasoned and reasoned before I go for this)

[@CyberneticOrganism01]

Interesting to see type theory in action....

[@anilraghu8687]

Per Martin Lof Intuitionistic type theory.

[@CyberneticOrganism01]

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

[@Drumnerd86]

What is the IDE/editor you used for the talk?

[@Drumnerd86]

Found out it's just "racket gui/main.rkt" in the pie root folder

[@GeorgWilde]

@@Drumnerd86 Hi. The compilation takes a few minutes. Is there a way to skip it next time and run it from the last compilation?