13 ms·

The Holy Trinity: Logic, Languages, Categories (2011)

111 points by rpbertp13 10y ago

igravious 10y ago
This link surfaced on HN before. :) 505 days ago to be precise during a discussion of the article “Relation Between Type Theory, Category Theory and Logic” on https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory https://ncatlab.org/nlab/show/relation+between+type+theory+a... Fascinating topic, previous discussion: https://news.ycombinator.com/item?id=9867465 https://news.ycombinator.com/item?id=9867465
- posterboy 10y ago
  The second comment in the discussion is confusing. What's the significance of the order in the tuple? An unordered set should be enough, so the tuples would be obvious permutations. Is the order decoded in the elements, eg. the operator *?
  - jsprogrammer 10y ago
    Everything (written, anyway) contains an order. The comment says that you may want to treat the same things in different orders as being the same "thing". A better, in my opinion, English translation of the univalence axiom is, "identity is equivalent to equivalency" (formally, [(A=B)~(A~B)]). You can find this translation in the HoTT book[0]. Also, check out multisets[1]. [0] http://saunders.phil.cmu.edu/book/hott-online.pdf http://saunders.phil.cmu.edu/book/hott-online.pdf (PDF page 16, or book page 4) [1] https://en.m.wikipedia.org/wiki/Multiset https://en.m.wikipedia.org/wiki/Multiset
  - lmm 10y ago
    You need to be able to write the group axioms down, so you need to distinguish the three elements. E.g. one of the axioms is 1 ∈ G, which means something very different from G ∈ 1. It all bottoms out in set theory, but (G, 1, X) really is a different set from (G, X, 1) (e.g. they might be represented as the sets {{G, 1, X}, {G, 1}, {G}} and {{G, 1, X}, {G, X}, {G}} respectively) so you do need to decide which is the "canonical" representation of that group, or else you need a rule that allows you to tell whether two different sets are representations of the same group.
adamnemecek 10y ago
I think that probability also deserves it's place in this tetrad.
- lambdasquirrel 10y ago
  Probability is an application of this aforementioned math, not foundational to it.
  - adamnemecek 10y ago
    The empirical point of view is definitely worth mentioning.
    - SomeStupidPoint 10y ago
      Could you elaborate on what you mean here? Im not sure I understand what you're trying to say.
      - adamnemecek 10y ago
        Well fundamentally probability is a framework for reasoning about the future based on previous events. This framework is analogous to logic but it's separate and even though it's not as clean it's a lot more useful for dealing with the real world.
        danharaj 10y ago
        Probability and probabilistic reasoning can be described by this framework. The theory is not yet as well developed as the classical theories. A discussion is here: https://golem.ph.utexas.edu/category/2007/02/category_theoretic_probability.html https://golem.ph.utexas.edu/category/2007/02/category_theore...
        aminorex 10y ago
        The framework itself needs description in probabilistic terms. Otherwise it has only pragmatic utility, and degraded epistemic status.
zengid 10y ago
I feel like this mystical mumbo-jumbo is counterproductive.
- throwaway729 10y ago
  It's a metaphor and meant to be tounge-in-cheek. There's nothing mystical about the actual content of the post.
xchaotic 10y ago
How is this going to make my code better? As far as I remember attempts to use proofs in production were counter productive. For most systems knowing that print "hello"; will do that is good enough.
- throwaway729 10y ago
  > How is this going to make my code better? This blog post is describing a research agenda that has already provided tremendous fruit to language designers. You can find the echoes of this research agenda in the design and implementation of basically every modern typed language, as well as a lot of the infrastructure for dynamic languages. If you're a language designer and you're not aware of the research agenda described in this blog post, learning more about programming language theory will be immensely beneficial. If you're not a language designer, then your attitude is kinda weird and off-putting. Like demanding an explanation for how fluid mechanics will make your code better. (As it turns out, understanding the theory behind the languages you're using will make you a better programmer, but that's really beside the point.) > As far as I remember attempts to use proofs in production were counter productive You remember incorrectly. > For most systems knowing that print "hello"; will do that is good enough. Isn't this attitude exactly how we end up with vulnerability-riddled, brittle, and barely maintainable code? I can't think of a single system I've designed or implemented where all I needed to know was that STDOUT worked properly. Most of my test cases capture far more interesting properties. The more of those test cases my tooling can rule out for me, the better.
  - posterboy 10y ago
    > > As far as I remember attempts to use proofs in production were counter productive Wait, does that mean in development? Otherwise, as I understood production so far it would be dependent typing. Supposedly that infers and automates a lot of otherwise handwritten safety checks. > You remember incorrectly. Indeed, Test Driven Development is huge and it's not even really formal. Formalisms should facilitate it a lot.
    - throwaway729 10y ago
