5 ms·

I really liked this brief overview of type systems overall, but I especially liked that the author took the effort to move away from the terms "strongly typed"

I really liked this brief overview of type systems overall, but I especially liked that the author took the effort to move away from the terms "strongly typed" and "weakly typed". Too often these terms cause confusion. Even worse is when people confuse them for "statically typed" and "dynamically typed" (respectively), leading to people making claims like "Python is weakly typed" and "C is strongly typed" (which, depending on your definitions, are not true statements). This material wasn't covered in my core curriculum for my CS degrees, which I think is a shame. Some students might find this stuff interesting, and I think introducing it to undergrads at least a little bit and saying "By the way, this is a thing you can research" could help some students with breaking into the academic side of CS.

msla 8y ago
It's more interesting to answer two questions: 1. Can I easily subvert this type system? 2. Can I make this type system map to concepts in the problem domain? In C, the answer to 1 is "yes" and the answer to 2 is "to a limited extent". In fact, in C, you can subvert the type system so easily that it's considered impossible not to, to the extent that using the standard library requires throwing type information away, by using pointers-to-void or generic "char" buffers, and as for the second... well, Apps Hungarian notation exists for a reason. (Systems Hungarian exists for a reason, too, but I'll try to keep the insults out of this post.) https://en.wikipedia.org/wiki/Hungarian_notation https://en.wikipedia.org/wiki/Hungarian_notation The first question is interesting because it tells you if the type system can be used to enforce invariants, and the second question is interesting because it tells you if those invariants will be worth enforcing. If you're writing in Standard Pascal, and your type system enforces array length as a part of array type, well, to quote a metal album: "So Far, So Good... So What?" What does that tell me about whether my program is semantically correct as regards the problem domain? Similarly with enforcing size specification types: Differentiating between a short, an int, and a long tells me Sweet Fanny Adams about what values of those sizes mean in my program. Typing isn't "strong" if it's enforcing rules which ultimately make no sense, and if it's "sound", well, mathematical proofs of something I'm not interested in are themselves uninteresting.
- dllthomas 8y ago
  I'd extend 1 to include "can I easily avoid subverting this type system?" Guarantees are better, but as long as I can get help that's enough for a tool to be useful assuming 2. Regarding 2, I've long complained that the conception of types embedded in many systems (and many heads) is very representational and most of the time we don't actually care about representation. The exceptions I typically mention are where we care a lot about performance, and at system boundaries. We can fit those into your analysis by asserting (reasonably, I think) that in those instances representation starts to be a part of your problem domain.
  - AnimalMuppet 8y ago
    I'd also extend 1 to include "can I subvert this type system when I really need to?" (And to those who would say "You never need to", I don't think you can be quite that dogmatic. The real world includes a lot of unforeseen scenarios...)
    - dllthomas 8y ago
      It's an important question. Systems where you can't ever subvert the type system may be useful in some places (sandboxing) where systems with an escape hatch aren't, and maybe vice-versa (plausibly "in theory", certainly "in practice" IME). The two might be variants of the same underlying language, though - Safe Haskell is at least an attempt in this space; I don't know how well it delivers.
    - munk-a 8y ago
      Aha! I will counter that you never actually want or need to break the type comprehension of your executable but the static analysis of the compiler or dynamic analysis at runtime may be inaccurate with regards to the truth and motivate you to try and subvert it. This may be about what you were thinking when you wrote your comment but I wanted to highlight a small but important difference. I may find a useful bitwise function that takes arguments of type int and really want to execute the same bitwise function on a pair of doubles, in this case the actual type of data I want the function to operate on is "a series of bytes" but the compiler/whatever's typing system may force me to declare the function as taking an IEEE 754 or two's complement integer instead. In these cases the typing system is constraining you from declaring a type safe operation the right way by forcing you to play within a subset of the universe of valid types.
deleted 8y ago
[deleted]

msla 8y ago

It's more interesting to answer two questions: 1. Can I easily subvert this type system? 2. Can I make this type system map to concepts in the problem domain? In C, the answer to 1 is "yes" and the answer to 2 is "to a limited extent". In fact, in C, you can subvert the type system so easily that it's considered impossible not to, to the extent that using the standard library requires throwing type information away, by using pointers-to-void or generic "char" buffers, and as for the second... well, Apps Hungarian notation exists for a reason. (Systems Hungarian exists for a reason, too, but I'll try to keep the insults out of this post.) https://en.wikipedia.org/wiki/Hungarian_notation https://en.wikipedia.org/wiki/Hungarian_notation The first question is interesting because it tells you if the type system can be used to enforce invariants, and the second question is interesting because it tells you if those invariants will be worth enforcing. If you're writing in Standard Pascal, and your type system enforces array length as a part of array type, well, to quote a metal album: "So Far, So Good... So What?" What does that tell me about whether my program is semantically correct as regards the problem domain? Similarly with enforcing size specification types: Differentiating between a short, an int, and a long tells me Sweet Fanny Adams about what values of those sizes mean in my program. Typing isn't "strong" if it's enforcing rules which ultimately make no sense, and if it's "sound", well, mathematical proofs of something I'm not interested in are themselves uninteresting.

dllthomas 8y ago
I'd extend 1 to include "can I easily avoid subverting this type system?" Guarantees are better, but as long as I can get help that's enough for a tool to be useful assuming 2. Regarding 2, I've long complained that the conception of types embedded in many systems (and many heads) is very representational and most of the time we don't actually care about representation. The exceptions I typically mention are where we care a lot about performance, and at system boundaries. We can fit those into your analysis by asserting (reasonably, I think) that in those instances representation starts to be a part of your problem domain.
- AnimalMuppet 8y ago
  I'd also extend 1 to include "can I subvert this type system when I really need to?" (And to those who would say "You never need to", I don't think you can be quite that dogmatic. The real world includes a lot of unforeseen scenarios...)
  - dllthomas 8y ago
    It's an important question. Systems where you can't ever subvert the type system may be useful in some places (sandboxing) where systems with an escape hatch aren't, and maybe vice-versa (plausibly "in theory", certainly "in practice" IME). The two might be variants of the same underlying language, though - Safe Haskell is at least an attempt in this space; I don't know how well it delivers.
  - munk-a 8y ago
    Aha! I will counter that you never actually want or need to break the type comprehension of your executable but the static analysis of the compiler or dynamic analysis at runtime may be inaccurate with regards to the truth and motivate you to try and subvert it. This may be about what you were thinking when you wrote your comment but I wanted to highlight a small but important difference. I may find a useful bitwise function that takes arguments of type int and really want to execute the same bitwise function on a pair of doubles, in this case the actual type of data I want the function to operate on is "a series of bytes" but the compiler/whatever's typing system may force me to declare the function as taking an IEEE 754 or two's complement integer instead. In these cases the typing system is constraining you from declaring a type safe operation the right way by forcing you to play within a subset of the universe of valid types.

deleted 8y ago

[deleted]