Well, I meant "high-level" in the sense of "closer to my mental representation of the problem, as opposed to the computer's representation of the problem as a bunch of bits". It so happens in this case that my mental representation of the types concerned can be implemented without using especially advanced type-system features.
Here's the thing. In untyped languages (like, er, BCPL), you can treat a variable containing an integer as if it were a character, or a pointer: if you do this and are less clever than you think you are, Bad Things happen. There are two ways to address this: either scan your program at compile-time, eliminating all such problematic usages, or track types at run-time, and perform error-correction when necessary. Both of these strategies eliminate the problem completely (though possibly introduce less severe problems as side-effects). This kind of thing is what I'm calling "low-level" typechecking: preventing problems that arise from misusing the computer's representations of data.
At the other end of the scale, we have something more interesting, and that's what I've called "high-level" typechecking: encoding your understanding of the "types" concerned into your program, and reasoning about correctness (automatically, or in your head) using this information.
So that's what I was talking about :-)
Now, in the normal distribution example, I wouldn't have needed to reason typefully if I were doing it myself - it's simple/well-known enough that I'd have just written down the right expressions. If anything, I'd have had a picture of a bell curve in my head and reasoned geometrically. But it was interesting that my student was making errors that could be caught by (high-level) type-checking, and perhaps more interesting that that was the first way that occurred to me to show to him why he was wrong! :-)
This is related to your point 1: in a problem like this, where we have only three types and not much code to write, the effort of coding up the necessary typechecks probably isn't worth it. Similarly, in your average short system-administration script, your high-level types might be "filename", "directory", "md5 hash", and "map of filenames to hashes" (represented as strings, strings, strings, and string to string hashes): simple enough to keep everything in your head. But if you additionally have to worry about the low-level types, you have to think about eight types at once, which is getting a bit more uncomfortable.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
no subject
Here's the thing. In untyped languages (like, er, BCPL), you can treat a variable containing an integer as if it were a character, or a pointer: if you do this and are less clever than you think you are, Bad Things happen. There are two ways to address this: either scan your program at compile-time, eliminating all such problematic usages, or track types at run-time, and perform error-correction when necessary. Both of these strategies eliminate the problem completely (though possibly introduce less severe problems as side-effects). This kind of thing is what I'm calling "low-level" typechecking: preventing problems that arise from misusing the computer's representations of data.
At the other end of the scale, we have something more interesting, and that's what I've called "high-level" typechecking: encoding your understanding of the "types" concerned into your program, and reasoning about correctness (automatically, or in your head) using this information.
So that's what I was talking about :-)
Now, in the normal distribution example, I wouldn't have needed to reason typefully if I were doing it myself - it's simple/well-known enough that I'd have just written down the right expressions. If anything, I'd have had a picture of a bell curve in my head and reasoned geometrically. But it was interesting that my student was making errors that could be caught by (high-level) type-checking, and perhaps more interesting that that was the first way that occurred to me to show to him why he was wrong! :-)
This is related to your point 1: in a problem like this, where we have only three types and not much code to write, the effort of coding up the necessary typechecks probably isn't worth it. Similarly, in your average short system-administration script, your high-level types might be "filename", "directory", "md5 hash", and "map of filenames to hashes" (represented as strings, strings, strings, and string to string hashes): simple enough to keep everything in your head. But if you additionally have to worry about the low-level types, you have to think about eight types at once, which is getting a bit more uncomfortable.