4 ms·

I've never really bought this argument. Casting is the way a programmer can selectively bypass the type system and every typed language I've ever used includes

I've never really bought this argument. Casting is the way a programmer can selectively bypass the type system and every typed language I've ever used includes casting. For Church-typed languages as opposed to Curry-typed languages, it's not even apparent what it would would mean to "preclude otherwise valid statements" because types are a part of the language. It's akin to saying structured programming precludes otherwise valid statements in the language because the lack of goto precludes otherwise valid statements in the language. Sure, but the lack of goto is precisely a facet of the language! For a Church-typed language the types are just another part of syntax (this is more than just theory, Racket shows that a type system can in fact be implemented simply as macros). Invoking Godel here I don't think makes sense. Godel's incompleteness theorems apply to what you can prove about a program with types. The majority of typed programming languages have type systems that are too weak for Godel's incompleteness theorems to apply. And there is no need for a type system to be sound (if thought of as a logical system with programs as proofs via the Curry-Howard isomorphism), again most programming languages' type systems are not sound in this manner. Even with a Curry-style system of semantics, the presence of casting is enough to allow any type system to allow every valid statement in the language (the proof of this is to cast every term to the same type). That being said I am sympathetic to the feeling that "I'm just doing this to satisfy the type checker," a feeling that can show up increasingly frequently for languages with increasingly sophisticated type systems. I would argue this often happens precisely when you take the power of casting away. This is the dark side of "correct by construction" techniques where if the construction technique is devilishly complex, then you're forced to deal with that complexity. But this usually only applies to languages with some amount of dependent typing, which the majority of languages do not have.

UncleMeat 7y ago
Casting is not always permitted in all contexts. In C++, many casts that would be valid on the real machine are undefined behavior in the language, for example.
- dwohnitmok 7y ago
  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.
deleted 7y ago
[deleted]
dwohnitmok 7y ago
I'll post a reply that I wrote to one of parent's comments that was deleted, but I think the parent had some reasonable points. It's slightly tweaked to remove some of the parts that don't really make sense without the other comment's context. You're implicitly assuming a Curry-style semantics to your language. Here's an outline of what I assume you mean. Correct me if I'm wrong. There are effectively two separate languages. Your type-level language and your term-level language. Each of these languages have their own notions of validity. At the type-level, a series of statements is valid if the type checker accepts them. At the term-level a series of statements is valid if the program runs without crashing. There is also some way of associating the two languages together, i.e. type assignment. Given these two languages, we would like for their two notions of validity to coincide. That is it would be great if given a type assignment, the type-level language is valid (type checker accepts it) if and only if the term-level language is valid (program does not crash). The first thing to note is that many (most?) statically typed languages don't have Curry-style semantics. As UncleMeat points out not crashing is not sufficient to be semantically valid in C++. It might just happen not to crash on your machine with a certain set of optimizations and compiler flags. Types play an integral role in what it means for a language to be semantically valid and it doesn't really make sense to consider the language independently of types. For Curry-style languages, there is an indirect linkage to Godel, but the more obvious link is through the halting problem. If type checking is decidable (something you probably want to be true) then your term-level language must be decidable as well if the two languages truly coincide. But then you lose Turing completeness as your first comment points out. The thing is though that no mainstream statically typed language tries to ensure this. All of them allow assigning a type to something that might loop forever or crash. I would argue you're effectively attacking a straw man of a type system. However, I agree with you that "there are times when a type system is too cumbersome, and we must escape it to do useful things." However, this is not something I view as limited to type systems. I view this as true of every facet of programming (and in a greater sense true of every facet of life). Every system must have a way of piercing its assumptions when you as its user have extra knowledge the system does not. This shows up in performance and protection against side-channel attacks (assembly intrinsics, FFI, etc.). This shows up in orchestration tools (yes yes yes it's all good and well to treat infrastructure as immutable and machines like cattle not pets but I would sometimes like to just SSH onto a machine and make some one-off changes!). This shows up in structured programming (once in a very blue moon Python, it would be great if you just gave me a goto/label). The list goes on and on.

UncleMeat 7y ago

Casting is not always permitted in all contexts. In C++, many casts that would be valid on the real machine are undefined behavior in the language, for example.

dwohnitmok 7y ago
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.

deleted 7y ago

[deleted]

dwohnitmok 7y ago

I'll post a reply that I wrote to one of parent's comments that was deleted, but I think the parent had some reasonable points. It's slightly tweaked to remove some of the parts that don't really make sense without the other comment's context. You're implicitly assuming a Curry-style semantics to your language. Here's an outline of what I assume you mean. Correct me if I'm wrong. There are effectively two separate languages. Your type-level language and your term-level language. Each of these languages have their own notions of validity. At the type-level, a series of statements is valid if the type checker accepts them. At the term-level a series of statements is valid if the program runs without crashing. There is also some way of associating the two languages together, i.e. type assignment. Given these two languages, we would like for their two notions of validity to coincide. That is it would be great if given a type assignment, the type-level language is valid (type checker accepts it) if and only if the term-level language is valid (program does not crash). The first thing to note is that many (most?) statically typed languages don't have Curry-style semantics. As UncleMeat points out not crashing is not sufficient to be semantically valid in C++. It might just happen not to crash on your machine with a certain set of optimizations and compiler flags. Types play an integral role in what it means for a language to be semantically valid and it doesn't really make sense to consider the language independently of types. For Curry-style languages, there is an indirect linkage to Godel, but the more obvious link is through the halting problem. If type checking is decidable (something you probably want to be true) then your term-level language must be decidable as well if the two languages truly coincide. But then you lose Turing completeness as your first comment points out. The thing is though that no mainstream statically typed language tries to ensure this. All of them allow assigning a type to something that might loop forever or crash. I would argue you're effectively attacking a straw man of a type system. However, I agree with you that "there are times when a type system is too cumbersome, and we must escape it to do useful things." However, this is not something I view as limited to type systems. I view this as true of every facet of programming (and in a greater sense true of every facet of life). Every system must have a way of piercing its assumptions when you as its user have extra knowledge the system does not. This shows up in performance and protection against side-channel attacks (assembly intrinsics, FFI, etc.). This shows up in orchestration tools (yes yes yes it's all good and well to treat infrastructure as immutable and machines like cattle not pets but I would sometimes like to just SSH onto a machine and make some one-off changes!). This shows up in structured programming (once in a very blue moon Python, it would be great if you just gave me a goto/label). The list goes on and on.