<p>The type $\def\Nat{\mathrm{Nat}}\forall a b. (a,b) \rightarrow (b,a)$ corresponds to the logical statement $\forall a b : \mathrm{Prop}. a \land b \rightarrow b \land a$. $(a,b)$ corresponds to $a \land b$ and quantification over types corresponds to quantification over propositions (and of course implies corresponds to function types). This basically just expresses the fact that logical and is commutative. If you ask me this has nothing to do with a swap function even though the swap function has this type so I think your examples satisfies your question.</p>

<p>If you think about functions of types like $\Nat \rightarrow \Nat$ they <strike>correspond</strike> are logically equivalent to $\top \rightarrow \top$ (which is of course equivalent to $\top$). Why is $\Nat$ <strike>correspond</strike> logically equivlent to $\top$? Well inhabitants can be constructed of type $\Nat$ no matter the case which is a property only true of tautologies so $\Nat$ is a tautology. <strike>One could argue that $\Nat$ corresponds to something else that is a tautology (as mentioned $\Nat \to \Nat$ is also a tautology) but it is still equivalent to $\top$.</strike> As Andrej noted logically equivalent does not mean corresponds and I was wrong in saying this. Thinking about it now that would be like saying $\forall a b. (a, b) \to (b, a)$ corresponded to $\top$ which is clearly wrong.</p>

<p>Most programs have extremely boring types quite frankly. In Haskell the only real types of interest are are types involving forall, because the rest usually have some type like $\;\cdots\, \to A$, where $A$ is a trivial tautology (like a list type or a number). Languages like Agda and Coq can have far more interesting types if you are interested in this sort of thing.</p>

CC BY-SA 3.0
2014-10-27T07:37:39.783Z
It is false that $\mathbb{N}$ corresponds to $\top$. You are making the mistake of *ignoring proofs* and you are just looking at inhabitation. (That roughly corresponds to making everything proof irrelevant). Just because two types are both inhabited, that does not make them equal, nor does it mean they correspond to the same proposition. They may have the same *extension* (truth value), but they have *different meaning*.
Andrej Bauer
CC BY-SA 3.0
2014-10-26T17:43:45.657Z
2014-10-27T15:37:40.307Z
2014-10-27T15:37:40.307Z
Jake
<p>I'll answer the opposite question which is: </p>

<blockquote>
  <p><strong>can Curry-Howard prove a theorem for your program, which has nothing to do with the type</strong>? </p>
</blockquote>

<p>The answer is yes, depending on the meaning of "nothing to do". I'll leave the Curry-Howard aspect aside somewhat, but it underlies a lot of this approach. </p>

<p>The key idea is Wadlers' <strong><a href="http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf">Theorems for Free!</a></strong> building on ideas from Reynolds, which allow you, given a program type, to deduce <em>something</em> about the program. For example, a program $f$ of type</p>

<pre><code>(a, b) -&gt; (b, a)
</code></pre>

<p>in haskell <em>must</em> satify</p>

<p>$$ \forall x\ y,\ f\ (x, y) = (y, x)$$</p>

<p>and therefore be the <code>swap</code> function.</p>

CC BY-SA 3.0
2014-10-26T20:03:02.037Z
This is definitely the more interesting. I love that paper too!
Jake
CC BY-SA 3.0
2014-10-26T19:09:06.117Z
2014-10-26T19:09:06.117Z
cody
<p>The <a href="https://news.ycombinator.com/item?id=8457761" rel="nofollow">following link states</a>:</p>

<blockquote>
  <p>Curry-Howard means that any type can be interpreted as a theorem in some logical system, and any term can be interpreted as a proof of its type.
  This does not mean that those theorems have anything to do with your program. Take the following function:</p>
</blockquote>

<pre><code>swap : forall a,b. (a,b) -&gt; (b,a)
swap pair = (snd pair, fst pair)
</code></pre>

<blockquote>
  <p>The type here is forall a,b. (a,b) -> (b,a). The logical meaning of this type is (a and b) => (b and a). Note that this is a theorem in logic, not a theorem about your program.</p>
</blockquote>

<p>My question is: <strong>Can Howard-Curry prove a theorem from the types in your program, that has nothing to do with your program?</strong></p>

CC BY-SA 3.0
2014-10-26T00:33:48.190Z
I mean frankly what does (a & b) -> (b & a) (commutativity of and) have to do with a swap function? I'd say your example already shows just this. If you think about a lot of functions we write like functions of type Nat -> Nat or Double -> Double. These all effectively just say that true implies true because we can provide constructions of them without anything else just like unit (true). Many functions have very uninteresting types frankly.
Jake
CC BY-SA 3.0
2014-10-26T09:59:49.310Z
Great - could you expand that into an answer?
hawkeye
CC BY-SA 3.0
2014-10-26T12:22:10.853Z
I always thought that the theorem proved by a type `Nat -> Nat` was: "Each time you provide a natural number as input to this function, you will get a natural number as result (instead of, say, a string)."
Giorgio
CC BY-SA 3.0
2014-10-26T17:34:19.120Z
That is how to think about the type not the logical statement it corresponds to in Curry-Howard
Jake
CC BY-SA 3.0
2014-10-27T07:38:22.647Z
This question is ill posed and it is not clear what is being asked. Furthermore, the accepted answer is misleading at best.
Andrej Bauer
<type-theory><curry-howard>
Can Curry-Howard prove a theorem from the types in your program, that has nothing to do with your program?
hawkeye
# Can Curry-Howard prove a theorem from the types in your program, that has nothing to do with your program?

