You have now entered the realm of Jawaninja.
Do not panic!
Only friendly geekiness around here. Mostly about Clojure, music and other interests of mine.
Idris is a one of those programming languages that empowers its users with the possibility to express very strong guarantees about the code they write before running it. It does this by using something called “Dependent Typing”, which is a very expressive kind of type system.
One of the guarantees you can get is to have safe arithmetic with
natural numbers (0, 1, 2, 3…). The interesting bit with Natural
numbers is that they cannot be negative, so the substraction
a - b
only works if
b ≤ a. Idris actually forces you to make sure of that
before trying to run your code.
I love Clojure and I love Haskell. Those are two of my favourite languages (I also really love Idris). They both offer semantics with very interesting properties and trade-offs.
Sadly there is a disconnect between the communities in both of those languages, where people try to communicate what they like about their favourite language but tend to do that by contrasting it with other languages, and that ends up being quite antagonistic and put people on the defensive.
This is my current intuition on types. I heard the best way to get feedback on the internet is to publish something inaccurate, so there you have it.
This post marks the dawn of yet another attempt at blogging.