<story><title>Types</title><url>https://gist.github.com/garybernhardt/122909856b570c5c457a6cd674795a9c?</url></story><parent_chain><item><author>twblalock</author><text>The Idris example seems to need further explanation:&lt;p&gt;&amp;gt; In Idris, we can say &amp;quot;the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument&amp;quot;:&lt;p&gt;&amp;gt; add : (x : Nat) -&amp;gt; (y : Nat) -&amp;gt; {auto smaller : LT x y} -&amp;gt; Nat&lt;p&gt;&amp;gt; add x y = x + y&lt;p&gt;That&amp;#x27;s all well and good, if you know the values of x and y at compile time. Consider a program that reads x and y from STDIN. The user could provide an x that is equal to or larger than y (or could provide only one value, or values that are not numbers). I see no way to deal with that except to throw a runtime error. Is that what would happen?</text></item></parent_chain><comment><author>_ibu9</author><text>The missing explanation is that `smaller` is a third argument to the function. It&amp;#x27;s type is a proof that x &amp;lt;= y. Since it is in curly brackets with the auto keyword, the compiler will fill in this proof in many cases, like when the values are statically known.&lt;p&gt;In the case where the values are read from the external environment, first you would have to compare them before calling the function. The comparator would return either a proof that x &amp;lt;= y, or x &amp;gt; y. In the first case you plug that value into the `smaller` argument, in the second case it&amp;#x27;s your responsibility to signal whatever kind of application-specific error is appropriate (assuming x &amp;gt; y is some kind of erroneous condition).</text></comment>
<story><title>Types</title><url>https://gist.github.com/garybernhardt/122909856b570c5c457a6cd674795a9c?</url></story><parent_chain><item><author>twblalock</author><text>The Idris example seems to need further explanation:&lt;p&gt;&amp;gt; In Idris, we can say &amp;quot;the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument&amp;quot;:&lt;p&gt;&amp;gt; add : (x : Nat) -&amp;gt; (y : Nat) -&amp;gt; {auto smaller : LT x y} -&amp;gt; Nat&lt;p&gt;&amp;gt; add x y = x + y&lt;p&gt;That&amp;#x27;s all well and good, if you know the values of x and y at compile time. Consider a program that reads x and y from STDIN. The user could provide an x that is equal to or larger than y (or could provide only one value, or values that are not numbers). I see no way to deal with that except to throw a runtime error. Is that what would happen?</text></item></parent_chain><comment><author>platz</author><text>not in idris, because it would force you to do that check manually and pass in the evidence as proof.  it has a bunch of tools to help you do this.. namely lifting values into types with &amp;#x27;dependent pairs&amp;#x27;.  idris doesnt automagically  calculate everything for you, but makes sure at compile time, that you provide evidence at run time for the things you have asserted in the types.  it makes more sense after going through some of the tutorials and books.</text></comment>