@@ -52,34 +52,37 @@ Curry-Howard correspondence
52So 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.
52So 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.
54The way that this works is that a proposition is a type so this,
54The way that this works is that a proposition is a type so this,
55− <table border="1">
55+
56− <tr>
56+.. code-block:: idris
57− <td><pre>Idris> 1+1=2
58+ 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+ 2 = 2 : Type
62is 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:
61is 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">
63+<table border="1">
65 <td><pre>Idris> 1+1=3
65 <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>
69Both 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.
70Both 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.
70A 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
71A 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">
73+<table border="1">
73 <td><pre>onePlusOne : 1+1=2
75 <td><pre>onePlusOne : 1+1=2
74onePlusOne = Refl</pre></td>
76onePlusOne = Refl</pre></td>
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>
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:
79.. code-block:: idris
82.. code-block:: idris
81 Idris> Refl
84 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
84So it must pattern match on its return type:
87So it must pattern match on its return type:
@@ -90,48 +93,24 @@ So it must pattern match on its return type:
91So now that we can represent propositions as types other aspects of propositional logic can also be translated to types as follows:
94So now that we can represent propositions as types other aspects of propositional logic can also be translated to types as follows:
93−<table border="1">
96++----------+-------------------+--------------------------+
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>
97+| | propositions | example of possible type |
98− </tr>
98++----------+-------------------+--------------------------+
100− <th bgcolor="#FFFF00" scope="row">A</th>
102− <td>x=y</td>
99+| A | x=y | |
103− </tr>
100++----------+-------------------+--------------------------+
105− <th bgcolor="#FFFF00" scope="row">B</th>
107− <td>y=z</td>
101+| B | y=z | |
108− </tr>
102++----------+-------------------+--------------------------+
110− <th bgcolor="#FFFF00" scope="row">and</th>
112− <td>Pair(x=y,y=z)</td>
103+| and | A /\ B | Pair(x=y,y=z) |
113− </tr>
104++----------+-------------------+--------------------------+
115− <th bgcolor="#FFFF00" scope="row">or</th>
117− <td>Either(x=y,y=z)</td>
105+| or | A \/ B | Either(x=y,y=z) |
118− </tr>
106++----------+-------------------+--------------------------+
119− <tr>
107+| implies | A -> B | (x=y) -> (y=x) |
120− <th bgcolor="#FFFF00" scope="row">implies</th>
108++----------+-------------------+--------------------------+
121− <td>A -> B</td>
109+| for all | y=z | |
122− <td>(x=y) -> (y=x)</td>
110++----------+-------------------+--------------------------+
123− </tr>
111+| exists | y=z | |
124− <tr>
112++----------+-------------------+--------------------------+
125− <th bgcolor="#FFFF00" scope="row">for all </th>
113+
130− <th bgcolor="#FFFF00" scope="row">exists</th>
136And (conjunction)
115And (conjunction)
137-----------------
116-----------------
@@ -190,7 +169,8 @@ Especially when working with equalities containing variable terms (inside functi
190 plusReducesR n = Refl
169 plusReducesR n = Refl
192plusReducesR gives the following error:
171plusReducesR gives the following error:
193− <table border="1">
173+<table border="1">
195 <td><pre>- + Errors (1)
175 <td><pre>- + Errors (1)
196 `-- proof.idr line 6 col 17:
176 `-- proof.idr line 6 col 17:
@@ -208,7 +188,7 @@ plusReducesR gives the following error:
209 plus n 0</pre></td>
189 plus n 0</pre></td>
211− </table>
191+</table>
213So why is 'Refl' able to prove some equality types but not others?
193So why is 'Refl' able to prove some equality types but not others?
@@ -221,7 +201,7 @@ So when we type 1+1 in Idris it is immediately converted to 2 because definition
221.. code-block:: idris
201.. code-block:: idris
223 Idris> 1+1
203 Idris> 1+1
224− 2</span> : Integer
204+ 2 : Integer
226In the following pages we discuss how to resolve propositionaly equalies.
206In the following pages we discuss how to resolve propositionaly equalies.