6 ms·

> You can't free yourself from thinking in terms of languages Now would I want to. Why would I deprive myself of the benefits of compositionality, separation o

> You can't free yourself from thinking in terms of languages Now would I want to. Why would I deprive myself of the benefits of compositionality, separation of concerns, or simply modeling the problem domain as faithfully as possible? > For meaning you have to pay real, measurable complexity. Complexity in the sense of complexity theory? I don't see how. If you mean the computational cost of type checking, that's in practice a non-problem as long as the type system is reasonable. (By which I mean: Types are first-order and there is no type-level computation beyond synonym expansion, so plain first-order unification can reconstruct out all the types. Damas-Milner is a special case of this.) Or are you talking about complexity in some other sense? I don't see the requirement of making sense as a burden. I'd feel burdened if I had to deal with some random computation I found in the wild, with no indication regarding what its meaning is.

pron 10y ago
> Now would I want to. Why would I deprive myself of the benefits of compositionality, separation of concerns, or simply modeling the problem domain as closely as possible? But now you're saying that you are interested in programming. TOC is about something else. > Complexity in the sense of complexity theory? Yes. > that's in practice a non-problem as long as the type system is reasonable. Whether that's an issue for the questions you're interested in asking doesn't define what "in practice" means. It certainly matters for the questions TOC is asking. A model that requires a computationally powerful collaborator -- a programmer -- can't arise spontaneously in nature, for example. > I don't see the requirement of making sense as a burden. Again, burden is a question of meaning (proof: you need an agent for something to be a burden for). The requirement, however, shows that the different models are objectively, essentially and radically different.
- catnaroek 10y ago
  > But now you're saying that you are interested in programming. TOC is about something else. (...) A model that requires a computationally powerful collaborator -- a programmer -- can't arise spontaneously in nature, for example. If you're trying to argue that “computation” is a physical phenomenon in the same sense gravity or electromagnetism are, I have bad news for you: it isn't. The theory of computation, just like information theory and probability theory, is first and foremost a mathematical theory: It is a priori only constrained by the requirement to be logically consistent. This is very different to what happens with a theory of gravitation or electromagnetism, which has to match external observations. > > Complexity in the sense of complexity theory? > Yes. Elaborate. > Whether that's an issue for the questions you're interested in asking doesn't define what "in practice" means. In practice, when I submit a Standard ML program to a REPL, the REPL tells me almost instantly whether my program is typable or not. > Again, burden is a question of meaning (proof: you need an agent for something to be a burden for). The requirement, however, shows that the different models are objectively, essentially and radically different. Agreed. Only one of the theories is actually useful. (Urgh, it's not a model in the logician's sense!)
  - pron 10y ago
    > If you're trying to argue that “computation” is a physical phenomenon in the same sense gravity or electromagnetism are, I have bad news for you: it isn't. Don't know what you mean by "in the same sense", but Turing, von Neumann, Gödel and Hartmanis would have been saddened by your news because they thought (I guess Hartmanis still does) differently. So did Church. The very idea of algorithms -- as Church writes in his review of Turing's paper -- contains a notion of physical realizability. The idea of un/decidability -- only intuitively touched upon in Church's paper, and pretty thoroughly discussed in Turing's -- is predicated on the notion that a computational step takes at least some constant amount of physical time. It is true that a computation isn't a specific physical phenomenon like gravity, but a general, abstract phenomenon, that can be realized in different ways. But if it can't be realized, then it isn't considered computation, unless the people discussing it exclaim very clearly that they're discussing hypothetical computation. Some people take it further and say that not only computation is physical, but as it is meant to model the work of the mathematician, it grounds all of math in the physical along with it, and things that can't be feasibly computed (in some reasonable amount of time) should be left outside the realm of math. You may have heard this story by Harvey Friedman about the ultrafinitist Alexander Esenin-Volpin who attended his lecture[1], and Paul Cockshott from the Univeristy of Glasgow writes this[2]: > Turing starts a philosophical tradition of grounding mathematics on the material and hence ultimately on what can be allowed by the laws of physics. The truth of mathematics become truths like those of any other science — statements about sets of possible configurations of matter. So the truths of arithmetic are predictions about the behaviour of actual physical calculating systems, whether these be children with chalks and slates or microprocessors. In this view it makes no more sense to view mathematical abstractions as Platonic ideals than it does to posit the existence of ideal doors and cups of which actual doors and cups are partial manifestations. Mathematics then becomes a technology of modeling one part of the material world with another. As to the rest, there's much more to computation than programming, and your personal line of work is not the definition of utility. [1]: https://en.wikipedia.org/wiki/Alexander_Esenin-Volpin#Mathematical_work https://en.wikipedia.org/wiki/Alexander_Esenin-Volpin#Mathem... [2]: http://blogs.nature.com/soapboxscience/2012/06/20/turing-the-irruption-of-materialism-into-thought http://blogs.nature.com/soapboxscience/2012/06/20/turing-the...

