@@ -52,34 +52,37 @@ Curry-Howard correspondence
5252So how to we relate these proofs to Idris programs? It turns out that there is a correspondence between constructive logic and type theory. They are the same structure and we can switch backward and forward between the two notations because they are the same thing.
5353
5454The way that this works is that a proposition is a type so this,
55− <table border="1">
56− <tr>
57− <td><pre>Idris> 1+1=2
58−<span class="style1">2</span> <span class="style2">=</span> <span class="style1">2</span> : <span class="style2">Type</span>
59−</pre></td>
60− </tr>
61− </table>
55+
56+.. code-block:: idris
57+
58+ Idris> 1+1=2
59+ 2 = 2 : Type
60+
6261is a proposition and it is also a type. This is built into Idris so when an '=' equals sign appears in a function type an equality type is generated. The following will also produce an equality type:
63− <table border="1">
62+
63+<table border="1">
6464 <tr>
6565 <td><pre>Idris> 1+1=3
66−<span class="style1">2</span> <span class="style2">=</span> <span class="style1">3</span> : <span class="style2">Type</span></pre></td>
66+<span class="style1">2 = <span class="style1">3 : Type</pre></td>
6767 </tr>
68− </table>
68+</table>
69+
6970Both of these are valid propositions so both are valid equality types. But how do we represent true judgment, that is, how do we denote 1+1=2 is true but not 1+1=3.
7071A type that is true is inhabited, that is, it can be constructed. An equality type has only on constructor 'Refl' so a proof of 1+1=2 is
71− <table border="1">
72+
73+<table border="1">
7274 <tr>
7375 <td><pre>onePlusOne : 1+1=2
7476onePlusOne = Refl</pre></td>
7577 </tr>
76− </table>
77− <p>So how can Refl, which is a constructor without any parameters, construct and equality type? If we type it on its own then it can't: </p>
78+</table>
79+
80+So how can Refl, which is a constructor without any parameters, construct and equality type? If we type it on its own then it can't:
7881
7982.. code-block:: idris
8083
8184 Idris> Refl
82− (input):Can't infer argument A to <span class="style1">Refl</span>, Can't infer argument x to <span class="style1">Refl</span>
85+ (input):Can't infer argument A to <span class="style1">Refl, Can't infer argument x to <span class="style1">Refl
8386
8487So it must pattern match on its return type:
8588
@@ -90,48 +93,24 @@ So it must pattern match on its return type:
9093
9194So now that we can represent propositions as types other aspects of propositional logic can also be translated to types as follows:
9295
93−<table border="1">
94− <tr>
95− <th bgcolor="#FFFF00" scope="col"> </th>
96− <th bgcolor="#FFFF00" scope="col">propositions</th>
97− <th bgcolor="#FFFF00" scope="col"> example of possible type</th>
98− </tr>
99− <tr>
100− <th bgcolor="#FFFF00" scope="row">A</th>
101− <td>A</td>
102− <td>x=y</td>
103− </tr>
104− <tr>
105− <th bgcolor="#FFFF00" scope="row">B</th>
106− <td>B</td>
107− <td>y=z</td>
108− </tr>
109− <tr>
110− <th bgcolor="#FFFF00" scope="row">and</th>
111− <td>A /\ B </td>
112− <td>Pair(x=y,y=z)</td>
113− </tr>
114− <tr>
115− <th bgcolor="#FFFF00" scope="row">or</th>
116− <td>A \/ B</td>
117− <td>Either(x=y,y=z)</td>
118− </tr>
119− <tr>
120− <th bgcolor="#FFFF00" scope="row">implies</th>
121− <td>A -> B</td>
122− <td>(x=y) -> (y=x)</td>
123− </tr>
124− <tr>
125− <th bgcolor="#FFFF00" scope="row">for all </th>
126− <td> </td>
127− <td> </td>
128− </tr>
129− <tr>
130− <th bgcolor="#FFFF00" scope="row">exists</th>
131− <td> </td>
132− <td> </td>
133− </tr>
134− </table>
96++----------+-------------------+--------------------------+
97+| | propositions | example of possible type |
98++----------+-------------------+--------------------------+
99+| A | x=y | |
100++----------+-------------------+--------------------------+
101+| B | y=z | |
102++----------+-------------------+--------------------------+
103+| and | A /\ B | Pair(x=y,y=z) |
104++----------+-------------------+--------------------------+
105+| or | A \/ B | Either(x=y,y=z) |
106++----------+-------------------+--------------------------+
107+| implies | A -> B | (x=y) -> (y=x) |
108++----------+-------------------+--------------------------+
109+| for all | y=z | |
110++----------+-------------------+--------------------------+
111+| exists | y=z | |
112++----------+-------------------+--------------------------+
113+
135114
136115And (conjunction)
137116-----------------
@@ -190,7 +169,8 @@ Especially when working with equalities containing variable terms (inside functi
190169 plusReducesR n = Refl
191170
192171plusReducesR gives the following error:
193− <table border="1">
172+
173+<table border="1">
194174 <tr>
195175 <td><pre>- + Errors (1)
196176 `-- proof.idr line 6 col 17:
@@ -208,7 +188,7 @@ plusReducesR gives the following error:
208188 and
209189 plus n 0</pre></td>
210190 </tr>
211− </table>
191+</table>
212192
213193So why is 'Refl' able to prove some equality types but not others?
214194
@@ -221,7 +201,7 @@ So when we type 1+1 in Idris it is immediately converted to 2 because definition
221201.. code-block:: idris
222202
223203 Idris> 1+1
224− 2</span> : Integer
204+ 2 : Integer
225205
226206In the following pages we discuss how to resolve propositionaly equalies.
227207