(Asked by: username_0 on 2014-10-25)

The following link states:

Curry-Howard means that any type can be interpreted as a theorem in some logical system, and any term can be interpreted as a proof of its type.
  This does not mean that those theorems have anything to do with your program. Take the following function:

swap : forall a,b. (a,b) -> (b,a)
swap pair = (snd pair, fst pair)


The type here is forall a,b. (a,b) -> (b,a). The logical meaning of this type is (a and b) => (b and a). Note that this is a theorem in logic, not a theorem about your program.

My question is: Can Howard-Curry prove a theorem from the types in your program, that has nothing to do with your program?

**Tags:** type-theory, curry-howard

> **Comments:**
> **username_1**: I mean frankly what does (a & b) -> (b & a) (commutativity of and) have to do with a swap function? I'd say your example already shows just this. If you think about a lot of functions we write like functions of type Nat -> Nat or Double -> Double. These all effectively just say that true implies true because we can provide constructions of them without anything else just like unit (true). Many functions have very uninteresting types frankly.  
> **username_0**: Great - could you expand that into an answer?  
> **username_2**: I always thought that the theorem proved by a type `Nat -> Nat` was: "Each time you provide a natural number as input to this function, you will get a natural number as result (instead of, say, a string)."  
> **username_1**: That is how to think about the type not the logical statement it corresponds to in Curry-Howard  
> **username_3**: This question is ill posed and it is not clear what is being asked. Furthermore, the accepted answer is misleading at best.  

---

## 2 answers

### Answer by username_1 on 2014-10-26. Score: -1 | Accepted answer

The type $\def\Nat{\mathrm{Nat}}\forall a b. (a,b) \rightarrow (b,a)$ corresponds to the logical statement $\forall a b : \mathrm{Prop}. a \land b \rightarrow b \land a$. $(a,b)$ corresponds to $a \land b$ and quantification over types corresponds to quantification over propositions (and of course implies corresponds to function types). This basically just expresses the fact that logical and is commutative. If you ask me this has nothing to do with a swap function even though the swap function has this type so I think your examples satisfies your question.

If you think about functions of types like $\Nat \rightarrow \Nat$ they correspond are logically equivalent to $\top \rightarrow \top$ (which is of course equivalent to $\top$). Why is $\Nat$ correspond logically equivlent to $\top$? Well inhabitants can be constructed of type $\Nat$ no matter the case which is a property only true of tautologies so $\Nat$ is a tautology. One could argue that $\Nat$ corresponds to something else that is a tautology (as mentioned $\Nat \to \Nat$ is also a tautology) but it is still equivalent to $\top$. As Andrej noted logically equivalent does not mean corresponds and I was wrong in saying this. Thinking about it now that would be like saying $\forall a b. (a, b) \to (b, a)$ corresponded to $\top$ which is clearly wrong.

Most programs have extremely boring types quite frankly. In Haskell the only real types of interest are are types involving forall, because the rest usually have some type like $\;\cdots\, \to A$, where $A$ is a trivial tautology (like a list type or a number). Languages like Agda and Coq can have far more interesting types if you are interested in this sort of thing.

> **Comments:**
> **username_3**: It is false that $\mathbb{N}$ corresponds to $\top$. You are making the mistake of *ignoring proofs* and you are just looking at inhabitation. (That roughly corresponds to making everything proof irrelevant). Just because two types are both inhabited, that does not make them equal, nor does it mean they correspond to the same proposition. They may have the same *extension* (truth value), but they have *different meaning*.  

---

### Answer by username_4 on 2014-10-26. Score: 6

I'll answer the opposite question which is: 

can Curry-Howard prove a theorem for your program, which has nothing to do with the type? 

The answer is yes, depending on the meaning of "nothing to do". I'll leave the Curry-Howard aspect aside somewhat, but it underlies a lot of this approach. 
The key idea is Wadlers' Theorems for Free! building on ideas from Reynolds, which allow you, given a program type, to deduce something about the program. For example, a program $f$ of type
(a, b) -> (b, a)

in haskell must satify
$$ \forall x\ y,\ f\ (x, y) = (y, x)$$
and therefore be the swap function.

> **Comments:**
> **username_1**: This is definitely the more interesting. I love that paper too!  

---

