Tech Talk: Idris, Proofs and Haskell with Edwin Brady
CoRecursive: Coding Stories
00:00
Idres
If you want your programme to compile based on a run time format string, you're going to have to check that format string at run time. The only way the machine is going to let me call the er vectr adition function is if i've checked that the inputs are the same length. So by having more precise types, we're not freeing the programmer from having to do run time checks,. but we are freeing the programme from having toDo unnecessary run tyme checks.
Transcript
Play full episode
