5 ms·

Documentation of data flow and rigorous testing might be an alternative and superior way to get correct answers, at least in some contexts. Just because a type

Documentation of data flow and rigorous testing might be an alternative and superior way to get correct answers, at least in some contexts. Just because a type has been assigned to some data does not mean that is necessarily correct. All input needs to be checked and can have various mistakes, errors, and distortions. Type systems are one method that may help to keep things in check, especially with complex business logic maintained by large and dynamic teams. But if the business logic is well defined and the teams are small then typing can be a digression that takes time and effort without bringing about superior results.

galaxyLogic 3y ago
The way I look at it is that "types" are assertions, which tell us whether our assumptions about the program are correct or not. There is no such thing as a "correct program". There is only our correct or incorrect understanding of what the program is doing. Type-declarations help us gain the understanding about that. Types express data, which allow the assertions to be structured and composite, and express assertions about the real data running through the program when it executes. So "types" in a sense do not exist as such, we are simply writing "predicates" in some formal language. Whether those predicates are checked at compile-time or run-time is a separate question. The reason many people assume that 'types' are a thing is that when using a "statically typed" language you are required to enter them always, and therefore they take on more or less existence of their own. Using a typed programming language you are always writing TWO programs, one that does what you want it to do, and another that observes and verifies the code's adherence to your assumptions about it. Thus types are a secondary utility, they are a harness that limits what your program can do. Types help you to better understand and to gain trust in your understanding of your program.
malcolmgreaves 3y ago
I agree that documentation is important. There's several methods by which we can communicate program semantics. I firmly believe that it's important to do this. For instance, there can be bugs in how the types are specified that don't align to what one wants. This is where written technical documentation or a specification can be incredibly useful. I'd like to hone in on the specific example you bring up to push back against the value of strongly and statically typed programs: > All input needs to be checked and can have various mistakes, errors, and distortions. This is something that should always be 100% represented in the type system. Input validation is something where the value of typing is probably at its best (in my opinion, at least). Input validation is a function that accepts data of some "raw" type and then produces a value of the "clean" type -- or an error. This is `raw --> (clean | error)`. If you're calling this kind of function, you will always need to include logic for handling both possibilities. Not doing so is a mistake. Think of a compiler: it accepts many text files (or strings thereof) and produces either a binary program or a list of errors. > But if the business logic is well defined and the teams are small then typing can be a digression that takes time and effort without bringing about superior results. Some programming languages have rather useless static type systems, where they will rely on exceptions. Perhaps this is the experience that you're drawing on? I would like to make minimal assumptions here, but I acknowledge that I hear this kind of line of thinking a lot when I talk to folks that have have only used statically typed languages like Java. I'll pick on Java for a bit, but there are more languages with weak static typing that this applies to. Java's type system is a real shame. It's very verbose and it doesn't do much useful work beyond very simple things. A major reason for this is because of the language designer's decision to make extensive use of exceptions. Even checked exceptions are a pain to deal with: they're not regular values, forcing programmers to use completely different syntax to deal with them. These poor ergonomics caused people to reach for unchecked exceptions. (Unchecked == every single exception that can be raised in Python, if that comparison helps.) Unchecked exceptions may provide runtime safety, but at the expense of making code verbose while also making it not actually handle the problem. It's a concept that needs to be used sparingly. Array index out of bounds? Sure. Your input validation failed? Terrible. Much of programming -- in the large or small -- needs to deal with the possibility of an action failing. It's a mistake to write code that can perform a failing operation without checking to see if it does fail. > digression that takes time and effort without bringing about superior results. I'd also like to focus on this part a bit. There are many good programming languages that have type inference. At some point, one always has to write the types of something. It may be obvious, such as e.g. `var x = 10`: we know that `10` is an `int`, so it's trivially clear that `x` is an `int` too. Good type systems are designed to push this idea as far as possible. If you're using a function that requires particular operations on its input, a type checker can see these constraints and infer the right type. Similarly, if the output of a function is used in a particular way, the type checker can see this and make inferences. There are statically typed programming languages where writing down types is actually fairly rare. They're usually only necessary at a few key points. Or necessary to add specific constraints to ensure that a particular thing is only used in a more specific way. For example, you may have a language where an operator like `+` is defined for both floating point and integer division as well as concatenating strings and lists together. You may write something like `def add(x) = x + x`, which could be inferred to be ok to work with anything where `+` is defined. But, you may actually want to ensure that this actually only works for floating point numbers, so you put in a `x: float` in the parameter list. You might want to do this so that your compiler can realize that it can implement this `add` function using very fast floating point hardware instructions.

