title: Curry-Howard isomorphism
body: <p>I've searched around the Internet, and I can't find any explanations of CHI which don't rapidly degenerate into a lecture on logic theory which is drastically over my head. (These people talk as if "intuitionistic proposition calculus" is a phrase that actually <em>means something</em> to normal humans!)</p>
  
  <p>Roughly put, CHI says that types are theorems, and programs are proofs of those theorems. But what the hell does that even <em>mean</em>??</p>
  
  <p>So far, I've figured this out:</p>
  
  <ul>
  <li><p>Consider <code>id :: x -&gt; x</code>. Its type says "given that X is true, we can conclude that X is true". Seems like a reasonable theorem to me.</p></li>
  <li><p>Now consider <code>foo :: x -&gt; y</code>. As any Haskell programmer will tell you, this is impossible. You cannot write this function. (Well, without cheating anyway.) Read as a theorem, it says "given that any X is true, we can conclude that any Y is true". This is obviously nonsense. And, sure enough, you cannot write this function.</p></li>
  <li><p>More generally, the function's arguments can be considered "this which are assumed to be true", and the result type can be considered "thing that is true assuming all the other things are". If there's a function argument, say <code>x -&gt; y</code>, we can take that as an assumption that X being true implies that Y must be true.</p></li>
  <li><p>For example, <code>(.) :: (y -&gt; z) -&gt; (x -&gt; y) -&gt; x -&gt; z</code> can be taken as "assuming that Y implies Z, that X implies Y, and that X is true, we can conclude that Z is true". Which seems logically sensible to me.</p></li>
  </ul>
  
  <p>Now, what the hell does <code>Int -&gt; Int</code> mean?? o_O</p>
  
  <p>The only sensible answer I can come up with is this: If you have a function X -> Y -> Z, then the type signature says "assuming that it's possible to construct a value of type X, and another of type Y, then it is possible to construct a value of type Z". And the function body describes exactly how you would do this.</p>
  
  <p>That seems to make sense, but it's not very <em>interesting</em>. So clearly there must be more to it than this...</p>