<story><title>Idris, a language that will change the way you think about programming (2015)</title><url>http://crufter.com/2015/01/01/idris-a-language-which-will-change-the-way-you-think-about-programming/</url></story><parent_chain><item><author>vosper</author><text>As a Python programmer who doesn&amp;#x27;t understand this notation - what am I looking at, and what&amp;#x27;s amazing about it?</text></item><item><author>bojo</author><text>&lt;p&gt;&lt;pre&gt;&lt;code&gt;    app : Vect n a -&amp;gt; Vect m a -&amp;gt; Vect (n + m) a
&lt;/code&gt;&lt;/pre&gt;
That is pretty amazing if you ask me.  I look forward to the day when we all use languages which save programmers from themselves.</text></item></parent_chain><comment><author>badsock</author><text>The &amp;quot;Vector m a&amp;quot; means that it&amp;#x27;s a vector (like a Python list) that can only be m elements long, and those elements can only be of type a.  E.g. &amp;quot;Vector 3 Int&amp;quot; will always be a Vector with three integers in it.  If you try to treat it like a vector of any other length it will refuse to compile (e.g. pass it to a function that requires that it have 4 or more elements).&lt;p&gt;The whole line is the type declaration for a function (app) that takes a Vector of length m, and a Vector of length n, and produces a Vector of length (m+n).  Which is to say, the compiler knows at compile time what length the resulting Vector will be, and will fail to compile if the function you&amp;#x27;ve written doesn&amp;#x27;t - provably - always meet that requirement.&lt;p&gt;From a Haskeller&amp;#x27;s perspective it&amp;#x27;s amazing because container types are famous loopholes for code that produces runtime errors.  For instance, if you call the &amp;quot;head&amp;quot; function (returns the first element) on an empty list it will halt the program at run time with an error, despite the fact that it passed the type check (because an empty list and a full one have the same type).&lt;p&gt;As someone who learned Haskell and subsequently have been writing a lot of Python, I keep a mental tally of how many of my bugs (some of which took ages to track down) would have been caught immediately by a type system like Haskell or Idris&amp;#x27;.  I&amp;#x27;d say it&amp;#x27;s well over half.&lt;p&gt;In Haskell those kind of errors are drastically reduced, but a few still slip through.  Languages like Idris can catch even more of them, in a clever way, which is awesome.</text></comment>
<story><title>Idris, a language that will change the way you think about programming (2015)</title><url>http://crufter.com/2015/01/01/idris-a-language-which-will-change-the-way-you-think-about-programming/</url></story><parent_chain><item><author>vosper</author><text>As a Python programmer who doesn&amp;#x27;t understand this notation - what am I looking at, and what&amp;#x27;s amazing about it?</text></item><item><author>bojo</author><text>&lt;p&gt;&lt;pre&gt;&lt;code&gt;    app : Vect n a -&amp;gt; Vect m a -&amp;gt; Vect (n + m) a
&lt;/code&gt;&lt;/pre&gt;
That is pretty amazing if you ask me.  I look forward to the day when we all use languages which save programmers from themselves.</text></item></parent_chain><comment><author>tunesmith</author><text>You have two parameters - a vector of size &amp;quot;m&amp;quot;, and a vector of size &amp;quot;n&amp;quot;.  The function signature then expects to get back a vector of size &amp;quot;m + n&amp;quot;.&lt;p&gt;Contrast that with a language with method signatures that can only return types like &amp;quot;Vector&amp;quot; or &amp;quot;List&amp;quot;, without any information that is dependent on the incoming parameters.&lt;p&gt;So then, the logic is checked - if the method returns a vector that is anything other than the size of the two incoming parameter vector sizes added together, it won&amp;#x27;t compile.&lt;p&gt;In other words, even more behavior that would normally be a runtime bug is checked at compile time, which is a good thing if you are working in a domain where correctness is important and want to avoid runtime bugs.</text></comment>