galaxyLogic 3y ago

The way I look at it is that "types" are assertions, which tell us whether our assumptions about the program are correct or not. There is no such thing as a "correct program". There is only our correct or incorrect understanding of what the program is doing. Type-declarations help us gain the understanding about that. Types express data, which allow the assertions to be structured and composite, and express assertions about the real data running through the program when it executes. So "types" in a sense do not exist as such, we are simply writing "predicates" in some formal language. Whether those predicates are checked at compile-time or run-time is a separate question. The reason many people assume that 'types' are a thing is that when using a "statically typed" language you are required to enter them always, and therefore they take on more or less existence of their own. Using a typed programming language you are always writing TWO programs, one that does what you want it to do, and another that observes and verifies the code's adherence to your assumptions about it. Thus types are a secondary utility, they are a harness that limits what your program can do. Types help you to better understand and to gain trust in your understanding of your program.

malcolmgreaves 3y ago

I agree that documentation is important. There's several methods by which we can communicate program semantics. I firmly believe that it's important to do this. For instance, there can be bugs in how the types are specified that don't align to what one wants. This is where written technical documentation or a specification can be incredibly useful. I'd like to hone in on the specific example you bring up to push back against the value of strongly and statically typed programs: > All input needs to be checked and can have various mistakes, errors, and distortions. This is something that should always be 100% represented in the type system. Input validation is something where the value of typing is probably at its best (in my opinion, at least). Input validation is a function that accepts data of some "raw" type and then produces a value of the "clean" type -- or an error. This is `raw --> (clean | error)`. If you're calling this kind of function, you will always need to include logic for handling both possibilities. Not doing so is a mistake. Think of a compiler: it accepts many text files (or strings thereof) and produces either a binary program or a list of errors. > But if the business logic is well defined and the teams are small then typing can be a digression that takes time and effort without bringing about superior results. Some programming languages have rather useless static type systems, where they will rely on exceptions. Perhaps this is the experience that you're drawing on? I would like to make minimal assumptions here, but I acknowledge that I hear this kind of line of thinking a lot when I talk to folks that have have only used statically typed languages like Java. I'll pick on Java for a bit, but there are more languages with weak static typing that this applies to. Java's type system is a real shame. It's very verbose and it doesn't do much useful work beyond very simple things. A major reason for this is because of the language designer's decision to make extensive use of exceptions. Even checked exceptions are a pain to deal with: they're not regular values, forcing programmers to use completely different syntax to deal with them. These poor ergonomics caused people to reach for unchecked exceptions. (Unchecked == every single exception that can be raised in Python, if that comparison helps.) Unchecked exceptions may provide runtime safety, but at the expense of making code verbose while also making it not actually handle the problem. It's a concept that needs to be used sparingly. Array index out of bounds? Sure. Your input validation failed? Terrible. Much of programming -- in the large or small -- needs to deal with the possibility of an action failing. It's a mistake to write code that can perform a failing operation without checking to see if it does fail. > digression that takes time and effort without bringing about superior results. I'd also like to focus on this part a bit. There are many good programming languages that have type inference. At some point, one always has to write the types of something. It may be obvious, such as e.g. `var x = 10`: we know that `10` is an `int`, so it's trivially clear that `x` is an `int` too. Good type systems are designed to push this idea as far as possible. If you're using a function that requires particular operations on its input, a type checker can see these constraints and infer the right type. Similarly, if the output of a function is used in a particular way, the type checker can see this and make inferences. There are statically typed programming languages where writing down types is actually fairly rare. They're usually only necessary at a few key points. Or necessary to add specific constraints to ensure that a particular thing is only used in a more specific way. For example, you may have a language where an operator like `+` is defined for both floating point and integer division as well as concatenating strings and lists together. You may write something like `def add(x) = x + x`, which could be inferred to be ok to work with anything where `+` is defined. But, you may actually want to ensure that this actually only works for floating point numbers, so you put in a `x: float` in the parameter list. You might want to do this so that your compiler can realize that it can implement this `add` function using very fast floating point hardware instructions.