Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

existentialtype.wordpress.com

Post reply on HN
Print view View original

31–40 of 51 posts

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

#31

Post by mafribe »

chriswarbo wrote: post #30
mafribe wrote: post #29

Earlier quoted context omitted.

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 Cu…

> 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. As far as I'm aware, a…

   unsound logic is still a logic
Hmmm ... If your logic is unsound, anything can be proven. Soundness is a key requirement of any logic for this reason.

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

#32

Post by lmm »

posterboy wrote: post #14
igravious wrote: post #2

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+a... Fascinating topic, previous discussion: https://news.ycombinator.com/item?id=9867465

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 *?

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.

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

#33

Post by cousin_it »

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.

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

#34

Post by lmm »

xchaotic wrote: post #6

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.

https://tahoe-lafs.org/~davidsarah/noether-friam4.pdf opens with a good explanation of the rationale for this kind of thing. Knowing that print prints is good enough until you get to programs that are too large to hold in your head all at once. At that point you need a language with symmetries that enable you to think about complex pieces in simpler terms; thinking about it in terms of logic can help clarify what those symmetries are and where they are broken, which usually corresponds to constructs that lead to unpleasant surprises in production.

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

#35

Post by chriswarbo »

mafribe wrote: post #31
chriswarbo wrote: post #30

Earlier quoted context omitted.

> 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. As far as I'm aware, a…

unsound logic is still a logic Hmmm ... If your logic is unsound, anything can be proven. Soundness is a key requirement of any logic for this reason.

I would hedge my bets, and say that soundness is often a useful property of logics, especially when they're used for proving theorems/conjectures.

In the case of C++ and Java, they're not often (ever?) used for proving, yet Curry-Howard tells us that they are logics.

Curry-Howard goes both ways, it's not a reduction of programming to theorem proving; if it were, then we could write optimising compilers for all dynamically typed languages, which output "null" for every input.

Likewise, mathematics cannot be summarised as "getting stuff to compile".

Instead, the concerns and interests of the practitioners from both sides are unchanged by Curry-Howard; it just tells us that both those groups are actually working within the same context, and hence they may be able to share ideas/tools/techniques/etc.

Whilst an unsound logic might be useless to a logician, a programmer (or even computer scientist!) may not care too much, since they might be much more concerned about, say, the computational complexity of an algorithm rather than its types.

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

#37

Post by mafribe »

chriswarbo wrote: post #35
mafribe wrote: post #31

Earlier quoted context omitted.

unsound logic is still a logic Hmmm ... If your logic is unsound, anything can be proven. Soundness is a key requirement of any logic for this reason.

I would hedge my bets, and say that soundness is often a useful property of logics, especially when they're used for proving theorems/conjectures. In the case of C++ and Java, they're not often (ever?) used for proving, yet Curry-Howard tells us that they are logics. Curry-Howard goes both ways, it's not a reduction of programming to theorem proving; if it were, then we could write optimising compilers for all dynami…

Can you explain to me in what sense the Java and C++ typing systems are logics? Because I don't see it.

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

#38

Post by AnimalMuppet »

danharaj wrote: post #21
pmoriarty wrote: post #18

"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?

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 foundat…

> 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.

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

#39

Post by dvt »

mafribe wrote: post #37
chriswarbo wrote: post #35

Earlier quoted context omitted.

I would hedge my bets, and say that soundness is often a useful property of logics, especially when they're used for proving theorems/conjectures. In the case of C++ and Java, they're not often (ever?) used for proving, yet Curry-Howard tells us that they are logics. Curry-Howard goes both ways, it's not a reduction of programming to theorem proving; if it were, then we could write optimising compilers for all dynami…

Can you explain to me in what sense the Java and C++ typing systems are logics? Because I don't see it.

Any typing system that has at least two types (functional and non-functional) is a logic. In fact, modus ponens follows axiomatically via →elimination:

Let α → H be a functional type where α is a Person type, and H is a boolean type.

   Γ ⊢ α → H     Γ ⊢ α
  --------------------- (→e)
            Γ ⊢ H
What this means is that you can have a function isAtHome(x) which takes a Person and returns a boolean. This schema itself is a logic insofar that it follows the same rules as the proposition A → B where A is true:

  A → B
  A
  ∴ B
(I wrote a simple and short paper[1] about typing λ-calculus in the context of Frege's concept horse paradox a few years ago.)

[1] http://dvt.name/logic/horse2.pdf

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

#40

Post by s-phi-nl »

cousin_it wrote: post #33

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…

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.
Post reply on HN