Dependent Types: Runtime assertions at compile time...whaaa? (S04E08)

Dependent types are a more expressive type system in programming languages used to catch a larger class of errors at compile time. What are would be typically assertions at runtime can now be caught at compile time. Show notes: Proposition as Types Parse, Don’t Validation “Scala vs Idris: Dependent types, now and in the future” Resources: http://www.e-pig.org/downloads/ydtm.pdf https://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c375196 Proof Theory Impressionism: Blurring the Curry-Howard Line Type Systems - The Good, Bad and Ugly Dependent types for practical use Idris: Practical Dependent Types with Practical Examples Making Illegal States unrepresentable Can types replace validation https://www.cs.ox.ac.uk/ralf.hinze/WG2.8/26/slides/xavier.pdf