7 ms·

I empathize with this point of view - if not in any other way then in principle. However, as a counterpoint, I'd suggest that encoding all known invariants as

I empathize with this point of view - if not in any other way then in principle. However, as a counterpoint, I'd suggest that encoding all known invariants as types may be prohibitively cumbersome and time-consuming - to the point where writing the program becomes more of an exercise in proofs rather than producing something useful. Often the invariants of a program are implied or can be easily inferred by the reader, which can actually make the program easier to understand for both the reader and the writer by leaving some things unsaid. Of course, whether a program is easier to understand when its invariants are written down vs. when they are left to be inferred by the reader is probably a matter of circumstance, so different tools for different jobs and all that. I've recently been writing a small program in Go - my first foray into the language - and I thoroughly enjoy how it gets out of my way. The lack of rigor is freeing if you don't stop to think about it too much.

ryangs 2y ago
The problem is that user inferring doesn't scale. For small projects this is reasonable but for enterprise software engineering it is easy for a constraint that isn't enforced by the type system to be missed by an engineer leading to a bug. Whereas typed constraints naturally propagate throughout the system.
- mason55 2y ago
  Yeah - in theory they are the same thing. You can have a dependent type that's an array with a length of 5 or you can create a type called ArrayLengthFive, and in both cases the type checker ensures that you don't accidentally use an unbounded array. But the difference is that with a dependent type, you get more guarantees (e.g. my ArrayLengthFive type could actually allow for arrays of length 20!). And the type checker forces you to prove the bounds (there could be a bug in my code when I create an ArrayLengthFive). And the dependent type allows other parts of the system to use the type info, whereas ArrayLengthFive is just an opaque type. I do think there is room for both ways of working. In the string -> Email example, it's probably enough to parse your string and just call it an email. You don't need to try to encode all the rules about an email into the type itself. But there are certainly other cases where it is useful to encode the data constraints into the type so that you can do more operations downstream.
  - bombela 2y ago
    > In the string -> Email example, it's probably enough to parse your string and just call it an email. You don't need to try to encode all the rules about an email into the type itself. There is also the in-between Rust approach. Start with the user input as a byte array. Pass it to a validation function, which returns it encapsulated within a new type. #[derive(Clone, Hash, Ord, Eq...)] struct Email(Box<str>); // validate UTF-8 + fn validate(raw: &[u8]) -> Result<Email, EmailValidationError>; What is annoying is the boilerplate required. You usually want your new type to behave like a (read-only) version of the original type, and you want some error type with various level of details. You can macro your way out of most of the boilerplate, with the downside that it quickly becomes a domain specific language.
    - oasisaimlessly 2y ago
      AKA the "parse, don't validate" approach [1]. 1: https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/ https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va...
      - bombela 2y ago
        The salient excerpt is: "A parser is just a function that consumes less-structured input and produces more-structured output". In opposition to a validation function that merely raises an error. - validate(raw) -> void - parse(raw) -> Email | Error Of course the type signature is what seals the deal at the end of the day. But I am going to follow this naming convention from now on.
  - taeric 2y ago
    Parsing a string into an email, of course, is already fraught with peril. Is it valid HTML? Or did you mean the email address? Is it a well formed email, or a validated address that you have received correspondence with? How long ago was it validated? Fun spin on the, "It's an older code, sir, but it checks out." I've seen attempts at solving each of those issues using types. I am not even positive they aren't solvable.
- joshlemer 2y ago
  But then ironically, the problem with relying on programming language type systems is that they don't scale (beyond the boundaries of a single process). As soon as you are crossing a wire you have to go back to runtime validations.
  - nightski 2y ago
    Throwing out type safety simply because you have unverified input is a little silly. It's trivial in most statically typed languages to safely turn input into a concrete type (or an error if it is invalid) at the edge and meanwhile maintain type safety throughout the rest of the code.
- TuringTest 2y ago
  There's where good documentation and training pays off. Some invariants that are too complex to express purely in code, requiring numerous separate low level bookkeeping functions throughout the system, can be concisely expressed as a high level idea in natural language (wether as comments or at an external technical document). Make sure that your developers are exposed to those documents, throw in a few tests for the most obvious cases to ensure that newcomers are learning the invariants by heart, and if they're competent you should not have problems but in the most obscure cases (that could appear anyway even if you try to formalize everything in code).
