In a world where cranks use Curry-Howard to justify their ridiculous beliefs, it is refreshing to see not just a correct application, but a well-formed and aesthetically pleasing presentation. Thank you for not trying to obfuscate the material.
> where cranks use Curry-Howard to justify their ridiculous beliefs
I'm not an abstract thinker so that correspondence is not interesting to me (open to being educated though if it is applicable to my daily work), but to what ridiculous beliefs do you refer? TIA
Sorry, by "untyped" I meant "dynamically typed." CL does have a sophisticated type hierarchy, but to my knowledge, according to the standard, types are checked at runtime, right? In the type-theoretic sense, "type" refers to a statically known classification.
Curry-Howard is the idea that static types are propositional formulas and expressions that have such types are their proofs. Under the Curry-Howard correspondence, a static typechecker analyzing your program is equivalent to a proof checker ensuring that your proof is valid.
People tend to invoke Curry-Howard to praise ML- and Haskell-style algebraic types (according to Curry-Howard, sum types are disjunction, product types are conjunction, and function/exponential types are implication).
Not entirely. There are type errors that are caught at compilation time.
A stark difference is that Lisp has the idea that type checking is done on values, not on symbols. If the compiler can deduce that a value is going to conflict in a given context, it will flag the error.
Curry-Howard-Lambek distills largely into a big table which relates type theory, category theory, formal logic, and metamathematics. This table is very precise, but high-dimensional, so that we can only take small limited slices of it. Nonetheless, the slices that we take are very formal. The important parts are well-known and published, say at [0] or [1]; extending beyond this is possible but requires care and effort. That said, once one groks the nature of the correspondence, then it becomes painfully obvious, to the point where folks who don't grok it seem block-headed.
I don't really have a glossary or nosology of how people misuse this, but I'd say some wrong ideas include:
* If a language has a type system, then it is usable for formal proofs, it is sound, and it is a language that ends the need for other languages.
* Dependently-typed languages have values that are also types, so all values are types, and therefore dependent typing makes no sense.
* Because my language uses higher-order logic instead of first-order logic, Turing's results don't limit my language's problem-solving abilities.
* Because of my religious beliefs, type universes have a certain shape, and thus Cantor's results are incorrect.
* The English language is far more powerful than any programming language.
* All logic is really just intuitionistic logic.
* All logic is really just linear logic.
* Syntactic formalism must be wrong, because abstracta only exist in my mind.
To repeat myself, all of these are wrong, despite some relatively large tribes of programmers believing them sincerely.
Thank you! That list intersects with some of what has been troubling me too. You should write a blog post or paper expanding on these. Some of these beliefs are more dangerous than others. Especially:
> * All logic is really just linear logic.
and
> * Because of my religious beliefs, type universes have a certain shape, and thus Cantor's results are incorrect.
The term you want to search for is "Natural Deduction". It's what you use if you study type theory. I don't know any lightweight introductions off the top of my head.
means "If A and B, then C". Any free variables in A, B, C are universally quantified outside the "if". The reason for writing the rules in this weird format is that you can combine them in a tree:
A B
-------
C D
---------
E
This proves E, given A, B, and D, via the application of two rules.
The blog post (and your response) is actually a bit confusing, as we should be seeing inline rules -- at least that's how I've seen it in just about every textbook. The "implication" rule you suggest is actually (technically) called "elimination" (in λ-calculus, we say you eliminate a variable) and should be denoted via →e (sometimes the arrow is omitted). As a more practical example, see proposition (11) in this paper I wrote back in college[1]. There are two elimination rules, both denoted by an inline →e.
While naming the different derivation rules can be useful for guiding readers the names are not formally necessary.
The rules
A B
-----
C
and
A B
----- (→c)
C
are logically equivalent, the latter just gives you a name to refer to the rule by.
Additionally, I would be careful about correcting others that something is "technically" called something else as programming language researchers often use many names for the same concept.
> Additionally, I would be careful about correcting others that something is "technically" called something else as programming language researchers often use many names for the same concept.
My point had nothing to do with programming language research (in fact, my academic background is logic/metalogic). And by the way, this is not a rule:
A B
----- (→c)
C
It's a derivation (also known as a proof) -- technical terms are important when doing logic. The rule is →c -- so I know what you're doing by including the →c there. Why the →c is necessary (and, again, I've seen it in every lambda calculus/type theory book I've taken a gander at) is because there are many rules[1] (including several kinds of elimination, so things can get complicated and it's important to keep our ducks in a row).
Perhaps using abstract names A, B, and C was unclear. The following is the rule that is commonly referred to as modus ponens:
A → B A
-----------
B
However, modus ponens is just one of the names for this. I could also call it function elimination. I could call it →e. Or I could not bother giving it a name and just say that this is a rule in my logic call it whatever you want in your head if you so desire.
Things can get complicated, but they aren't always complicated so naming rules isn't strictly necessary.
During undergrad, I was only exposed to logic in my set theory and theory of computation classes. Any recommendations on good books/textbooks that are good for a relative beginners exploring set theory and type theory?
Chapter 1 of the HoTT book introduces Martin-Lof's dependent type theory, then the rest of the book covers HoTT-specific topics: https://homotopytypetheory.org/book/
That's an entire book that is merely a guide on which other books to read and what to focus on in one's journey of formal logic.
I have started with the most intro book it recommends "How to Prove It : A Structured Approach by Daniel J. Velleman". It seems to be quite similar to whatever text book I used in the class that focused on logic in college. I intend to skip around a bit though as my real goal here is to be able to understand all of this advanced type theory that I keep seeing in the FP/Haskell/Idris world.
IMO Paul Tarau has some good stuff in this area, e.g.: "On a uniform representation of combinators, arithmetic, lambda terms and types", Paul Tarau https://dl.acm.org/doi/10.1145/2790449.2790526
Abstract:
> A uniform representation, as binary trees with empty leaves, is given to expressions built with Rosser's X-combinator, natural numbers, lambda terms and simple types. Type inference, normalization of combinator expressions and lambda terms in de Bruijn notation, ranking/unranking algorithms and tree-based natural numbers are described as a literate Prolog program.
> With sound unification and compact expression of combinatorial generation algorithms, logic programming is shown to conveniently host a declarative playground where interesting properties and behaviors emerge from the interaction of heterogenous but deeply connected computational objects.
> Yet, I believe it is fairly common to call this kind of logic intuitionistic logic, even though there is no rule for ⊥.
I don't believe this is very common—it's _an_ intuitionist logic, but "intuitionistic logic" by itself pretty much always includes ex falso—but actually it's rather strange that this is the case; it's not immediately clear that ex falso is constructive at all!
Minimal logic is both 'intuitionistic' (since LEM does not hold) and paraconsistent (since ex falso does not hold). I actually think there's a fairly solid case to say that only paraconsistent logics can be thought of as truly constructive; certainly if we start from BHK, it's not at all obvious that ex falso is a sound principle, and Kolmogorov himself had great issues accepting this. When he finally managed to convince himself of this in 1932 [1], it seems more that he was trying to finish off the logical framework by sidestepping the issue.
Kapsner [2] argues that the constructivist can only accept ex falso if she is willing to accept so called "empty promise constructions" as being constructive (see the source for more details on what this means, but it seems to broadly line up with Kolmogorov's justification); I personally don't think that they are compatible with the way BHK is usually presented at all.
Brouwer isn't around to tell us exactly what _he_ means by constructivism, so ultimately this is all philosophical, but I think this it's an interesting area that people don't really think aboutl I think a lot of people are exposed to intuitionistic logic via Martin-Lof type theories but don't actually consider how the logic fits into the wider notion of constructivism.
I put a related question on Computer Science Stack Exchange a week ago. Linking it here in the hopes that HN users roll-calling here will shed some light.
25 comments
[ 3.4 ms ] story [ 68.3 ms ] threadI'm not an abstract thinker so that correspondence is not interesting to me (open to being educated though if it is applicable to my daily work), but to what ridiculous beliefs do you refer? TIA
Curry-Howard is the idea that static types are propositional formulas and expressions that have such types are their proofs. Under the Curry-Howard correspondence, a static typechecker analyzing your program is equivalent to a proof checker ensuring that your proof is valid.
People tend to invoke Curry-Howard to praise ML- and Haskell-style algebraic types (according to Curry-Howard, sum types are disjunction, product types are conjunction, and function/exponential types are implication).
Not entirely. There are type errors that are caught at compilation time.
A stark difference is that Lisp has the idea that type checking is done on values, not on symbols. If the compiler can deduce that a value is going to conflict in a given context, it will flag the error.
And types are checked at run time as well.
I don't really have a glossary or nosology of how people misuse this, but I'd say some wrong ideas include:
* If a language has a type system, then it is usable for formal proofs, it is sound, and it is a language that ends the need for other languages.
* Dependently-typed languages have values that are also types, so all values are types, and therefore dependent typing makes no sense.
* Because my language uses higher-order logic instead of first-order logic, Turing's results don't limit my language's problem-solving abilities.
* Because of my religious beliefs, type universes have a certain shape, and thus Cantor's results are incorrect.
* The English language is far more powerful than any programming language.
* All logic is really just intuitionistic logic.
* All logic is really just linear logic.
* Syntactic formalism must be wrong, because abstracta only exist in my mind.
To repeat myself, all of these are wrong, despite some relatively large tribes of programmers believing them sincerely.
[0] https://ncatlab.org/nlab/show/relation+between+type+theory+a...
[1] http://math.ucr.edu/home/baez/rosetta.pdf
Obviously it's all really just tensorial logic :^)
> * All logic is really just linear logic.
and
> * Because of my religious beliefs, type universes have a certain shape, and thus Cantor's results are incorrect.
> All logic is really just linear logic.
Who has said these?
https://en.wikipedia.org/wiki/Natural_deduction
The short version is that
means "If A and B, then C". Any free variables in A, B, C are universally quantified outside the "if". The reason for writing the rules in this weird format is that you can combine them in a tree: This proves E, given A, B, and D, via the application of two rules.[1] https://dvt.name/logic/horse2.pdf
The rules
and are logically equivalent, the latter just gives you a name to refer to the rule by.Additionally, I would be careful about correcting others that something is "technically" called something else as programming language researchers often use many names for the same concept.
My point had nothing to do with programming language research (in fact, my academic background is logic/metalogic). And by the way, this is not a rule:
It's a derivation (also known as a proof) -- technical terms are important when doing logic. The rule is →c -- so I know what you're doing by including the →c there. Why the →c is necessary (and, again, I've seen it in every lambda calculus/type theory book I've taken a gander at) is because there are many rules[1] (including several kinds of elimination, so things can get complicated and it's important to keep our ducks in a row).[1] https://www.irif.fr/~mellies/mpri/mpri-ens/biblio/Selinger-L...
Things can get complicated, but they aren't always complicated so naming rules isn't strictly necessary.
This is an exposition of Martin-Lof's dependent type theory: http://www.cs.nott.ac.uk/~psztxa/mgs-17/notes-mgs17.pdf Section 5 is about Homotopy Type Theory (HoTT), a newer type theory that is still being developed.
Chapter 1 of the HoTT book introduces Martin-Lof's dependent type theory, then the rest of the book covers HoTT-specific topics: https://homotopytypetheory.org/book/
That's an entire book that is merely a guide on which other books to read and what to focus on in one's journey of formal logic.
I have started with the most intro book it recommends "How to Prove It : A Structured Approach by Daniel J. Velleman". It seems to be quite similar to whatever text book I used in the class that focused on logic in college. I intend to skip around a bit though as my real goal here is to be able to understand all of this advanced type theory that I keep seeing in the FP/Haskell/Idris world.
Abstract:
> A uniform representation, as binary trees with empty leaves, is given to expressions built with Rosser's X-combinator, natural numbers, lambda terms and simple types. Type inference, normalization of combinator expressions and lambda terms in de Bruijn notation, ranking/unranking algorithms and tree-based natural numbers are described as a literate Prolog program.
> With sound unification and compact expression of combinatorial generation algorithms, logic programming is shown to conveniently host a declarative playground where interesting properties and behaviors emerge from the interaction of heterogenous but deeply connected computational objects.
I don't believe this is very common—it's _an_ intuitionist logic, but "intuitionistic logic" by itself pretty much always includes ex falso—but actually it's rather strange that this is the case; it's not immediately clear that ex falso is constructive at all!
Minimal logic is both 'intuitionistic' (since LEM does not hold) and paraconsistent (since ex falso does not hold). I actually think there's a fairly solid case to say that only paraconsistent logics can be thought of as truly constructive; certainly if we start from BHK, it's not at all obvious that ex falso is a sound principle, and Kolmogorov himself had great issues accepting this. When he finally managed to convince himself of this in 1932 [1], it seems more that he was trying to finish off the logical framework by sidestepping the issue.
Kapsner [2] argues that the constructivist can only accept ex falso if she is willing to accept so called "empty promise constructions" as being constructive (see the source for more details on what this means, but it seems to broadly line up with Kolmogorov's justification); I personally don't think that they are compatible with the way BHK is usually presented at all.
Brouwer isn't around to tell us exactly what _he_ means by constructivism, so ultimately this is all philosophical, but I think this it's an interesting area that people don't really think aboutl I think a lot of people are exposed to intuitionistic logic via Martin-Lof type theories but don't actually consider how the logic fits into the wider notion of constructivism.
[1] : https://plato.stanford.edu/entries/intuitionistic-logic-deve...
[2] : https://www.springer.com/gp/book/9783319052052
I find the discussion in of logic in https://sites.math.northwestern.edu/~richter/HolInformalMath... more concrete and more accessible.
Ref: https://cs.stackexchange.com/questions/122066/does-the-under...