orbifold 10y ago
An interesting published review of this relationship is "Physics, Topology, Logic and Computation: A Rosetta Stone", by John C. Baez, Mike Stay https://arxiv.org/abs/0903.0340 https://arxiv.org/abs/0903.0340. The first author alos has lots of interesting stuff related to (quantum) computation on his website.
dvt 10y ago
> Imagine a world in which logic, programming, and mathematics are unified, in which every proof corresponds to a program, every program to a mapping, every mapping to a proof! For those of you that may not know, this is called the Curry-Howard(-Lambek) Correspondence[1]. It establishes an isomorphism between well-formed computer programs and formal logic. This isomorphism is fairly intuitive when doing something like (typed) λ-calculus, but it also applies to things like Java and C++. [1] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
- Chinjut 10y ago
  Yes, Bob Harper is aware of, and intentionally discussing precisely, this. (The "Curry-Howard-Lambek" correspondence, if you like)
  - dvt 10y ago
    He's a PhD in CS so I assumed he did :) I linked it for other people that may not know that it's a thing. The article itself is a bit hand-wavy.
    - aminorex 10y ago
      Extremely so. Lacking so much as useful keywords for finding what he refers to as "standard sources".
- mafribe 10y ago
  Curry-Howard is not known to apply to Java and C++. That's because the typing systems of these languages are no logics. For a start, in both languages, you can write non-terminating programs, hence any type is inhabited, which means inconsistency if you interpret types as truth-bearing propositions. Currently Curry-Howard mostly only works for strongly normalising, pure functional languages. It's also not clear if Curry-Howard is really an isomorphism. For a map to be an isomorphism, structure has to be preserved in both directions, but what is the structure on proofs? That's a wide open question. We can't even agree on what it means for proofs to be equal. (The structure of is the content of Hilbert's 24th problem that he decided not to include in his famous 23 problems [1].) It's better to speak of the Curry-Howard correspondence. [1] https://en.wikipedia.org/wiki/Hilbert%27s_twenty-fourth_problem https://en.wikipedia.org/wiki/Hilbert%27s_twenty-fourth_prob...
pmoriarty 10y ago
"In this sense all three have ontological force; they codify what is, not how to describe what is already given to us." What's the difference between "what is" and "what is already given to us"? What's the difference between codifying and describing it?
- danharaj 10y ago
  20th century mathematics takes first order classical logic and set theory as foundational. All other mathematics then becomes the analysis of sets via proofs in first order classical logic. The ugliness of this definition is that it is unnatural. Mathematicians don't always think in sets, they think directly about mathematical objects intuitively. No one cares which set encodes the number e, for example, but foundationally speaking the number e must be a set, and the properties of e are the properties of that set. This is unsatisfactory from both an aesthetic and practical point of view: the Set foundations of modern mathematics obscure the fundamental, recurring themes of mathematics. This is true even in computer science. Turing machines are sets too! I know, ridiculous. Harper is saying that the correspondence between logic, language, and category is a suitable foundation for mathematical/logical/computational activity and they're all the same thing. This is not merely in the sense that the objects we work with are given beforehand by some more fundamental theory and we are merely analyzing them, but in the sense that logic/language/category is the appropriate setting in which to define our objects, to do synthetic as well as analytical reasoning. That is what makes a particular theory foundational.
  - AnimalMuppet 10y ago
    > All other mathematics then becomes the analysis of sets via proofs in first order classical logic. That's like saying that home construction becomes an exercise in atomic physics. Yes, in some sense it's true, but it's so far removed from what's actually going on that it's completely uninteresting. Take the person working on differentiable manifolds. Do they care about that as problems in set theory? Not at all. Change it to problems in logic/language/category theory? They still don't care. Axiomatize mathematics how you will, they won't care, because they're as many layers away from it as the home construction people are from atomic physics.
cousin_it 10y ago
Unfortunately the most beautiful form of that analogy is the one that's crippled on both sides: computation (without Turing completeness) is equivalent to logic (without excluded middle). Add Turing completeness and you lose soundness. Add excluded middle and you lose confluence. Of course you can put epicycles on top of the simple idea and make it do anything you want, but as far as I know, no one has ever used the Curry-Howard toolbox to solve a nontrivial algorithmic problem for the first time. Any exciting paper about algorithms (like quicksort, Dijkstra's algorithm, or Primes in P) will usually have a lot of math involving numbers, but no math involving types.
- s-phi-nl 10y ago
  Could you point to a reference for the non-confluence of logic without excluded middle? It sounds interesting and a quick Google search did not find anything.
  - cousin_it 10y ago
    With excluded middle. This is the explanation that clicked for me: http://stackoverflow.com/questions/24711643/how-come-that-we-can-implement-call-cc-but-the-classical-logic-intuitionistic http://stackoverflow.com/questions/24711643/how-come-that-we...
    - s-phi-nl 10y ago
      Thanks! Yes, with excluded middle is what I meant.
