Against Curry-Howard Mysticism
28 points by LesleyLai
28 points by LesleyLai
My rule of thumb is “show me a problem without mentioning the theory, then show me how the theory solves it.”
This can be used both as a challenge to an entire theory (“does this theory do anything?”) and to specific explanations (“does this explanation show why this theory matters?”)
Not the specific topic at hand, but related: a lot of discussions of category theory fail on the second point. They show some code, they show some category theory, but they do not show how the category theory generates insight about the code.
I thought the use of category theory in this article on Diffie-Hellman was interesting, in particular this bit:
I mean, it will be a set in any practical situation, but we can pretend that we don’t know that, for some really, really cool math. And you should always pretend that you don’t know something when it leads to some really, really cool math.
An analogous thing happened with the application of category theory to functional programming in the late 1980s when it was found that if you pretend you don’t know the specifics of certain types then the same kinds of higher-order functions keep turning up, and these kinds of functions correspond to certain categories. So functional programming gained a whole collection of off-the-shelf structures that are known to work well together.
The problem with abstract nonsense is that if you pretend you know hardly anything about what is going on, it’s hard to say anything practically useful. Examples are crucial for gaining intuition, but for very abstract things the examples can seem trivial. The value of the abstraction comes from spotting rules that are useful to follow in lots of situations. The insight comes from seeing the same structure again and again. Whether the abstraction is better than the trivial implementation is another question! It helps if the vocabulary of little connectives doesn’t sprawl too much: APL does better than Rust, for instance.
Wrt type theory, it’s clearly useful for mechanizing mathematics and proofs of correctness in software, but the vast majority of programmers aren’t doing those things. It’s sad that all the Turing-complete type systems in mainstream languages are so ad-hoc: I’d love to see more machine-oriented dependently-typed languages. (Is ATS the only one?) Like, take the type-theory 101 example of a sized vector, and apply that to actual arrays (instead of linked lists in trenchcoats). Use range types with control-flow-aware type refinement (as in TypeScript) to eliminate hidden bounds checks. That kind of thing.
Wrt. machine-oriented dependently-typed languages:
Futhark has (a very limited form of) dependent types for exactly the use-case you mention: size types. It’s a joy to work with.
To the abstract nonsense point, any results from category theory can be proven in a specific setting, obviously. But abstraction can show us that 1) the specifics don’t actually matter for this particular results, clarifying the proof and 2) you might be able to apply the “trivial” abstract results to a category where nobody thought about it before and see what happens.
In my opinion, is more important.
It’s interesting that many of those bounds checks are elided or hoisted by the compiler. Yet we can’t “see” it with our dev tooling as it’s usually quite late in the process (eg LLVM might do it…).
For programming and software engineering practice, Curry-Howard is of essentially no practical benefit, unless you are using a dependently-typed language.
You don’t really need full dependent types, the Curry-Howard correspondence is readily applicable in Haskell where you have purity, parametricity and higher rank polymorphism. The most straightforward demonstration of this is Ghosts of Departed Proofs. But you don’t have to go full Ghosts of Departed Proofs all the time either, you will find nuggets of Curry-Howard correspondence scattered throughout Haskell codebases.
So, no, the programming community decided to settle on languages where nothing theoretically interesting can be applied directly at the type level, but if you decide to use Haskell, you can use the Curry-Howard correspondence for asserting theorems about every day business logic.
Ducks in anticipation of the pointless “bottom” and unsafePerformIO arguments, which actually don’t have any practical relevance
I didn’t quite understand how the Ghosts of Departed Proofs is an exception to the point the author makes in Section 1
If
balanceis the only way to produce aBalancedTree, then one might be tempted to say that this type “corresponds” to a proposition that a tree is balanced. But this is not a theorem that follows from formulae-as-types but rather from good ol’ type safety and enforcement of module boundaries, just as above.
In their first example (sorting a list), could you explain what the logical proposition used is? I would guess that maybe the Rank 2 polymorphism is important to the proposition, but I am having a hard time understanding how they are encoding a proof of sortedness. From my brief skim, it feels more like the use of higher rank polymorphism is a trick to prevent a user from violating the API (as illustrated in their newtype example without Rank 2 polymorphsim).
Is the point of Ghosts of Departed Proofs that you don’t strictly need a proof in types of the sortedness proposition, but rather a proof that you used the sortBy function before mergeBy (which I will add appears only provable by an invariant I don’t seen manifest in the types: namely that the constructor of the SortedBy is not exported)? If that’s the case, I don’t really see how it’s very different from the author’s point.
You also need all programs to terminate, or else you can prove arbitrary things:
data Bottom -- has no constructors
prove_false :: () -> Bottom
prove_false () = prove_false ()
Great article! I like reading reasoned arguments that push back against the ‘received wisdoms’ in certain FP-heavy areas of programming. This, along with ‘Only pure FP is real FP’, and ‘Monads are important to learn’, are some of my pet peeves from thought leaders in this space.
Don’t get me wrong, Curry-Howard is very cool, but when was the last time any of us applied it in our quotidian industrial programming jobs?
The success of Rust has shown programmers really can handle some complexity at the type level, given the right conditions of hype, poor alternatives, and compelling syntax (personally, I found rust to be the most difficult thing I learned in years). So always there will be this dialectic of bringing people up to the level of a programming language vs. pushing the boundaries of language capabilities where people are at. This exists within each language design; designers have a novelty budget dependent on the current state of general programmer knowledge, and they ignore this budget at the peril of rendering their language obscure & irrelevant.
Probably FP can be accused of neglecting the second part of the dialectic and focusing too much on bringing people up to the level of the language. Since educating people is very expensive, this results in lack of quotidian industry uptake. However, I think FP can readily argue that its best features it has been using for decades are only now making their way into mainstream languages. Variants & pattern matching are mainstream now, and programmers aren’t going back.
Whether monads will ever go mainstream is yet to be decided. When I learned them it seemed like an interesting generalization of map/filter/fold/iterate all bundled into one abstract thing. Programmers have been broadly acquainted with map/filter/fold for over a decade now, so maybe the time for a new conceptual leap is nigh.
I like to see posts like this because I often feel like I can’t tell the difference between BS and a point I’m missing.
Can we get one for questions like “Isn’t XYZ (Undecidable|NP-Complete|PSPACE-Complete)?” I definitely was one of these people who thought I had discovered some amazing gotcha. Now that I am a little wiser, I recall someone’s words of wisdom to me in response to that question, “Everything interesting that we do in PL is undecidable.”
Yeah! Usually the interesting thing is how we choose to restrict our problem to recover decidability. For example, “isn’t type inference for higher rank/dependent types undecidable?” commonly parroted by people when we talk about implementing these kinds of type systems. Yes, they are if you want to retain the principle types property (i.e. where every term in the language has a single most-general type). You can recover decidability if you choose to give up this property and allow programmers to supply type annotations to resolve ambiguities (see bidirectional typing).
This inspired me to write an undecidability explainer, hope you like it!
I’m flattered and I did like the explainer.
Although I kind of like the direction you took for your NP-Complete explainer better, which I think still applies to undecidable problems.
Like your quick takeaway is:
- We will have to spend time and mental effort to determine if it has P
- We may not be successful.
I’m not sure that undecidable problems necessarily require a lot of time and mental effort to determine (or at least, any more than other problems). To me, there is only one caveat to undecidability: for pathological inputs, your system won’t halt.
I think the more interesting question to ask when your problem is undecidable is “will someone ever care to try and run it on something that it cannot decide?” and the answer is almost always “no.” The higher rank polymorphism types thing @brendan mentioned is a great example: the paper about rank-2 (or greater than rank-2?) inference being undecidable literally encoded some kind of turing machine in the type system itself. This is SIGBOVIK stuff (except the SIGBOVIK stuff is not done for things which we care about).
This applies equally to other pathological properties (sometimes as computer scientists we forget that big O is an upper bound), like how Hindley-Milner is worst-case exponential. Or is it the algorithm Haskell uses? Whatever. The point is that you can write really short programs whose types blow up, and when you look at them they look incredibly silly. Maybe possibly one person has ever encountered a problem with their code because of this property.
I think a good follow-up blog post to summarize both this and your NP-Complete post might be titled “Hardness is an Upper Bound” ;)
Although I could also add that to the backlog of things I’ve been meaning to write…
I think the more interesting question to ask when your problem is undecidable is “will someone ever care to try and run it on something that it cannot decide?” and the answer is almost always “no.”
This is why I like to frame it in terms of “what could we accomplish if the problem was decidable”, ie which of those pathological inputs would become interesting if the problem became decidable. Like, imagine if rank-3 inference was decidable. As you said, then by adapting the approach in Rice’s Theorem we could bootstrap a type inference engine that can infer any type. Then, by the Curry-Howard correspondence (ha!) there exists a type corresponding to the theorem “P != NP”, and then an inference of that type constitutes a valid proof. Then we just spin up a halt detector and iterate over every possible program to automatically prove or disprove the theorem.
Of course that doesn’t work in our reality because any such construction has to worm its way through six or seven dozen “pathological inputs”. But it does show that undecidability does rule out possible approaches to problems!
Fair enough!
I concede that all my time spent trying to solve trivially undecidable problems has numbed me to the meaning of undecidability. If you were to tell me that finding such a proof of P != NP was indeed decidable, I would challenge you to decide it in a single digit number of millennia. But I agree that there is some utility in using decidability as a proxy (however weak) for hardness.
I’m tempted now to construct a nontrivial looking problem which is efficiently solvable with the exception of scant few undecidable instances.
If you end up constructing such a program you should absolutely do a writeup, too. I’d love to read it!
So many many years ago I did my masters thesis on compiling Haskell to the .net runtime. To give context for age, I spent the summer break a year previously porting the rotor gyro patch to ppc - rotor was the shared source .net impl, gyro was the original implementation of generics for .net from ms research.
The feedback from one of the reviewers was almost entirely stuff like “replace ‘lambda lifting with beta transforms’ or something similar (it’s been too long for me to remember the actual terms and phrases he demanded), literally none of which helped understanding: people in the FL academic community knew what lambda lifting (and similar) meant, most practical FL developers didn’t, and everyone else only knew lambda lifting and similar terms. Essentially all the feedback was “make your thesis less readable or understandable”
It was phenomenally annoying, and I can’t remember if I surrendered to the demands or not. If anyone is interested (why? :) ) it’s on nerget.com - a page that shows all the web dev skills I learned from almost a decade of working on browser engines :D
I had a look because I’m curious exactly what “lambda lifting” was replaced by and what citations supported the terminology (and who might be to blame!) but no dice, lambda lifting survived the review intact :-)
(beta transforms seem to be a thing in chaotic iterated functions, related to the logistic map.)
I didn’t understand how the author’s comment aligns with the linked paper by Wadler, which points out correspondences at both the term- and type-levels. The paper seemed very clear to me:
Propositions as Types is a notion with depth. It describes a correspondence between a given logic and a given programming language. At the surface, it says that for each proposition in the logic there is a corresponding type in the programming language—and vice versa. Thus we have
propositions as types.
It goes deeper, in that for each proof of a given proposition, there is a program of the corresponding type—and vice versa. Thus we also have
proofs as programs.
And it goes deeper still, in that for each way to simplify a proof there is a corresponding way to evaluate a program—and vice versa. Thus we further have
simplification of proofs as evaluation of programs.
Hence, we have not merely a shallow bijection between propositions and types, but a true isomorphism preserving the deep structure of proofs and programs, simplification and evaluation.
The post seems to claim that the type-level correspondence is not useful unless you’re leveraging dependent types, which I can certainly believe. But I didn’t understand why the post’s examples of term correspondences didn’t “count” as instances of Curry-Howard. Perhaps someone could elucidate for me?
Regarding the balanced tree example:
But this is not a theorem that follows from formulae-as-types but rather from good ol’ type safety and enforcement of module boundaries, just as above.
I agree that it doesn’t follow from formulae-as-types. But type-safety is a statement about “evaluation of programs” and the soundness of the corresponding logic.
(My wild conjecture here is that, for PL theorists, the term-level correspondence is so banal that it’s scarcely worth considering, hence the post only focusing on the type-level correspondence? That is: If your evaluation semantics are unsound, then you can’t prove anything useful anyways, so why consider it? But there are meaningful framings at the term-level for the uninitiated. For example, modeling implicit nulls as proof disjunction makes it clear why it’s fundamentally pernicious when it comes to program reasoning.)
For programming and software engineering practice, Curry-Howard is of essentially no practical benefit, unless you are using a dependently-typed language.
Could it be that a programming language that has a direct correspondence with logic is more coherent and easier to reason about? (Even if you don’t reason about your programs using your type system via dependent types.)