5 ms·

There are plenty of languages that let you type without having to "type" out a type definition, auto types in C++, type inference in Haskell. Probably most of m

by foxes 5y ago

There are plenty of languages that let you type without having to "type" out a type definition, auto types in C++, type inference in Haskell. Probably most of my Haskell code I do not need to specify types. So the technology and theory exists to make this happen. But also, when has typing ever gotten in the way? Actually having to think about the problem and the correctness of your program? It's somewhat amazing that correctness is so easily discarded. People just get stuck in a local minimum.

dgb23 5y ago
They don't get in the way in that regard. There are solutions they simply cannot express and sometimes the best solution is one of these. Correctness has little to do with it. Most type systems cannot express the actually important stuff, so you need to write defensive code anyway and make sure it works. When you write in a dynamically typed language you are going to miss static typing sometimes and vice versa. The big advantage of static typing is performance and not necessarily correctness.
- foxes 5y ago
  I would be interested in you giving an example of a problem that is not solvable or expressible in a typed language. I am not able to think of such a thing of the top of my head. I disagree that performance is a big advantage. Perhaps there are certain optimisations that can be done if you have added more constraints? But that seems like an added benefit. I feel like there are a plethora of examples of type errors however. Obviously it doesn't rule out logical errors, but at least at the type level its "correct". You can even lift problems to just be type problems. For example only being able to construct inputs as something in the type system. Seems like that rules out a whole class of possible errors with parsing input.
  - dgb23 5y ago
    > I would be interested in you giving an example of a problem that is not solvable or expressible in a typed language. I meant to say that some of many solutions can better, typically simpler, while being just as correct because you don't need to express it in static types. > Obviously it doesn't rule out logical errors, but at least at the type level its "correct". You can even lift problems to just be type problems. For example only being able to construct inputs as something in the type system. That is orthogonal to a type system though. If you take care of the invariants of a data-structure you are almost always going to need more than what most type systems can express. In fact I would argue that type systems provide immediate documentation of very basic properties, which is often an advantage, but from my experience the errors it covers for you are rare, yet can be severe and confusing. Again, having used both I'm not entirely happy with either. I prefer when static, or more generally developer-time-checks are opt-in and expressive, which seems to be a growing trend.
- kaba0 5y ago
  Statically typed languages always have escape hatches, so in that way there really is nothing that can’t be done in such a language vs a dynamic one (at least in theory)
  - dgb23 5y ago
    Agreed! To clear it up: I meant the expressivity of the type system, not the language as a whole.
rocqua 5y ago
Note that there are downsides to type inference. Most notably, with too much type inference you quickly run into undecidability. Specifically, programs for which the question "is this well typed" is not decidable. (Essentially it allows encoding of paradoxes in the type system). This is why Haskell and C++ do sometimes require types to be mentioned.
- foxes 5y ago
  I mean I am not sure that is a downside, just a limitation. Sometimes yes you have to specify if there is an ambiguity. I guess usually on input, but then that is not a huge price to pay.

by foxes 5y ago

dgb23 5y ago

They don't get in the way in that regard. There are solutions they simply cannot express and sometimes the best solution is one of these. Correctness has little to do with it. Most type systems cannot express the actually important stuff, so you need to write defensive code anyway and make sure it works. When you write in a dynamically typed language you are going to miss static typing sometimes and vice versa. The big advantage of static typing is performance and not necessarily correctness.

foxes 5y ago
I would be interested in you giving an example of a problem that is not solvable or expressible in a typed language. I am not able to think of such a thing of the top of my head. I disagree that performance is a big advantage. Perhaps there are certain optimisations that can be done if you have added more constraints? But that seems like an added benefit. I feel like there are a plethora of examples of type errors however. Obviously it doesn't rule out logical errors, but at least at the type level its "correct". You can even lift problems to just be type problems. For example only being able to construct inputs as something in the type system. Seems like that rules out a whole class of possible errors with parsing input.
- dgb23 5y ago
  > I would be interested in you giving an example of a problem that is not solvable or expressible in a typed language. I meant to say that some of many solutions can better, typically simpler, while being just as correct because you don't need to express it in static types. > Obviously it doesn't rule out logical errors, but at least at the type level its "correct". You can even lift problems to just be type problems. For example only being able to construct inputs as something in the type system. That is orthogonal to a type system though. If you take care of the invariants of a data-structure you are almost always going to need more than what most type systems can express. In fact I would argue that type systems provide immediate documentation of very basic properties, which is often an advantage, but from my experience the errors it covers for you are rare, yet can be severe and confusing. Again, having used both I'm not entirely happy with either. I prefer when static, or more generally developer-time-checks are opt-in and expressive, which seems to be a growing trend.
kaba0 5y ago
Statically typed languages always have escape hatches, so in that way there really is nothing that can’t be done in such a language vs a dynamic one (at least in theory)
- dgb23 5y ago
  Agreed! To clear it up: I meant the expressivity of the type system, not the language as a whole.

rocqua 5y ago

Note that there are downsides to type inference. Most notably, with too much type inference you quickly run into undecidability. Specifically, programs for which the question "is this well typed" is not decidable. (Essentially it allows encoding of paradoxes in the type system). This is why Haskell and C++ do sometimes require types to be mentioned.

foxes 5y ago
I mean I am not sure that is a downside, just a limitation. Sometimes yes you have to specify if there is an ambiguity. I guess usually on input, but then that is not a huge price to pay.