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

21–30 of 51 posts

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

#21

Post by danharaj »

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

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

#22

Post by danharaj »

adamnemecek wrote: post #20
SomeStupidPoint wrote: post #19

Earlier quoted context omitted.

Could you elaborate on what you mean here? Im not sure I understand what you're trying to say.

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.

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

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

#23

Post by hyperpape »

posterboy wrote: post #11
throwaway729 wrote: post #9

Earlier quoted context omitted.

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

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

At some level of abstraction, types of any kind are already proofs, and they're tremendously important in many actual existing languages.

What you're probably glomming on to is that efforts to push the bounds of what you can prove (higher kinded or dependent types) have had mixed results (mixed in the sense that some people think they're great, others are unconvinced).

So we're in a weird situation where many many people are using a tool, but relatively few are interested in new developments concerning how to use that tool.

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

#24

Post by Ericson2314 »

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.

I could go on and on about why this stuff will make programming more beautiful/enjoyable. But let's do the stick not the caret. From recently-posted http://www.dailydot.com/layer8/bruce-schneier-internet-of-th..., it's high time we tighten your "good enough".

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

#25

Post by jsprogrammer »

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

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 (PDF page 16, or book page 4)

[1] https://en.m.wikipedia.org/wiki/Multiset

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

#26

Post by cscurmudgeon »

lambdasquirrel wrote: post #8
adamnemecek wrote: post #3

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

Probability is an application of this aforementioned math, not foundational to it.

While on the surface probability seems different from logic, it fits neatly within it.

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

#27

Post by aminorex »

dvt wrote: post #17
Chinjut wrote: post #15

Earlier quoted context omitted.

Yes, Bob Harper is aware of, and intentionally discussing precisely, this. (The "Curry-Howard-Lambek" correspondence, if you like)

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.

Extremely so. Lacking so much as useful keywords for finding what he refers to as "standard sources".

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

#28

Post by aminorex »

danharaj wrote: post #22
adamnemecek wrote: post #20

Earlier quoted context omitted.

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.

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

The framework itself needs description in probabilistic terms. Otherwise it has only pragmatic utility, and degraded epistemic status.

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

#29

Post by mafribe »

dvt wrote: post #13

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

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

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

#30

Post by chriswarbo »

mafribe wrote: post #29
dvt wrote: post #13

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

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 complicated, inscrutable, unsound logic is still a logic. It's debatable whether it's a useful logic, but even that's not a fatal flaw for these languages, seeing as their main design focus is making normalisation of programs/proofs convenient.

I suppose the two perspectives of Curry-Howard aren't so much about proving/programming as they are about caring-about-the-theorem/caring-about-the-proof. The existence of non-termination is a problem if you care about theorems, since you can't trust proofs and must deal with them manually to see if they're doing anything fishy.

Java and C++ care so much about proofs that they don't really understand what else you might want to do other than dealing with proofs (programs) manually. If you presented a C++ programmer with an automated theorem prover (given a C++ type signature, return a C++ program fragment of that type) I imagine they wouldn't be particularly impressed, since types are just one small part of the concerns that a C++ programmer has.

Post reply on HN