4 ms·
Actually it's not that easy. Everywhere you have a type you need to proof that the expression really has the right type, and it's not just type annotation, it's
by solomatov 11y ago
Actually it's not that easy. Everywhere you have a type you need to proof that the expression really has the right type, and it's not just type annotation, it's a real mathematical proof.
To understand the complexity of the task, try proving that insertion sort is really a sort algorithm. You write more code, and writing it will take more time than you would do in a 'normal' typed language.
- serverholic 11y agoYou can choose how rigorous you want your proof to be. I'd highly recommend reading Chapter 1, Section 1.3 from Type-Driven Development. The first chapter is free. https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...