5 ms·

"Compile time" is artificial, but the difference between static and dynamic is natural (in some sense, I realize these words are quite slippery). It emerges fro

by Silfen 9y ago

"Compile time" is artificial, but the difference between static and dynamic is natural (in some sense, I realize these words are quite slippery). It emerges from the underlying mathematics. There's a real difference between correctness properties that I can prove without running my program and correctness properties that will introduce failures at runtime.

shalabhc 9y ago
> 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.
sparkie 9y ago
You're using a dynamic language (bash) to invoke your statically-typed-language-compiler and then to also invoke the binary it produces. But what's the difference to say, having just a single dynamically typed language with library functions "type-check-my-code", which returns an encapsulated value, and "run-my-typechecked-code" which takes the encapsulated value as input? The whole process happens at "runtime" here. The artificial static/runtime boundary is introduced by the way Unix implements files and processes. All statically typed languages are effectively supersets of the language of Unix. In Unix we can treat each executable binary as a library function (except that we have a massive overhead for calling it). The designers of Unix were well aware of this which is why from the POV of bash, there's no distinction between invoking a binary and invoking another script written in bash. How much of the Unix binary and process bloat is really necessary though to say, concatenate N files? Even someone writing a C program will avoid calling cat and instead implement it themselves, or call a library that does it. Perhaps we need to reconsider where the boundary between type checking and running code should be.
- xfer 9y ago
  runtime here means the runtime of target program, it has nothing to do with unix. If your program fails while executing due to a type error, it's not static type-checking.
  - shalabhc 9y ago
    I think sparkie has a very valid point. It has to do with Unix because a 'program' in Unix has specific meaning (and Windows is no different in this regard, btw). A Unix program doesn't map exactly to what a program means in the theoretical sense. E.g. two Unix processes talking over a socket are not thought of as single Unix program, even though they can be considered a single theoretical program. So there is a tendency to think in 'processes' not 'systems'. I elaborated a little more about this elsewhere in this thread (https://news.ycombinator.com/item?id=15581591 https://news.ycombinator.com/item?id=15581591).
    - xfer 9y ago
gnulinux 9y ago
There certainly is a fundamental difference between what programmers refer to as compile-time and runtime. Naming is probably problematic; but mathematically you cannot prove all the properties of a program just by looking at its syntax, in general. Because this implies a solution to the halting problem. In other words, there is no program, given your program, that can verify it; whereas, there exists a program, given an input and your program, that can verify that your program outputs the correct thing (as long as the language can be emulated by a Turing machine). When it comes to programming languages, the distinction can be trickier, since you can technically get a python program and statically analyze it. So, "compile" time and "run"time are not necessarily perfect words but they belong to the programming terminology. The more crucial thing is, there is a mathematical difference between those two.
- loup-vaillant 9y ago
  > mathematically you cannot prove all the properties of a program just by looking at its syntax, in general. A solution that is often overlooked is to simply shrink the set of legal programs. Simply typed lambda calculus for instance has a perfectly decidable halting problem (which is, programs written in it always halt). There are 2 ways to handle undecidable properties with static analysis: either reject programs for which you can't prove the property holds (you will reject correct programs), or accept programs for which you can't prove it doesn't (you will accept incorrect programs, and may use runtime checks to compensate). Rejecting correct programs is a problem only to the extent one would like to write such a program in the first place. Take this expression for instance: if 2 + 2 = 4 then "Yay!" else 0 It is a perfectly fine expression, of type `string`. Most type systems will reject it however because the two branches of the conditional don't have the same type. Thing is, we don't care about this program in practice, since the constant test expression screams code smell to begin with.
  - gnulinux 9y ago
    Yeah, but now you're arguing something else. Simply typed lambda calculus is not Turing-complete. With a Turing-complete language, you cannot decide the halting problem of an arbitrary sentence of that language. With a non-Turing-complete one, you potentially can. For example, Charity is one such non-Turing-complete language, for which, hypothetically, one can find an algorithm to decide halting of an arbitrary program. But most languages today are Turing-complete, because TC is a very easy property not to have, and it is very hard to construct non-TC but useful languages (eg, C++ metaprogramming is accidentally Turing complete, so is HTML+CSS). So, while what you explained is correct, it does not have direct implications on languages like Python, C++ etc. We still have different sort of properties while we're statically analyzing a TC language, and executing it with an input. This was what I was trying to explain.

