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.
@pablogician @liamoc @jer_gib well, the kind of meta-level reasoning you’re doing — “can be the type only of composition” — requires parametricity reasoning, not props as types (as liam points out). but perhaps when there *is* a nice parametricity property, thinking about writing a proof for the corresponding proposition is a good way to wind up with the right code
@chrisamaphone @pablogician @liamoc Right. "How can I construct that output from these inputs?" That feels to me closer to "How can I prove that conclusion from these premisses?" than to anything about parametricity.
@jer_gib @chrisamaphone @pablogician I think if your prior knowledge is how to prove things, and you now want to learn how to construct programs, you might be using C-H thinking to map one skill to the other. But for most programmers, "How can I construct that output from these inputs?" doesn't require first mapping that question to "How can I prove that conclusion from these premises?".
@liamoc @jer_gib @chrisamaphone That's like saying that it is of no use to a mathematician to learn programming in order to build intuition on how to build (constructive) proofs. While it may not be strictly necessary, I still think it can clarify a lot of concepts. It is always instructive to understand a subject from various viewpoints, especially when the connection between these viewpoints is not obvious or well known.