I'm surprised I haven't published it before. Type-Driven Dev | ITGram

I'm surprised I haven't published it before. Type-Driven Development in Idris is a great talk from Edwin Brady, the creator of Idris language, about, well, Idris.

Idris is a language with the best type system out there. Brady has other newer talks about Idris 2, a new more powerful version of Idris, so from the point of view of semantics this talk is a bit outdated. It was published 7 years ago! But I still think this is the best one because I want you to learn not Idris but the fundamental ideas behind it.

The Idris type system has a few very powerful features that your language, most likely, doesn't:

+ Higher-kinded types: you can write functions that operate with types as values.
+ Refined types: you can use very specific types, like "non-empty list", "even integer", "positive number", "hexadeciaml string", etc.
+ Dependent types: you can call functions from type annotations, so some types will be generated depending on types and values of other arguments. A classic example is printf function in C-like languages (or str.format in Python) where the types and amount of arguments depend on the template you pass as the first argument. For instance, if you pass "%s has %d messages", the function needs exactly 2 more arguments, and the first one must have type String and the second one must have type Integer. If you pass wrong arguments, most of the languages (I know for sure it's true for C and Go) will fail at runtime, unless you use a linter. In Idris, the error will be correctly detected at compilation time.

I watched this talk about 3 years ago when type annotations in Python were quite new thing for me and for the most of the Python community. And it changed how I think about types and static analysis in general. Showed, how cool and powerful it all might be. It inspired me to bring more static analysis into deal, including a basic formal verification.

There is my advice. Doesn't matter which language you write on, run all static analysis you can. It's almost free. Writing type annotations for everything is no-brainer, you know what type your function expects and returns anyway. And more you write annotations, cleaner they will be, because you start to think about your code in a more structured, "type-safe" manner. And good linters, even if they have false-positives, it happens not so often and usually indicates that your code is over-complicated and too magical anyway. I happened to meet multiple times engineers that were "smarter than linters", and no, they were not.

#idris