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  32111 reads

Browse archivesActive forum topics 
Recent comments
2 days 5 hours ago
1 week 1 day ago
1 week 5 days ago
2 weeks 5 days ago
3 weeks 11 hours ago
3 weeks 11 hours ago
3 weeks 15 hours ago
4 weeks 11 hours ago
4 weeks 4 days ago
4 weeks 5 days ago