by Silfen 9y ago

shalabhc 9y ago

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

sparkie 9y ago

You're using a dynamic language (bash) to invoke your statically-typed-language-compiler and then to also invoke the binary it produces. But what's the difference to say, having just a single dynamically typed language with library functions "type-check-my-code", which returns an encapsulated value, and "run-my-typechecked-code" which takes the encapsulated value as input? The whole process happens at "runtime" here. The artificial static/runtime boundary is introduced by the way Unix implements files and processes. All statically typed languages are effectively supersets of the language of Unix. In Unix we can treat each executable binary as a library function (except that we have a massive overhead for calling it). The designers of Unix were well aware of this which is why from the POV of bash, there's no distinction between invoking a binary and invoking another script written in bash. How much of the Unix binary and process bloat is really necessary though to say, concatenate N files? Even someone writing a C program will avoid calling cat and instead implement it themselves, or call a library that does it. Perhaps we need to reconsider where the boundary between type checking and running code should be.

xfer 9y ago
runtime here means the runtime of target program, it has nothing to do with unix. If your program fails while executing due to a type error, it's not static type-checking.
- shalabhc 9y ago
  I think sparkie has a very valid point. It has to do with Unix because a 'program' in Unix has specific meaning (and Windows is no different in this regard, btw). A Unix program doesn't map exactly to what a program means in the theoretical sense. E.g. two Unix processes talking over a socket are not thought of as single Unix program, even though they can be considered a single theoretical program. So there is a tendency to think in 'processes' not 'systems'. I elaborated a little more about this elsewhere in this thread (https://news.ycombinator.com/item?id=15581591 https://news.ycombinator.com/item?id=15581591).
  - xfer 9y ago

gnulinux 9y ago

There certainly is a fundamental difference between what programmers refer to as compile-time and runtime. Naming is probably problematic; but mathematically you cannot prove all the properties of a program just by looking at its syntax, in general. Because this implies a solution to the halting problem. In other words, there is no program, given your program, that can verify it; whereas, there exists a program, given an input and your program, that can verify that your program outputs the correct thing (as long as the language can be emulated by a Turing machine). When it comes to programming languages, the distinction can be trickier, since you can technically get a python program and statically analyze it. So, "compile" time and "run"time are not necessarily perfect words but they belong to the programming terminology. The more crucial thing is, there is a mathematical difference between those two.

loup-vaillant 9y ago
> mathematically you cannot prove all the properties of a program just by looking at its syntax, in general. A solution that is often overlooked is to simply shrink the set of legal programs. Simply typed lambda calculus for instance has a perfectly decidable halting problem (which is, programs written in it always halt). There are 2 ways to handle undecidable properties with static analysis: either reject programs for which you can't prove the property holds (you will reject correct programs), or accept programs for which you can't prove it doesn't (you will accept incorrect programs, and may use runtime checks to compensate). Rejecting correct programs is a problem only to the extent one would like to write such a program in the first place. Take this expression for instance: if 2 + 2 = 4 then "Yay!" else 0 It is a perfectly fine expression, of type `string`. Most type systems will reject it however because the two branches of the conditional don't have the same type. Thing is, we don't care about this program in practice, since the constant test expression screams code smell to begin with.
- gnulinux 9y ago
  Yeah, but now you're arguing something else. Simply typed lambda calculus is not Turing-complete. With a Turing-complete language, you cannot decide the halting problem of an arbitrary sentence of that language. With a non-Turing-complete one, you potentially can. For example, Charity is one such non-Turing-complete language, for which, hypothetically, one can find an algorithm to decide halting of an arbitrary program. But most languages today are Turing-complete, because TC is a very easy property not to have, and it is very hard to construct non-TC but useful languages (eg, C++ metaprogramming is accidentally Turing complete, so is HTML+CSS). So, while what you explained is correct, it does not have direct implications on languages like Python, C++ etc. We still have different sort of properties while we're statically analyzing a TC language, and executing it with an input. This was what I was trying to explain.