[andrzejsz]

Although I am not expert on these things but it seems to me that Idris has better support for so called dependent types http://ejenk.com/blog/why-dependently-typed-programming-will...

[allenguo]

This was an interesting read. Thanks for sharing!

> This means that whenever I call this function, I need to provide together with a and b a proof that b isn’t zero.

What might such a proof look like? And is this supposed to work at compile-time?

[nbouscal]

Yes, it happens at compile time. To understand how proofs work here, you want to look at the Curry-Howard correspondence. Basically, there's a correspondence between types and propositions, and between the values inhabiting those types and proofs of the corresponding propositions. So a proof looks like a value of a certain type.