Propositions Are Not Types (2018)

https://medium.com/@rplevy/propositions-are-not-types-naturalizing-information-content-in-computing-e51b94ad6674

by shalabhc • 7 years ago

16 17 7 years ago

auggierose• 7 years ago

Sorry. This text is absolutely useless to me. What is it trying to say? Don't get it, although I agree that propositions are not necessarily types.

uryga3• 7 years ago

propositions are not necessarily types

could you expand on this?

TheAsprngHacker• 7 years ago

I'm very confused about what this blog post is trying to argue. Most of what it discusses isn't related to the Curry-Howard correspondence at all?

At the risk of sounding anti-intellectual, perhaps Orwell's "Politics and the English Language" [0] is relevant here?

[0] http://www.orwell.ru/library/essays/politics/english/e_polit

uryga3• 7 years ago

yeah, Ctrl+F "type" gives 4 (non-title) occurrences, all of them in the first two paragraphs. the rest seems to be related to AI and the problems of making it "actually refer to the real world". weird!

EDIT2: i think the author is actually talking about cogsci "mental propositions". (see my other comment)

jrsala3• 7 years ago

I think in the context of the author's field, an enlarged definition of the notion of "propositions" is adopted whereby a proposition is a useful statement about the real world, distinct from, but related to the mathematical definition of a formal object used for reasoning about some notion of truth.

The author's point in part 1 is that type systems are intrinsically incapable of formalizing propositions so as to achieve the holy grail of making software systems effective, safe, or whatever other property is sought after, in the real world. The author then goes on to explain this idea and to suggest a different approach.

As for the Curry-Howard isomorphism, the author does say it is perfectly valid from a mathematical point of view, but that is not the subject of the text.

mcguire• 7 years ago

On what grounds is it argued that humanity operates on "content" grounds? If the stuff in my head operates purely on syntactic, formal, biological, chemical, physics methods, then the introduction of semantics or "content" is a red herring, even if you argue that multiple humans is the magic factor, it seems to me.

fauigerzigerk3• 7 years ago

Initially I thought that this could be one of those automatically generated nonsensical but scientific sounding texts (https://pdos.csail.mit.edu/archive/scigen/)

But upon closer reading I now think it's actually the reverse. The author apparently tried very hard to obfuscate the fact that he does have something meaningful to say by using utterly nonsensical sounding language.

jrsala3• 7 years ago

I think the author simply uses the vocabulary of his field, and he tries to communicate effectively with it. As a consequence, his language is terse and full of references to concepts that are foreign to a run-of-the-mill SWE like me ("naturalization", "symbol grounding", "intentional-referential behavior").

Effectiveness of communication is relative, of course, and what is appropriate for an audience may not be appropriate for another. A parallel with programming languages can be drawn here: mainstream language programmers often have a knee-jerk reaction to being told "look, in Haskell, this program that took you 80 lines in your favorite OOP language is just 4 lines of almost only special characters that look like I banged my head on the keyboard!" but it's just a matter of easing into a different language and different concepts.

fauigerzigerk3• 7 years ago

I don't disagree with you in principle, but I read a lot of papers from fields I'm not sufficiently familiar with and I know what that is like.

I also know from my own field that some people like to write for effect rather than effectiveness.

evdev• 7 years ago

The content of this whole wing of thinking is "you have to have a brain-like system to have a brain-like thing". Which, fair. But what's crazy-making about it is that people have decided this sort of insight says something about mathematics and metaphysics, which it does not.

For example, this:

This observation which they refer to as the “hard problem of content” or the “covariance-is-not-content principle” is that systems acting on covariance information, while acting on information, do not constitute content-bearing systems, because to bear content is to embody claims about how things stand, when in fact they merely embody capacities to affect the world.

is just complete nonsense, and to extract the charitable reading I put in quotes above, you have to read closely for paragraph after paragrah to see that what's going on is the word "content" is reserved to mean "things brain-like things do in a brain-like way to other brain-like things in a context built for brain-like things."

Again, okay! But: it's wildly misleading to frame this as being about mathematical logic or the metaphysics of symbols, syntax and semantics.

ppod• 7 years ago

Has the author read Brandom?

lupire• 7 years ago

This nonsensicaly-titled article is somewhere between a rehash of "the map is the not the territory / one cannot pass from the informal to the formal by purely formal means" and Sokal-esque gobbledygook.

otikik• 7 years ago

I couldn't follow this. I'm usually capable of following technical papers. The jargon was thick as a jungle, it seems auto-generated. Use plainer language next time, please.

uryga3• 7 years ago

the title seems to be an unfortunate pun. from a quick look at the article, it's mostly cogsci stuff, where "proposition" has a very different meaning from the one "Propositions as types" normally refers to:

"The proposition is a concept borrowed by cognitive psychologists from linguists and logicians. The propostion is the most basic unit of meaning in a [mental] representation." [1]

the article seems to mostly be talking about AI and the problems of making it "actually refer to the real world". so i think title could be paraphrased as sth like "Information about the world ([mental] propositions) is hard to represent with symbolic, digital things (types)".

[1](http://www.bcp.psych.ualberta.ca/~mike/Pearl_Street/Dictiona...)

nathias• 7 years ago

bad title, good article

Propositions Are Not Types (2018)

Related Stories