- yencabulator 2y ago
  Typed constraints don't scale either. I eagerly await your implementation of a type describing my tax return. And to implement a compiler for the new programming language you'll inevitably have to construct, we're gonna need two types, one expressing all valid source programs, and the other all valid programs for the target platform. Oh, can we also get updates to that for next year's taxes, new platforms, and other such future business needs? Of course the current requirements have to still remain supported.
- wredue 2y ago
  There is no world where the added time here for the developers is with the trade off, and if you look through my history, you will see that I largely reject “dev time trade off” as a notion a company should ever seriously entertain as a significant burden.

ryangs 2y ago

The problem is that user inferring doesn't scale. For small projects this is reasonable but for enterprise software engineering it is easy for a constraint that isn't enforced by the type system to be missed by an engineer leading to a bug. Whereas typed constraints naturally propagate throughout the system.

mason55 2y ago
Yeah - in theory they are the same thing. You can have a dependent type that's an array with a length of 5 or you can create a type called ArrayLengthFive, and in both cases the type checker ensures that you don't accidentally use an unbounded array. But the difference is that with a dependent type, you get more guarantees (e.g. my ArrayLengthFive type could actually allow for arrays of length 20!). And the type checker forces you to prove the bounds (there could be a bug in my code when I create an ArrayLengthFive). And the dependent type allows other parts of the system to use the type info, whereas ArrayLengthFive is just an opaque type. I do think there is room for both ways of working. In the string -> Email example, it's probably enough to parse your string and just call it an email. You don't need to try to encode all the rules about an email into the type itself. But there are certainly other cases where it is useful to encode the data constraints into the type so that you can do more operations downstream.
- bombela 2y ago
  > In the string -> Email example, it's probably enough to parse your string and just call it an email. You don't need to try to encode all the rules about an email into the type itself. There is also the in-between Rust approach. Start with the user input as a byte array. Pass it to a validation function, which returns it encapsulated within a new type. #[derive(Clone, Hash, Ord, Eq...)] struct Email(Box<str>); // validate UTF-8 + fn validate(raw: &[u8]) -> Result<Email, EmailValidationError>; What is annoying is the boilerplate required. You usually want your new type to behave like a (read-only) version of the original type, and you want some error type with various level of details. You can macro your way out of most of the boilerplate, with the downside that it quickly becomes a domain specific language.
  - oasisaimlessly 2y ago
    AKA the "parse, don't validate" approach [1]. 1: https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/ https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va...
    - bombela 2y ago
      The salient excerpt is: "A parser is just a function that consumes less-structured input and produces more-structured output". In opposition to a validation function that merely raises an error. - validate(raw) -> void - parse(raw) -> Email | Error Of course the type signature is what seals the deal at the end of the day. But I am going to follow this naming convention from now on.
- taeric 2y ago
  Parsing a string into an email, of course, is already fraught with peril. Is it valid HTML? Or did you mean the email address? Is it a well formed email, or a validated address that you have received correspondence with? How long ago was it validated? Fun spin on the, "It's an older code, sir, but it checks out." I've seen attempts at solving each of those issues using types. I am not even positive they aren't solvable.
joshlemer 2y ago
But then ironically, the problem with relying on programming language type systems is that they don't scale (beyond the boundaries of a single process). As soon as you are crossing a wire you have to go back to runtime validations.
- nightski 2y ago
  Throwing out type safety simply because you have unverified input is a little silly. It's trivial in most statically typed languages to safely turn input into a concrete type (or an error if it is invalid) at the edge and meanwhile maintain type safety throughout the rest of the code.
TuringTest 2y ago
There's where good documentation and training pays off. Some invariants that are too complex to express purely in code, requiring numerous separate low level bookkeeping functions throughout the system, can be concisely expressed as a high level idea in natural language (wether as comments or at an external technical document). Make sure that your developers are exposed to those documents, throw in a few tests for the most obvious cases to ensure that newcomers are learning the invariants by heart, and if they're competent you should not have problems but in the most obscure cases (that could appear anyway even if you try to formalize everything in code).
yencabulator 2y ago
Typed constraints don't scale either. I eagerly await your implementation of a type describing my tax return. And to implement a compiler for the new programming language you'll inevitably have to construct, we're gonna need two types, one expressing all valid source programs, and the other all valid programs for the target platform. Oh, can we also get updates to that for next year's taxes, new platforms, and other such future business needs? Of course the current requirements have to still remain supported.
wredue 2y ago
There is no world where the added time here for the developers is with the trade off, and if you look through my history, you will see that I largely reject “dev time trade off” as a notion a company should ever seriously entertain as a significant burden.