pron 10y ago

> Now would I want to. Why would I deprive myself of the benefits of compositionality, separation of concerns, or simply modeling the problem domain as closely as possible? But now you're saying that you are interested in programming. TOC is about something else. > Complexity in the sense of complexity theory? Yes. > that's in practice a non-problem as long as the type system is reasonable. Whether that's an issue for the questions you're interested in asking doesn't define what "in practice" means. It certainly matters for the questions TOC is asking. A model that requires a computationally powerful collaborator -- a programmer -- can't arise spontaneously in nature, for example. > I don't see the requirement of making sense as a burden. Again, burden is a question of meaning (proof: you need an agent for something to be a burden for). The requirement, however, shows that the different models are objectively, essentially and radically different.

catnaroek 10y ago
> But now you're saying that you are interested in programming. TOC is about something else. (...) A model that requires a computationally powerful collaborator -- a programmer -- can't arise spontaneously in nature, for example. If you're trying to argue that “computation” is a physical phenomenon in the same sense gravity or electromagnetism are, I have bad news for you: it isn't. The theory of computation, just like information theory and probability theory, is first and foremost a mathematical theory: It is a priori only constrained by the requirement to be logically consistent. This is very different to what happens with a theory of gravitation or electromagnetism, which has to match external observations. > > Complexity in the sense of complexity theory? > Yes. Elaborate. > Whether that's an issue for the questions you're interested in asking doesn't define what "in practice" means. In practice, when I submit a Standard ML program to a REPL, the REPL tells me almost instantly whether my program is typable or not. > Again, burden is a question of meaning (proof: you need an agent for something to be a burden for). The requirement, however, shows that the different models are objectively, essentially and radically different. Agreed. Only one of the theories is actually useful. (Urgh, it's not a model in the logician's sense!)
- pron 10y ago
  > If you're trying to argue that “computation” is a physical phenomenon in the same sense gravity or electromagnetism are, I have bad news for you: it isn't. Don't know what you mean by "in the same sense", but Turing, von Neumann, Gödel and Hartmanis would have been saddened by your news because they thought (I guess Hartmanis still does) differently. So did Church. The very idea of algorithms -- as Church writes in his review of Turing's paper -- contains a notion of physical realizability. The idea of un/decidability -- only intuitively touched upon in Church's paper, and pretty thoroughly discussed in Turing's -- is predicated on the notion that a computational step takes at least some constant amount of physical time. It is true that a computation isn't a specific physical phenomenon like gravity, but a general, abstract phenomenon, that can be realized in different ways. But if it can't be realized, then it isn't considered computation, unless the people discussing it exclaim very clearly that they're discussing hypothetical computation. Some people take it further and say that not only computation is physical, but as it is meant to model the work of the mathematician, it grounds all of math in the physical along with it, and things that can't be feasibly computed (in some reasonable amount of time) should be left outside the realm of math. You may have heard this story by Harvey Friedman about the ultrafinitist Alexander Esenin-Volpin who attended his lecture[1], and Paul Cockshott from the Univeristy of Glasgow writes this[2]: > Turing starts a philosophical tradition of grounding mathematics on the material and hence ultimately on what can be allowed by the laws of physics. The truth of mathematics become truths like those of any other science — statements about sets of possible configurations of matter. So the truths of arithmetic are predictions about the behaviour of actual physical calculating systems, whether these be children with chalks and slates or microprocessors. In this view it makes no more sense to view mathematical abstractions as Platonic ideals than it does to posit the existence of ideal doors and cups of which actual doors and cups are partial manifestations. Mathematics then becomes a technology of modeling one part of the material world with another. As to the rest, there's much more to computation than programming, and your personal line of work is not the definition of utility. [1]: https://en.wikipedia.org/wiki/Alexander_Esenin-Volpin#Mathematical_work https://en.wikipedia.org/wiki/Alexander_Esenin-Volpin#Mathem... [2]: http://blogs.nature.com/soapboxscience/2012/06/20/turing-the-irruption-of-materialism-into-thought http://blogs.nature.com/soapboxscience/2012/06/20/turing-the...