threepipeproblm 10y ago
What a coincidence... just ran across this video -- https://www.youtube.com/watch?v=YRu7Xi-mNK8 https://www.youtube.com/watch?v=YRu7Xi-mNK8 -- last night, where Prof. Frank Pfenning makes a similar point in the first few minutes.

111 points by rpbertp13 10y ago

This link surfaced on HN before. :) 505 days ago to be precise during a discussion of the article “Relation Between Type Theory, Category Theory and Logic” on https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory https://ncatlab.org/nlab/show/relation+between+type+theory+a... Fascinating topic, previous discussion: https://news.ycombinator.com/item?id=9867465 https://news.ycombinator.com/item?id=9867465

posterboy 10y ago
The second comment in the discussion is confusing. What's the significance of the order in the tuple? An unordered set should be enough, so the tuples would be obvious permutations. Is the order decoded in the elements, eg. the operator *?
- jsprogrammer 10y ago
  Everything (written, anyway) contains an order. The comment says that you may want to treat the same things in different orders as being the same "thing". A better, in my opinion, English translation of the univalence axiom is, "identity is equivalent to equivalency" (formally, [(A=B)~(A~B)]). You can find this translation in the HoTT book[0]. Also, check out multisets[1]. [0] http://saunders.phil.cmu.edu/book/hott-online.pdf http://saunders.phil.cmu.edu/book/hott-online.pdf (PDF page 16, or book page 4) [1] https://en.m.wikipedia.org/wiki/Multiset https://en.m.wikipedia.org/wiki/Multiset
- lmm 10y ago
  You need to be able to write the group axioms down, so you need to distinguish the three elements. E.g. one of the axioms is 1 ∈ G, which means something very different from G ∈ 1. It all bottoms out in set theory, but (G, 1, X) really is a different set from (G, X, 1) (e.g. they might be represented as the sets {{G, 1, X}, {G, 1}, {G}} and {{G, 1, X}, {G, X}, {G}} respectively) so you do need to decide which is the "canonical" representation of that group, or else you need a rule that allows you to tell whether two different sets are representations of the same group.

adamnemecek 10y ago

I think that probability also deserves it's place in this tetrad.

