11 ms·

> It emerges from the underlying mathematics. Which mathematics? (Lisp has its own math, for instance.)

mjburgess 9y ago
What on earth are you talking about? > The internet is dynamically typed. That's an incoherent claim. Dynamic typing is where types belong to values. Static typing is where they apply to terms. Really to call the former "typing" is misnomer. It's an abuse of the word "type" to mean "memory mode". It has not much relationship to typing in the logic/math/philosophy of logic sense in which types are sets and type relationships are those between sets. It is the Curry-Howard isomorphism (https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...) which defines the correspondance between types in computer science and mathematics. This is "static" only because the "dynamic" alternative isnt really an alternative at all, and really just a different kind of thing all together.
- dang 9y ago
  This crosses into incivility. That breaks the site guidelines. Please re-read them and don't do that when commenting here. https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html
  - mjburgess 9y ago
    I'm not sure how this is incivil? The claim is logically incoherent: typing cannot be a property of the internet, in the same way tuesday cannot be pink nor can addition sound terrifying. The claim is a category error: the internet cannot posses such a property. In addition, to say, of something, that it is " is a made up thing " is a degree of hubris that is presumably reasonably met by being perplexed at overconfidence of the claim posed with such little correct information. Is being perplexed more uncivil than hubris? Are we really policing people's language to this minute degree?
    - dang 9y ago
      "What on earth are you talking about" is uncivil. Your comment didn't need that. Actually you broke this guideline as well: "Please respond to the strongest plausible interpretation of what someone says, not a weaker one that's easier to criticize." It's possible that shalabhc intended to make a mathematical claim, but a stronger plausible interpretation is easy to come up with (e.g. "it's hard to enforce static guarantees across the software that interoperates on the internet"). The reason we ask people to follow this guideline is not so much that it's nicer, but that nitpicking things each other probably didn't say is tedious and detracts from good conversation, which is what we're really hoping for.
Silfen 9y ago
Very fundamental ideas around computability, or total vs partial functions. There are some correctness properties that we can prove without running the underlying program, such that we can always accept or reject a given program. None of this is particular to lisp.
- shalabhc 9y ago
  Fundamental ideas about computability include the model of the Turing machine, which has no notion of types, verification, or even functions whatsoever - there are just too many degrees of freedom. I agree there are correctness properties we can prove without running a 'program', but how do we map the notion of a 'program' into the real world. Is a single function a program? A single module which includes multiple functions? A single executable? A single system that includes multiple processes communicating over a network? I'm arguing each of these is a 'program' and a Turing machine in the theoretical sense. Each of these programs is hooked up to other 'programs' outside of it. 'Compilation' requires the input to be static, but if we think about how things are in flux (you can change a function, switch out a shared library or upgrade and restart a running process, etc.) when do you verify that a 'program' is 'correct'? This is what I mean by 'compile time is made-up' - it falls out of the current frame of thinking of one OS process = one program = static set of source files. It is possible to design systems that have no notion of 'compile time'. You could still have verification, but it could be incremental and spread out all through the lifetime of the running system. So the system would have no 'compile phase' - it would be running live and as you update parts of it, the updated parts would integrate with the rest of the system and do verification like things.

What on earth are you talking about? > The internet is dynamically typed. That's an incoherent claim. Dynamic typing is where types belong to values. Static typing is where they apply to terms. Really to call the former "typing" is misnomer. It's an abuse of the word "type" to mean "memory mode". It has not much relationship to typing in the logic/math/philosophy of logic sense in which types are sets and type relationships are those between sets. It is the Curry-Howard isomorphism (https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...) which defines the correspondance between types in computer science and mathematics. This is "static" only because the "dynamic" alternative isnt really an alternative at all, and really just a different kind of thing all together.

dang 9y ago
This crosses into incivility. That breaks the site guidelines. Please re-read them and don't do that when commenting here. https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html
- mjburgess 9y ago
  I'm not sure how this is incivil? The claim is logically incoherent: typing cannot be a property of the internet, in the same way tuesday cannot be pink nor can addition sound terrifying. The claim is a category error: the internet cannot posses such a property. In addition, to say, of something, that it is " is a made up thing " is a degree of hubris that is presumably reasonably met by being perplexed at overconfidence of the claim posed with such little correct information. Is being perplexed more uncivil than hubris? Are we really policing people's language to this minute degree?
  - dang 9y ago
    "What on earth are you talking about" is uncivil. Your comment didn't need that. Actually you broke this guideline as well: "Please respond to the strongest plausible interpretation of what someone says, not a weaker one that's easier to criticize." It's possible that shalabhc intended to make a mathematical claim, but a stronger plausible interpretation is easy to come up with (e.g. "it's hard to enforce static guarantees across the software that interoperates on the internet"). The reason we ask people to follow this guideline is not so much that it's nicer, but that nitpicking things each other probably didn't say is tedious and detracts from good conversation, which is what we're really hoping for.

Silfen 9y ago

Very fundamental ideas around computability, or total vs partial functions. There are some correctness properties that we can prove without running the underlying program, such that we can always accept or reject a given program. None of this is particular to lisp.

shalabhc 9y ago
Fundamental ideas about computability include the model of the Turing machine, which has no notion of types, verification, or even functions whatsoever - there are just too many degrees of freedom. I agree there are correctness properties we can prove without running a 'program', but how do we map the notion of a 'program' into the real world. Is a single function a program? A single module which includes multiple functions? A single executable? A single system that includes multiple processes communicating over a network? I'm arguing each of these is a 'program' and a Turing machine in the theoretical sense. Each of these programs is hooked up to other 'programs' outside of it. 'Compilation' requires the input to be static, but if we think about how things are in flux (you can change a function, switch out a shared library or upgrade and restart a running process, etc.) when do you verify that a 'program' is 'correct'? This is what I mean by 'compile time is made-up' - it falls out of the current frame of thinking of one OS process = one program = static set of source files. It is possible to design systems that have no notion of 'compile time'. You could still have verification, but it could be incremental and spread out all through the lifetime of the running system. So the system would have no 'compile phase' - it would be running live and as you update parts of it, the updated parts would integrate with the rest of the system and do verification like things.