3 ms·

That's sort of the point though. Contexts where casting is not permitted in that sense are where the types are an integral part of the semantics of the language

That's sort of the point though. Contexts where casting is not permitted in that sense are where the types are an integral part of the semantics of the language and for which it doesn't make sense to speak of "otherwise valid statements" (as indeed is the case here with C++). The original comment's "otherwise valid statements" are precisely UB in C++.

UncleMeat 7y ago
But is there a difference between a statement that is excluded from the language by a non-typing rule and a statement that is excluded from the language by a typing rule? In both cases, the "natural" evaluation could work as the developer intends but some language rule prevents that program from being executed.
- dwohnitmok 7y ago
  Honestly the answer is it depends and needs to be looked at on a language-by-language basis. There's certain languages for which there is no difference between typing rules and non-typing rules. Type-checking is literally the same as syntax checking (this is what I was referring to with a types as macros approach that has an implementation in Racket). There's others where you can try to finesse some sort of Curry-style semantics out of a language that doesn't have those semantics. The crucial question though is to what end? The original contention is that types represent a limitation on a language, a limitation that you might want to sometimes lift. To the extent that you can separate the types from a language itself I agree that's true in theory, but that problem is solvable with casts. And to the extent it isn't solvable with casts, it isn't solvable precisely because the Curry-style interpretation fails and the line between being excluded by a "surface-level" typing rule vs a deeper matter of language semantics is blurred. All that being said, there is an argument to be made that you sometimes want to preserve a Curry-style fragment of your language precisely in order to facilitate this kind of "escape hatch" with a cast However, going back to my original point, at least for me, this isn't something I worry about with mainstream languages. It feels more like a theoretical concern than a practical one. If you have a language with a type system that cares a lot about soundness and expressivity then it's something to keep in mind. I worry in dependently-typed languages that without preserving this distinction between types that have runtime-significance and types that do not, you lack an effective cast escape hatch. For mainstream languages my concerns are exactly the opposite. The type system often is of little use to me because so much code makes use of escape hatches.

UncleMeat 7y ago

But is there a difference between a statement that is excluded from the language by a non-typing rule and a statement that is excluded from the language by a typing rule? In both cases, the "natural" evaluation could work as the developer intends but some language rule prevents that program from being executed.

dwohnitmok 7y ago
Honestly the answer is it depends and needs to be looked at on a language-by-language basis. There's certain languages for which there is no difference between typing rules and non-typing rules. Type-checking is literally the same as syntax checking (this is what I was referring to with a types as macros approach that has an implementation in Racket). There's others where you can try to finesse some sort of Curry-style semantics out of a language that doesn't have those semantics. The crucial question though is to what end? The original contention is that types represent a limitation on a language, a limitation that you might want to sometimes lift. To the extent that you can separate the types from a language itself I agree that's true in theory, but that problem is solvable with casts. And to the extent it isn't solvable with casts, it isn't solvable precisely because the Curry-style interpretation fails and the line between being excluded by a "surface-level" typing rule vs a deeper matter of language semantics is blurred. All that being said, there is an argument to be made that you sometimes want to preserve a Curry-style fragment of your language precisely in order to facilitate this kind of "escape hatch" with a cast However, going back to my original point, at least for me, this isn't something I worry about with mainstream languages. It feels more like a theoretical concern than a practical one. If you have a language with a type system that cares a lot about soundness and expressivity then it's something to keep in mind. I worry in dependently-typed languages that without preserving this distinction between types that have runtime-significance and types that do not, you lack an effective cast escape hatch. For mainstream languages my concerns are exactly the opposite. The type system often is of little use to me because so much code makes use of escape hatches.