René
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.
Jon Sterling@liamoc Curry Howard Isomorphism — isomorphic in the sense of JavaScript (not sure if this meme still lives)
@jonmsterling because of the weird misuse of mathematical terminology I had assumed until right now that the JS runtime "deno" had some ridiculous nominal connection to denotational semantics but apparently it's just meant as an anagram of node.
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.
@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.
Guillaume Munch-Maccagnoni@liamoc Thanks for this write up ! It resonates with me. What is the Curry-Howard correspondence beyond a point of view taken in some research programmes, and how successful have those been? Your point about mathematical fetishism reminded me of Tomas Petricek's commentary about the "sociology of monads" in "What we talk about when we talk about monads" (https://arxiv.org/abs/1803.10195); he talks about the "romance of mathematics".
What we talk about when we talk about monads
Computer science provides an in-depth understanding of technical aspects of programming concepts, but if we want to understand how programming concepts evolve, how programmers think and talk about them and how they are used in practice, we need to consider a broader perspective that includes historical, philosophical and cognitive aspects. In this paper, we develop such broader understanding of monads, a programming concept that has an infamous formal definition, syntactic support in several programming languages and a reputation for being elegant and powerful, but also intimidating and difficult to grasp. This paper is not a monad tutorial. It will not tell you what a monad is. Instead, it helps you understand how computer scientists and programmers talk about monads and why they do so. To answer these questions, we review the history of monads in the context of programming and study the development through the perspectives of philosophy of science, philosophy of mathematics and cognitive sciences. More generally, we present a framework for understanding programming concepts that considers them at three levels: formal, metaphorical and implementation. We base such observations on established results about the scientific method and mathematical entities -- cognitive sciences suggest that the metaphors used when thinking about monads are more important than widely accepted, while philosophy of science explains how the research paradigm from which monads originate influences and restricts their use. Finally, we provide evidence for why a broader philosophical, sociological look at programming concepts should be of interest for programmers. It lets us understand programming concepts better and, fundamentally, choose more appropriate abstractions as illustrated in number of case studies that conclude the paper.
mb21@liamoc Seems the question “programs are proofs, yes, but proofs about what?.” wasn’t really answered? Or did I miss it somehow? Would love an example.
@mb21 it is; the answer is that they're proofs of abstract logical sentences in propositional or second-order logic.
@mb21 Viewed from a traditional logical lens, the types (32-bit) Int and Bool are both just true, albeit with 2^32 and 2 witnesses to that truth respectively. So, I guess, assuming true, we have true? It's a very pointless logical proposition to prove. The value of the type doesn't come from its logical interpretation here.
Robin Adams@robinadams @mb21 Right -- it's even a stretch to say that "Int" is a proof that there exists an integer, in the traditional sense (∃ x. x ∈ ℤ). Rather it is a true proposition with |ℤ| many different witnesses to its truth. The notion of something being an integer or a boolean doesn't exist in the logic.
@liamoc a related misconception happens when one adds Lambek to the correspondence. Then we also add a program logic to the calculus in questions in the form of a class of categorical models. Sometimes people conflate this with giving a denotational semantics to the language in question. It is, however, a separate activity. (One can give a denotational semantics that is not a categorical semantics, and one can give a categorical semantics that's not a useful denotational semantics, either because it mirrors the syntax too closely or because it doesn't have interesting models that aren't the syntax.)
@liamoc It took me a long while to understand this point, I think it was Neel Krishnaswami and @jonmsterling who (separately) taught me enough to notice.
Steph. Luis Rolland-Brabant ⁂@stphrolland @liamoc I mean something like this:
http://lmf.di.uminho.pt/quantum-logic-1920/LQ-Lec8.pdf
(One of the first hits Duck Duck Go gave me.)
@ohad @liamoc
I have just skimmed it... I saw no mention of the misconception you were mentionning.
My current understanding of the misconception about the Curry-Howard isomorphism: it is more meaningful if we use truncation so as to decouple a Type which implies an heavy machinery, versus a Truncation, which is only witnessing that the type is inhabited, and which is sufficient enough for Logic/Theorem Proving.
That's more or less what I understood from several statements I read from discussion between mathematicians like J. Carette and M. Escardo
From what I understand the paper you indicate is only establishing the Curry-Howard-Lambek correspondance.
I have not seen concerns about misconceptions around it.
Am I mistaken ?
I admit I am not yet fluent enough to understand fully the paper, I will have to re-read it and dig some parts. But I have not seen a passage about misconceptions induced by Lambek calculus.
@stphrolland @liamoc thanks, I didn't know if you wanted me to explain Lambek or what I meant in this nuance, and so just linked to the Lambek correspondence.
That's great. I have not worked enough on the concept.
I am interested because I have beginning of experiments where I put a layer that probably can be modeled with Lambek calculus. But for the moment, it is an additional/external layer. I am tempted to think there will be ways to connect the layers.
But I am not experienced enough to bet on the fact that I will not fall into misconceptions, of the kind you are highlighting.
That's why I am interested in case you remember papers dealing with them.
I only sort of "feel" the sort of decoupling you express between a categorical semantics and a denotational semantics. But I am not yet at ease.
I ask you more "by fear" of doing mistakes.
Nathan 🌻@liamoc I think the first time this clicked with me was when getting familiar with a proof assistant and getting practical intuition that proving a disjunction looks very similar to if then else in programming, so I do think it's useful to show a student coming from either direction that programming and theorem proving (specifically computer assisted theorem proving) are not that different deep down and it's not just by coincidence.
Besides giving you confidence that your skills can be partially transferred if you shift your reasoning mode a bit, I don't find much use for it.
I think one should also point out that non-computer assisted theorem proving has often very little to do with any practical programming, it seems a very different skill set. So maybe it's like drawing and writing, you can use pen and paper to do either but you won't learn much about doing one practicing the other.
Ashton Wiersdorf@liamoc a decent chunk of my blog posts stem from frustrating conversations. Thank you for writing yours up!
Apostolis@liamoc Imagine the damage they do, when someone then tries to approach the untyped community.
We have a bad reputation, let me tell you that, some for good reason.