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

The Technium

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