4 ms·

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-ty

• allenguo 12y ago
  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 12y ago
    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.