lambdasquirrel 10y ago
Probability is an application of this aforementioned math, not foundational to it.
- adamnemecek 10y ago
  The empirical point of view is definitely worth mentioning.
  - SomeStupidPoint 10y ago
    Could you elaborate on what you mean here? Im not sure I understand what you're trying to say.
    - adamnemecek 10y ago
      Well fundamentally probability is a framework for reasoning about the future based on previous events. This framework is analogous to logic but it's separate and even though it's not as clean it's a lot more useful for dealing with the real world.
      - danharaj 10y ago
        Probability and probabilistic reasoning can be described by this framework. The theory is not yet as well developed as the classical theories. A discussion is here: https://golem.ph.utexas.edu/category/2007/02/category_theoretic_probability.html https://golem.ph.utexas.edu/category/2007/02/category_theore...
        aminorex 10y ago
        The framework itself needs description in probabilistic terms. Otherwise it has only pragmatic utility, and degraded epistemic status.

zengid 10y ago

I feel like this mystical mumbo-jumbo is counterproductive.

throwaway729 10y ago
It's a metaphor and meant to be tounge-in-cheek. There's nothing mystical about the actual content of the post.

xchaotic 10y ago

How is this going to make my code better? As far as I remember attempts to use proofs in production were counter productive. For most systems knowing that print "hello"; will do that is good enough.

throwaway729 10y ago
> How is this going to make my code better? This blog post is describing a research agenda that has already provided tremendous fruit to language designers. You can find the echoes of this research agenda in the design and implementation of basically every modern typed language, as well as a lot of the infrastructure for dynamic languages. If you're a language designer and you're not aware of the research agenda described in this blog post, learning more about programming language theory will be immensely beneficial. If you're not a language designer, then your attitude is kinda weird and off-putting. Like demanding an explanation for how fluid mechanics will make your code better. (As it turns out, understanding the theory behind the languages you're using will make you a better programmer, but that's really beside the point.) > As far as I remember attempts to use proofs in production were counter productive You remember incorrectly. > For most systems knowing that print "hello"; will do that is good enough. Isn't this attitude exactly how we end up with vulnerability-riddled, brittle, and barely maintainable code? I can't think of a single system I've designed or implemented where all I needed to know was that STDOUT worked properly. Most of my test cases capture far more interesting properties. The more of those test cases my tooling can rule out for me, the better.
- posterboy 10y ago
  > > As far as I remember attempts to use proofs in production were counter productive Wait, does that mean in development? Otherwise, as I understood production so far it would be dependent typing. Supposedly that infers and automates a lot of otherwise handwritten safety checks. > You remember incorrectly. Indeed, Test Driven Development is huge and it's not even really formal. Formalisms should facilitate it a lot.
  - throwaway729 10y ago

orbifold 10y ago

An interesting published review of this relationship is "Physics, Topology, Logic and Computation: A Rosetta Stone", by John C. Baez, Mike Stay https://arxiv.org/abs/0903.0340 https://arxiv.org/abs/0903.0340. The first author alos has lots of interesting stuff related to (quantum) computation on his website.

dvt 10y ago

> Imagine a world in which logic, programming, and mathematics are unified, in which every proof corresponds to a program, every program to a mapping, every mapping to a proof! For those of you that may not know, this is called the Curry-Howard(-Lambek) Correspondence[1]. It establishes an isomorphism between well-formed computer programs and formal logic. This isomorphism is fairly intuitive when doing something like (typed) λ-calculus, but it also applies to things like Java and C++. [1] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

Chinjut 10y ago
Yes, Bob Harper is aware of, and intentionally discussing precisely, this. (The "Curry-Howard-Lambek" correspondence, if you like)
- dvt 10y ago
  He's a PhD in CS so I assumed he did :) I linked it for other people that may not know that it's a thing. The article itself is a bit hand-wavy.
  - aminorex 10y ago
    Extremely so. Lacking so much as useful keywords for finding what he refers to as "standard sources".
