tag:blogger.com,1999:blog-29826497641915134892024-03-13T15:11:51.438-07:00joco42Unknownnoreply@blogger.comBlogger1125tag:blogger.com,1999:blog-2982649764191513489.post-33106266966189458032016-01-09T11:45:00.003-08:002016-01-10T00:40:58.157-08:00<br />
Idris Adventures - a nice surprise.<br />
<br />
Let's compare 3 examples.<br />
<br />
The following code compiles:<br />
<br />
<u>Example 1:</u><br />
<br />
<span style="font-family: Courier New, Courier, monospace;">data D :Nat-> Type where</span><br />
<span style="font-family: Courier New, Courier, monospace;"> MkD: (a:Nat)-> D a</span><br />
<span style="font-family: Courier New, Courier, monospace;"><br /></span>
<span style="font-family: Courier New, Courier, monospace;">showNat : (D a)->String</span><br />
<span style="font-family: Courier New, Courier, monospace;">showNat (MkD a) =show a</span><br />
<span style="font-family: Courier New, Courier, monospace;"><br /></span>
<span style="font-family: inherit;">but the following does NOT compile:</span><br />
<br />
<u>Example 2:</u><br />
<span style="font-family: inherit;"><br /></span>
<br />
<span style="font-family: Courier New, Courier, monospace;">data D :Nat-> Type where</span><br />
<span style="font-family: Courier New, Courier, monospace;"> MkD: (a:Nat)-> D a</span><br />
<span style="font-family: Courier New, Courier, monospace;"><br /></span>
<span style="font-family: Courier New, Courier, monospace;">showNat : (D a)->String</span><br />
<span style="font-family: Courier New, Courier, monospace;">showNat (MkD b) =show b</span><br />
<span style="font-family: Courier New, Courier, monospace;"><br /></span>
<span style="font-family: inherit;">why not ?</span><br />
<span style="font-family: inherit;"><br /></span>
Because the following DOES compile:<br />
<br />
<u>Example 3:</u><br />
<br />
<span style="font-family: Courier New, Courier, monospace;">data D :Nat-> Type where</span><br />
<span style="font-family: Courier New, Courier, monospace;"> MkD: (a:Nat)-> D Z</span><br />
<span style="font-family: Courier New, Courier, monospace;"><br /></span>
<span style="font-family: Courier New, Courier, monospace;">showNat : (D a)->String</span><br />
<span style="font-family: Courier New, Courier, monospace;">showNat (MkD c) =show c</span><br />
<span style="font-family: Courier New, Courier, monospace;"><br /></span>
<span style="font-family: inherit;">Why does Example 1 and 3 compile and 2 not ?</span><br />
<span style="font-family: inherit;"><br /></span>
<span style="font-family: inherit;">Because Idris knows in Example 2 that the parameter </span><span style="font-family: Courier New, Courier, monospace;">a</span><span style="font-family: inherit;"> is the </span><b style="font-family: inherit;">same</b><span style="font-family: inherit;"> in the type and in the value because of the </span>constraint given by the data constructor <span style="font-family: 'Courier New', Courier, monospace;">MkD:</span><span style="font-family: 'Courier New', Courier, monospace;"> </span><span style="font-family: 'Courier New', Courier, monospace;">(a:Nat)-> D a</span><span style="font-family: inherit;"> .</span><br />
<span style="font-family: inherit;"><br /></span>
<span style="font-family: inherit;"><br /></span>
<span style="font-family: inherit;">Cool !</span><br />
<span style="font-family: inherit;"><br /></span>
<span style="font-family: inherit;">--</span><br />
<span style="font-family: inherit;"><br /></span>
<span style="font-family: inherit;">UPDATE:</span><br />
<span style="font-family: inherit;"><br /></span>
<span style="font-family: inherit;">Perhaps this is a bug.... - to be confirmed.</span><br />
<span style="font-family: inherit;"><br /></span>
<span style="font-family: inherit;">because this :</span><br />
<span style="font-family: inherit;"><br /></span>
<span style="background-color: white; color: #333333; font-size: 15px; line-height: 17px; white-space: pre-wrap;"><span style="font-family: Courier New, Courier, monospace;">showD : D a -> String; </span></span><br />
<span style="background-color: white; color: #333333; font-size: 15px; line-height: 17px; white-space: pre-wrap;"><span style="font-family: Courier New, Courier, monospace;"> showD {a = x} (MkD x) = show x</span></span><br />
<span style="background-color: white; color: #333333; font-size: 15px; line-height: 17px; white-space: pre-wrap;"><span style="font-family: Courier New, Courier, monospace;"><br /></span></span>
<span style="font-family: Arial, Helvetica, sans-serif;"><br /></span>
<span style="color: #333333; font-family: Arial, Helvetica, sans-serif;"><span style="background-color: white; font-size: 15px; line-height: 17px; white-space: pre-wrap;">compiles too. </span></span><br />
<span style="color: #333333; font-family: Arial, Helvetica, sans-serif;"><span style="background-color: white; font-size: 15px; line-height: 17px; white-space: pre-wrap;"><br /></span></span>
<span style="color: #333333; font-family: Arial, Helvetica, sans-serif;"><span style="background-color: white; font-size: 15px; line-height: 17px; white-space: pre-wrap;">The { } means pattern match. It brings <b>a</b> into scope, from the type level to the value level and then assigns <b>a</b> to <b>x</b> (yes, that is a reverse assignment syntax).</span></span><br />
<span style="color: #333333; font-family: Arial, Helvetica, sans-serif;"><span style="background-color: white; font-size: 15px; line-height: 17px; white-space: pre-wrap;"><br /></span></span>
<span style="color: #333333; font-family: Arial, Helvetica, sans-serif;"><span style="background-color: white; font-size: 15px; line-height: 17px; white-space: pre-wrap;"><br /></span></span>Unknownnoreply@blogger.com0