3
$\begingroup$

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?

$\endgroup$
  • 2
    $\begingroup$ 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. $\endgroup$ – Jake Oct 26 '14 at 0:33
  • $\begingroup$ Great - could you expand that into an answer? $\endgroup$ – hawkeye Oct 26 '14 at 9:59
  • $\begingroup$ 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)." $\endgroup$ – Giorgio Oct 26 '14 at 12:22
  • $\begingroup$ That is how to think about the type not the logical statement it corresponds to in Curry-Howard $\endgroup$ – Jake Oct 26 '14 at 17:34
  • 1
    $\begingroup$ This question is ill posed and it is not clear what is being asked. Furthermore, the accepted answer is misleading at best. $\endgroup$ – Andrej Bauer Oct 27 '14 at 7:38
-1
$\begingroup$

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.

$\endgroup$
  • 4
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Oct 27 '14 at 7:37
6
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ This is definitely the more interesting. I love that paper too! $\endgroup$ – Jake Oct 26 '14 at 20:03

Not the answer you're looking for? Browse other questions tagged or ask your own question.