Liam O'ConnorI had an extremely frustrating exchange with a FP practitioner who was overly enthusiastic about Curry-Howard the other day, so I tried to write up my thoughts in this note here.
Pablo Donato@liamoc I feel this blog post might give the wrong impression that the Curry-Howard correspondence is just a fun curiosity, but that most concepts of interests (e.g. type safety, type isomorphism, etc) can only be stated in type-theoretical parlance. This is not the case, because the correspondence is not only at the static levels of type/propositions and programs/proofs, but also at the *dynamic* level of execution/cut-elimination (this is also why I am usually reluctant to add Lambek to the correspondence's name). Thus it really is an isomorphism, that is no abuse of language.
Of course this does not invalidate your thesis that currently, having deep knowledge of Curry-Howard doesn't bring much practical benefit to software engineers. I agree that it becomes really useful in the presence of dependent types, but I still think more people should be exposed to Curry-Howard as a way of thinking about types, seen as a way to express and enforce your code's logic (literally) declaratively. At least when I was learning FP, it was eye-opening to me to understand that e.g. sum types are just a way to encode disjunction/case reasoning.
chris martens@pablogician @liamoc as someone who has always found logic more intuitive than programming, i agree with this - especially programming with continuations :)
Jeremy Gibbons@chrisamaphone @pablogician @liamoc I also think @liamoc is maybe being a bit harsh. You can drive a lot of benefit in plain ordinary FP from seeing how the types mean that your components will fit together in only one way. I'm thinking in particular of tricky data structure dissections, such as zippers, or tree manipulation. These exploit the same kind of insight as that (b->c)->(a->b)->a->c can be the type only of composition, or (a->b)*a -> b of application. Those are C-H correspondences, of transitivity of implication and of modus ponens respectively. They are the types whose inhabitants Agda can write for you, but you don't need to be using dependent types to get at least some of the benefit.
@jer_gib @chrisamaphone @pablogician They "have" C-H correspondences, as does basically everything -- But none of this reasoning comes from props as types unless you are trying to map prior experience in writing proofs (which most programmers lack) into construction of programs.
@liamoc @chrisamaphone @pablogician Then I don't think I understand what it is that the enthusiasts you've been talking to believe that C-H gives them.
@jer_gib @chrisamaphone @pablogician Mostly I see a conflation of theorems about programs obtained from type safety or parametricity with theorems obtained via C-H.
@jer_gib @chrisamaphone @pablogician But this is something I figured out only after many minutes of frustrating back-and-forth. Because my interlocutor had a *very* muddled understanding in the first place, and was clearly done an educational disservice at some point.
@liamoc @jer_gib @chrisamaphone Okay I see your point @liamoc. For me CH should be seen as a dictionary allowing bidirectional translation between two domains of study (PLT and proof theory), not as a technique to prove (meta-)theorems. Of course one way to get results in PLT is to first get the equivalent result in proof theory and then translate (and vice-versa).
@pablogician @jer_gib @chrisamaphone That is of course a valid method, and I would advocate understanding C-H for someone learning about PLT or proofs, even if they're just doing it out of curiosity --- there's nothing wrong with that. But when I hear people saying that understanding C-H is important for programming practice, which is an oft-repeated claim among the non-academic FP community, I cringe a little, because such misconceptions as I describe in my post are almost certainly the root of such a claim.