User loginNavigation 
Relevance of CurryHowardHi there, I have read a lot about the CurryHoward isomorphism, but its relevance is not yet clear to me. I know there are experts on this topic here in this board, so please enlighten me :) Technically, I understand the relation between simplytyped lambda calculus and constructive logic and how the isomorphism between proofs and programs works. However, what does CurryHoward mean in general? Why is it significant? Does it say anything about a setting different from simplytyped lambda calculus/constructive logic? I understand that one interpretation of CH is this: If I have a function of type t > t', then the function body is a constructive proof that it is possible to construct a t' value from a t value. However, this "type inhabitation" question seems to have a trivial answer in almost any real programming language: You can construct a value/function for whatever type you want (e.g., in Haskell you can just use "undefined") I have never seen any type in a program that expresses an interesting, nontrivial proposition, but maybe I have not looked closely enough? Would it be possible to take an arbitrary mathematical theorem (let's say: "string concatenation is associative", or Fermat's little theorem) and express it as a type? I am also still a bit confused about conceptually viewing a type as a proposition. I think of types (of functions) as partial specifications, whereby the type checker checks conformance of the implementation to this partial specification. How does this fit together? By Klaus Ostermann at 20060601 23:25  LtU Forum  previous forum topic  next forum topic  other blogs  28906 reads

Browse archivesActive forum topics 
Recent comments
3 hours 18 min ago
4 hours 50 min ago
7 hours 54 min ago
8 hours 8 min ago
8 hours 26 min ago
9 hours 10 min ago
11 hours 27 min ago
12 hours 17 min ago
23 hours 28 min ago
1 day 2 hours ago