3 ms·

> This array of integers is sorted ascendingly, and that index is a valid index into this other array which points to a number between 48 and 58 These are diff

> This array of integers is sorted ascendingly, and that index is a valid index into this other array which points to a number between 48 and 58 These are difficult to encode in a way that lets the compiler check the code that sorts or calculates an index. They are trivial to encode in a way that simply tags the values. I still need to be concerned with making sure my sorting is correct, but that's a very isolated concern. I still find it very useful to know whether I've called a function on the array that depends on it being sorted, and that doesn't require any heavy lifting at all.

jstimpfle 10y ago
I haven't had good experiences with tagging. There are just too many "tags" (often one per line or group of lines). They also have disadvantages in that they separate data which is only different by some aspects, but not most others. (For a simple example, the printing function is not interested in a "safe HTML" Tag. The effort needed for constant tagging and untagging (or using "Stringy" classes, or the cognitive overhead you need to pay if you found a clever way to remove the syntactical burden) is too big except in very few cases.
- dllthomas 10y ago
  > I haven't had good experiences with tagging. Fair enough. I have. > There are just too many "tags" (often one per line or group of lines). Where the burden outweighs the benefit, you always have the freedom of typing things too loosely - to be sure, without something like refinement types, there is a granularity you can easily try for that's just not worthwhile. But that's a pretty different thing than "can't be expressed with mainstream type systems at all." For me, the questions are 1) how far does this type move information in its use through the program, and 2) what part of these are likely to change in ways such that I'll want to be notified about this piece of code here?

jstimpfle 10y ago

I haven't had good experiences with tagging. There are just too many "tags" (often one per line or group of lines). They also have disadvantages in that they separate data which is only different by some aspects, but not most others. (For a simple example, the printing function is not interested in a "safe HTML" Tag. The effort needed for constant tagging and untagging (or using "Stringy" classes, or the cognitive overhead you need to pay if you found a clever way to remove the syntactical burden) is too big except in very few cases.

dllthomas 10y ago
> I haven't had good experiences with tagging. Fair enough. I have. > There are just too many "tags" (often one per line or group of lines). Where the burden outweighs the benefit, you always have the freedom of typing things too loosely - to be sure, without something like refinement types, there is a granularity you can easily try for that's just not worthwhile. But that's a pretty different thing than "can't be expressed with mainstream type systems at all." For me, the questions are 1) how far does this type move information in its use through the program, and 2) what part of these are likely to change in ways such that I'll want to be notified about this piece of code here?