Types
Great overview article but I have a comment.<p>&gt; In Idris, we can say &quot;the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument&quot;:<p>&gt; If we try to call this function as add 2 1, where the first argument is larger than the second, then the compiler will reject the program at compile time.<p>&gt; Haskell has no equivalent of the Idris type above, and Go has no equivalent of either the Idris type or the Haskell type. As a result, Idris can prevent many bugs that Haskell can&#x27;t, and Haskell can prevent many bugs that Go can&#x27;t. In both cases, we need additional type system features, which make the language more complex.<p>I really wish when people talk about dependently typed programming languages (e.g. Idris, Coq, Agda, ATS), they would mention the effort involved to get these compile time checks to happen.<p>These languages allow you to capture almost any program property you can think of as a type. Instead of being limited to saying function F &quot;returns a number&#x2F;list&#x2F;string&quot; like common type systems, you can capture arbitrarily complex properties like &quot;F returns an even number&quot;, &quot;F returns a permutation of the input list&quot;, &quot;F always halts&quot; or &quot;F returns a proof of Fermat&#x27;s Last Theorem&quot;. You don&#x27;t get this for free and you have to help the computer verify these.<p>Proving F matches the type is arbitrary hard and is impossible to automated in general (e.g. the halting problem tells us we cannot always tell if a function halts). For example, consider the type &quot;F returns a sorted permutation of the input list&quot;, where F could be an implementation of bubble sort, quicksort, merge sort, radix sort or something even more complex. Each algorithm will require a different and potentially complex proof and most of the time the programmer needs to help the computer find the proof. It&#x27;s completely unlike what people are used to from type systems and is an even more massive leap than for someone moving from the type systems of e.g. C++&#x2F;Java to Haskell.<p>I&#x27;m glad people are more aware of dependently typed languages but I feel the immense jump in how practical they are to use is severely overlooked.