{"type":"rich","version":"1.0","provider_name":"Transistor","provider_url":"https://transistor.fm","author_name":"The Technium","title":"Dependent Types: Runtime assertions at compile time...whaaa? (S04E08)","html":"<iframe width=\"100%\" height=\"180\" frameborder=\"no\" scrolling=\"no\" seamless src=\"https://share.transistor.fm/e/c107e2bd\"></iframe>","width":"100%","height":180,"duration":7627,"description":"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.\n\nShow notes:\nProposition as Types\nParse, Don’t Validation\n“Scala vs Idris: Dependent types, now and in the future”\nResources:\nhttp://www.e-pig.org/downloads/ydtm.pdf\nhttps://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c375196\nProof Theory Impressionism: Blurring the Curry-Howard Line\nType Systems - The Good, Bad and Ugly\nDependent types for practical use\nIdris: Practical Dependent Types with Practical Examples\nMaking Illegal States unrepresentable\nCan types replace validation\nhttps://www.cs.ox.ac.uk/ralf.hinze/WG2.8/26/slides/xavier.pdf","thumbnail_url":"https://img.transistorcdn.com/s_TeOjvmo9Kza_wHNraLFOqoG1-rSKJllNhkA8fY_ps/rs:fill:0:0:1/w:400/h:400/q:60/mb:500000/aHR0cHM6Ly9pbWct/dXBsb2FkLXByb2R1/Y3Rpb24udHJhbnNp/c3Rvci5mbS9zaG93/LzI2NjMwLzE2NDA4/Mjg2MjMtYXJ0d29y/ay5qcGc.webp","thumbnail_width":300,"thumbnail_height":300}