mafribe 10y ago
Curry-Howard is not known to apply to Java and C++. That's because the typing systems of these languages are no logics. For a start, in both languages, you can write non-terminating programs, hence any type is inhabited, which means inconsistency if you interpret types as truth-bearing propositions. Currently Curry-Howard mostly only works for strongly normalising, pure functional languages. It's also not clear if Curry-Howard is really an isomorphism. For a map to be an isomorphism, structure has to be preserved in both directions, but what is the structure on proofs? That's a wide open question. We can't even agree on what it means for proofs to be equal. (The structure of is the content of Hilbert's 24th problem that he decided not to include in his famous 23 problems [1].) It's better to speak of the Curry-Howard correspondence. [1] https://en.wikipedia.org/wiki/Hilbert%27s_twenty-fourth_problem https://en.wikipedia.org/wiki/Hilbert%27s_twenty-fourth_prob...

pmoriarty 10y ago

"In this sense all three have ontological force; they codify what is, not how to describe what is already given to us." What's the difference between "what is" and "what is already given to us"? What's the difference between codifying and describing it?

danharaj 10y ago
20th century mathematics takes first order classical logic and set theory as foundational. All other mathematics then becomes the analysis of sets via proofs in first order classical logic. The ugliness of this definition is that it is unnatural. Mathematicians don't always think in sets, they think directly about mathematical objects intuitively. No one cares which set encodes the number e, for example, but foundationally speaking the number e must be a set, and the properties of e are the properties of that set. This is unsatisfactory from both an aesthetic and practical point of view: the Set foundations of modern mathematics obscure the fundamental, recurring themes of mathematics. This is true even in computer science. Turing machines are sets too! I know, ridiculous. Harper is saying that the correspondence between logic, language, and category is a suitable foundation for mathematical/logical/computational activity and they're all the same thing. This is not merely in the sense that the objects we work with are given beforehand by some more fundamental theory and we are merely analyzing them, but in the sense that logic/language/category is the appropriate setting in which to define our objects, to do synthetic as well as analytical reasoning. That is what makes a particular theory foundational.
- AnimalMuppet 10y ago
  > All other mathematics then becomes the analysis of sets via proofs in first order classical logic. That's like saying that home construction becomes an exercise in atomic physics. Yes, in some sense it's true, but it's so far removed from what's actually going on that it's completely uninteresting. Take the person working on differentiable manifolds. Do they care about that as problems in set theory? Not at all. Change it to problems in logic/language/category theory? They still don't care. Axiomatize mathematics how you will, they won't care, because they're as many layers away from it as the home construction people are from atomic physics.

cousin_it 10y ago

Unfortunately the most beautiful form of that analogy is the one that's crippled on both sides: computation (without Turing completeness) is equivalent to logic (without excluded middle). Add Turing completeness and you lose soundness. Add excluded middle and you lose confluence. Of course you can put epicycles on top of the simple idea and make it do anything you want, but as far as I know, no one has ever used the Curry-Howard toolbox to solve a nontrivial algorithmic problem for the first time. Any exciting paper about algorithms (like quicksort, Dijkstra's algorithm, or Primes in P) will usually have a lot of math involving numbers, but no math involving types.

s-phi-nl 10y ago
Could you point to a reference for the non-confluence of logic without excluded middle? It sounds interesting and a quick Google search did not find anything.
- cousin_it 10y ago
  With excluded middle. This is the explanation that clicked for me: http://stackoverflow.com/questions/24711643/how-come-that-we-can-implement-call-cc-but-the-classical-logic-intuitionistic http://stackoverflow.com/questions/24711643/how-come-that-we...
  - s-phi-nl 10y ago
    Thanks! Yes, with excluded middle is what I meant.

threepipeproblm 10y ago

What a coincidence... just ran across this video -- https://www.youtube.com/watch?v=YRu7Xi-mNK8 https://www.youtube.com/watch?v=YRu7Xi-mNK8 -- last night, where Prof. Frank Pfenning makes a similar point in the first few minutes.