3 ms·

But he said type safety, which is entirely compile time and allows you to avoid run time checks, making it faster not slower.

by Sssnake 13y ago

sanxiyn 13y ago
Type safety means well-typed programs can't go wrong. Corrupted memory is surely a case of going wrong, so memory safety is a part of type safety. (In this sense, C, C++, etc. are not type safe.) By the way, it is possible and sometimes preferrable to do all type checks in runtime. Haskell provides this option: https://ghc.haskell.org/trac/ghc/wiki/DeferErrorsToRuntime https://ghc.haskell.org/trac/ghc/wiki/DeferErrorsToRuntime
- Sssnake 13y ago
  Context is cool. With context, you can participate in a conversation, rather than stating an obvious but non-sequitur fact. By definition, type checks are done at compile time. Haskell's defer-type-errors is precisely an example of that. The error is found at compile time, but rather than signal it, the offending code is replaced with an exception.
  - brandonbloom 13y ago
    sanxiyn's comment seems to fully understand the context. Re-read his message in the context of my message. > By definition, type checks are done at compile time. That does not match my definition of type checks. Ignoring things like Typed Racket or clojure.core.typed for a moment. Consider a cast in Java: This is a type safe operation which incurs a runtime type check. Now maybe you're thinking of global type checking for correctness. In which case, I'd still disagree, since there is no rule that you can't have a resident analyzer and run type checks after compilation. Go read about Typed Racket, for example.
    - Sssnake 13y ago
      >sanxiyn's comment seems to fully understand the context No it doesn't, given that the context was specifically runtime checks like array bounds checking, and he replied with a non-sequitur about memory corruption. >That does not match my definition of type checks. That is because "your definition" is incorrect. I am using the actual definition. "Dynamic typing" is a deliberately incorrect name for untyped languages. Runtime checking of value compatibility is not type checking.
      - brandonbloom 13y ago
        1) Surely the most common source of memory corruption is bounds violations. 2) Even reconciling our disagreement on terminology, I still disagree A) that a strict phase separation is a prerequisite for types to exist at all and B) that it even makes sense to talk about "untyped" as if I couldn't just invent a type system (however complex) for proving properties of a particular language that previously had no known type system. The simple fact of the matter is that definitions evolve over time as we learn more about our field. "Type safety" is historically valid phrase for what we now know as "memory safety". In context of the performance claims, it was quite clear what the author meant.
        Sssnake 13y ago
        >Surely the most common source of memory corruption is bounds violations. Surely the most common source of oranges is orange trees. >Even reconciling our disagreement on terminology You aren't reconciling it, you are just repeating "I don't like the real definition of type system in regards to computer science". That's great for you and all, but it has nothing to do with me. If you want to learn about it I can recommend some material, but if you just want to argue "I don't understand X therefore using the correct terminology for X is wrong" then there's no need to continue.

But he said type safety, which is entirely compile time and allows you to avoid run time checks, making it faster not slower.

by Sssnake 13y ago

But he said type safety, which is entirely compile time and allows you to avoid run time checks, making it faster not slower.

sanxiyn 13y ago

Type safety means well-typed programs can't go wrong. Corrupted memory is surely a case of going wrong, so memory safety is a part of type safety. (In this sense, C, C++, etc. are not type safe.) By the way, it is possible and sometimes preferrable to do all type checks in runtime. Haskell provides this option: https://ghc.haskell.org/trac/ghc/wiki/DeferErrorsToRuntime https://ghc.haskell.org/trac/ghc/wiki/DeferErrorsToRuntime

Sssnake 13y ago
Context is cool. With context, you can participate in a conversation, rather than stating an obvious but non-sequitur fact. By definition, type checks are done at compile time. Haskell's defer-type-errors is precisely an example of that. The error is found at compile time, but rather than signal it, the offending code is replaced with an exception.
- brandonbloom 13y ago
  sanxiyn's comment seems to fully understand the context. Re-read his message in the context of my message. > By definition, type checks are done at compile time. That does not match my definition of type checks. Ignoring things like Typed Racket or clojure.core.typed for a moment. Consider a cast in Java: This is a type safe operation which incurs a runtime type check. Now maybe you're thinking of global type checking for correctness. In which case, I'd still disagree, since there is no rule that you can't have a resident analyzer and run type checks after compilation. Go read about Typed Racket, for example.
  - Sssnake 13y ago
    >sanxiyn's comment seems to fully understand the context No it doesn't, given that the context was specifically runtime checks like array bounds checking, and he replied with a non-sequitur about memory corruption. >That does not match my definition of type checks. That is because "your definition" is incorrect. I am using the actual definition. "Dynamic typing" is a deliberately incorrect name for untyped languages. Runtime checking of value compatibility is not type checking.
    - brandonbloom 13y ago
      1) Surely the most common source of memory corruption is bounds violations. 2) Even reconciling our disagreement on terminology, I still disagree A) that a strict phase separation is a prerequisite for types to exist at all and B) that it even makes sense to talk about "untyped" as if I couldn't just invent a type system (however complex) for proving properties of a particular language that previously had no known type system. The simple fact of the matter is that definitions evolve over time as we learn more about our field. "Type safety" is historically valid phrase for what we now know as "memory safety". In context of the performance claims, it was quite clear what the author meant.
      - Sssnake 13y ago
        >Surely the most common source of memory corruption is bounds violations. Surely the most common source of oranges is orange trees. >Even reconciling our disagreement on terminology You aren't reconciling it, you are just repeating "I don't like the real definition of type system in regards to computer science". That's great for you and all, but it has nothing to do with me. If you want to learn about it I can recommend some material, but if you just want to argue "I don't understand X therefore using the correct terminology for X is wrong" then there's no need to continue.