5 ms·

> Is it safe to call f(x)? The author asserts that static typing allows the compiler to answer this question, but this only allows the compiler to spot type er

by xapata 10y ago

> Is it safe to call f(x)? The author asserts that static typing allows the compiler to answer this question, but this only allows the compiler to spot type errors in advance. There are many other kinds of errors that are completely invisible to the compiler. In a dynamically typed language, if I don't spot the error from reading the code, I must wait until runtime/testing to discover the error. This is also true for a statically typed language for every kind of error except type errors. Personally, type errors haven't been the kind of errors that haunt my dreams. I guess that's why I'm not enthusiastic about static typing.

NickPollard 10y ago
You are right - in a tautalogical way - that type systems only catch type errors. However, in modern languages (including Haskell, Scala, as well as newer, more experimental languages like Idris), those type errors can be extremely powerful. Many people assume that 'types' are simply primitives like Int and String, and that a type checker just makes sure you don't pass an Int to a function expecting String. However, it is possible to express far more powerful statements about your data using a good type system. For example, you can express the idea of non-emptiness of a container, as mentioned in the article. Then you know that, say, taking the max element of a non-empty container is guaranteed to give you an element, whereas with a possibly-empty container you might not have any element at all, causing a null, or exception, or at least requiring an Optional type. You can express safety properties such as a sanitized string vs. unsanitized. You can have a Sanitized type that can only be created by calling a sanitize function - which carefully escapes/handles any invalid characters - and then functions that might, say, pass a value into an SQL instruction can be typed to only take Sanitized strings. Now the representation in memory of Strings and Sanitized strings is identical, but by using different types and a certain set of allowed functions on those types, you can encode the invariant that a string cannot be inserted into an SQL query until it has been sanitized. Now your type checker can catch SQL insertion vulnerabilities for you. How's that for a type error?
- xapata 10y ago
  You make a good point, so I'll answer in parts. First, when most people talk about static typing, they're talking about the near-useless version -- just types like Int and String. I think we agree there, so I won't mention it further. Second, a dynamically typed language like Python has more typing information than some folks first assume. Python's AttributeError is quite similar to a TypeError. In fact, with old-style classes (v2.1 and earlier), many errors that are now TypeErrors were AttributeErrors. Calling len() on an inappropriate object would raise "AttributeError: no __len__". In many cases where folks talk about wanting a static type system, they really just want interfaces. The Sanitized string example is a good counter-point because the interface needs to be near-identical to a regular string. I'm not certain a more complex memory representation (caused by defining a different class) would cause noticeable inefficiency. We're probably not doing vectorized operations on strings. This brings me to my third point, that Python 3 has a similar split between two types: bytes and str. The memory representation is slightly different, bytes vs unicode, but the interfaces are nearly identical. Two differences would be decode vs encode and that getting an element from bytes (annoyingly) gives an int. The distinction between the two types is enforced mostly inside builtin functions, implemented in C. This was a big deal, causing backwards incompatibility, many flamewars, and we're still resolving it, though I think it's clear to most people now that Python 3 is the future. Is it possible that the Python 2/3 split could have been avoided if we had a static type system? Perhaps, if we had multiple dispatch, the function signatures could have remained the same, avoiding backwards incompatibility... I'm just speculating here. My guess is no, getting rigorous about unicode would cause incompatibility regardless of the type system. I'll get back to the main topic now. > Now your type checker can catch SQL insertion vulnerabilities for you. This sounds useful, but a good interface solves the problem just as well. I'm a Pythonista (if you haven't noticed), so my example is PEP 249 that specifies a DB API for all database wrapper implementers to follow. It states that it's the wrapper dev's responsibility to implement a sanitizing string interpolation for the cursor's execute method. My conclusion is that designing a good interface is important whether you have dynamic or static typing. Static typing errs on the side of safety, dynamic typing errs on the side of flexibility. Both can mimic the other. Arguing that one is better is like saying linear regression is better/worse than k-nearest-neighbors.
  - the_af 10y ago
- rbonvall 10y ago
  Yes, this is the point that's often missing in discussions about types. You can (and you have to work to) encode properties as types to get more value out of them. It's not about avoid mixing ints and strings.
lallysingh 10y ago
> Personally, type errors haven't been the kind of errors that haunt my dreams. The point of strongly-typed systems is that you can represent your constraints as types. This takes extra thinking and work, but gives you almost almost unlimited expressive power (ref: agda). Simple example: meters and feet as different numerical types. When you multiply them, you get a silly unit (foot-meters) that doesn't fit with whatever you wanted (meters^2), and thusly fails compilation.
- xapata 10y ago
  I haven't met anyone other than Haskellians that would create separate types for meters and feet. I also wonder when you would make that distinction in the lifecycle of your application. I suspect not until you first encounter the bug of accidentally mixing units. If so, we'd be solving the problem at the same time, just using different techniques.
  - jdmichal 10y ago
    F# allows sub-typing of numerics with a unit of measure. https://docs.microsoft.com/en-us/dotnet/articles/fsharp/language-reference/units-of-measure https://docs.microsoft.com/en-us/dotnet/articles/fsharp/lang...
    - xapata 10y ago
      That is a nifty syntax.
  - lallysingh 10y ago
    Hi! nice to meet you. I've used this in C++ to great effect. It's also in boost. I put it in anywhere I expect math on units that are easily screwed up. I don't retrofit them in. It's easy enough to have a meters_t typedef from the beginning. It also serves as documentation for the code.
- Koshkin 10y ago
  An even simpler example would be the fact that it makes no sense to add values expressed in different units (without an appropriate type conversion).
staticassertion 10y ago
"Type errors" go way further than "Damn, I passed a string in where I expected an integer". Types are a way of expressing aspects of your code. You can avoid race conditions, you can ensure a program's state is always expected, you can avoid race conditions, you can avoid design errors by encoding the contracts of your design into your types. I think if you're used to a language like Java or C++ you may not see what types can really buy you, but that's because most languages have bad type systems.
- xapata 10y ago
  Static typing is one technique for designing safe, easy to use interfaces. Depending on the language, there may be other tools that are just as effective.
  - staticassertion 10y ago
    Like what? I assume you're referring to testing. Tests are a way to ensure that for some set of inputs you will get some set of desired outputs. And this is assuming you wrote correct tests. Types are far more rigorous - you can ensure, with types, that your code behaves in a certain way given any input. Yes, this extends to "design" bugs ie: not just crashes - you can write a type that ensures that an API can only be used correctly, for example. You can encode logic like "Don't allow unauthenticated users to access this content" into your type system - and you no longer need tests. Of course, type systems don't prevent you from writing tests. They actually make it easier, you can generate test cases based on types, as an example.
    - jdmichal 10y ago
      A type checker is a formal proof system. A test determines correctness for a given input. A formal proof system determines correctness for all inputs.
      - xapata 10y ago
        The are limits to what a formal proof system can do (eg. The halting problem). I also have never met someone who claimed to never need tests because of a powerful type system.
mkonecny 10y ago
The biggest issue with dynamic programming for me is refactoring code. I feel very confident when refactoring a static code-base. With a dynamic code-base it 's much more risky - to the point where I avoid. Of course having great test coverage helps alleviate this, but it's very rare where a large project has 100% test coverage.

by xapata 10y ago

NickPollard 10y ago

You are right - in a tautalogical way - that type systems only catch type errors. However, in modern languages (including Haskell, Scala, as well as newer, more experimental languages like Idris), those type errors can be extremely powerful. Many people assume that 'types' are simply primitives like Int and String, and that a type checker just makes sure you don't pass an Int to a function expecting String. However, it is possible to express far more powerful statements about your data using a good type system. For example, you can express the idea of non-emptiness of a container, as mentioned in the article. Then you know that, say, taking the max element of a non-empty container is guaranteed to give you an element, whereas with a possibly-empty container you might not have any element at all, causing a null, or exception, or at least requiring an Optional type. You can express safety properties such as a sanitized string vs. unsanitized. You can have a Sanitized type that can only be created by calling a sanitize function - which carefully escapes/handles any invalid characters - and then functions that might, say, pass a value into an SQL instruction can be typed to only take Sanitized strings. Now the representation in memory of Strings and Sanitized strings is identical, but by using different types and a certain set of allowed functions on those types, you can encode the invariant that a string cannot be inserted into an SQL query until it has been sanitized. Now your type checker can catch SQL insertion vulnerabilities for you. How's that for a type error?

xapata 10y ago
You make a good point, so I'll answer in parts. First, when most people talk about static typing, they're talking about the near-useless version -- just types like Int and String. I think we agree there, so I won't mention it further. Second, a dynamically typed language like Python has more typing information than some folks first assume. Python's AttributeError is quite similar to a TypeError. In fact, with old-style classes (v2.1 and earlier), many errors that are now TypeErrors were AttributeErrors. Calling len() on an inappropriate object would raise "AttributeError: no __len__". In many cases where folks talk about wanting a static type system, they really just want interfaces. The Sanitized string example is a good counter-point because the interface needs to be near-identical to a regular string. I'm not certain a more complex memory representation (caused by defining a different class) would cause noticeable inefficiency. We're probably not doing vectorized operations on strings. This brings me to my third point, that Python 3 has a similar split between two types: bytes and str. The memory representation is slightly different, bytes vs unicode, but the interfaces are nearly identical. Two differences would be decode vs encode and that getting an element from bytes (annoyingly) gives an int. The distinction between the two types is enforced mostly inside builtin functions, implemented in C. This was a big deal, causing backwards incompatibility, many flamewars, and we're still resolving it, though I think it's clear to most people now that Python 3 is the future. Is it possible that the Python 2/3 split could have been avoided if we had a static type system? Perhaps, if we had multiple dispatch, the function signatures could have remained the same, avoiding backwards incompatibility... I'm just speculating here. My guess is no, getting rigorous about unicode would cause incompatibility regardless of the type system. I'll get back to the main topic now. > Now your type checker can catch SQL insertion vulnerabilities for you. This sounds useful, but a good interface solves the problem just as well. I'm a Pythonista (if you haven't noticed), so my example is PEP 249 that specifies a DB API for all database wrapper implementers to follow. It states that it's the wrapper dev's responsibility to implement a sanitizing string interpolation for the cursor's execute method. My conclusion is that designing a good interface is important whether you have dynamic or static typing. Static typing errs on the side of safety, dynamic typing errs on the side of flexibility. Both can mimic the other. Arguing that one is better is like saying linear regression is better/worse than k-nearest-neighbors.
- the_af 10y ago
rbonvall 10y ago
Yes, this is the point that's often missing in discussions about types. You can (and you have to work to) encode properties as types to get more value out of them. It's not about avoid mixing ints and strings.

lallysingh 10y ago

> Personally, type errors haven't been the kind of errors that haunt my dreams. The point of strongly-typed systems is that you can represent your constraints as types. This takes extra thinking and work, but gives you almost almost unlimited expressive power (ref: agda). Simple example: meters and feet as different numerical types. When you multiply them, you get a silly unit (foot-meters) that doesn't fit with whatever you wanted (meters^2), and thusly fails compilation.

xapata 10y ago
I haven't met anyone other than Haskellians that would create separate types for meters and feet. I also wonder when you would make that distinction in the lifecycle of your application. I suspect not until you first encounter the bug of accidentally mixing units. If so, we'd be solving the problem at the same time, just using different techniques.
- jdmichal 10y ago
  F# allows sub-typing of numerics with a unit of measure. https://docs.microsoft.com/en-us/dotnet/articles/fsharp/language-reference/units-of-measure https://docs.microsoft.com/en-us/dotnet/articles/fsharp/lang...
  - xapata 10y ago
    That is a nifty syntax.
- lallysingh 10y ago
  Hi! nice to meet you. I've used this in C++ to great effect. It's also in boost. I put it in anywhere I expect math on units that are easily screwed up. I don't retrofit them in. It's easy enough to have a meters_t typedef from the beginning. It also serves as documentation for the code.
Koshkin 10y ago
An even simpler example would be the fact that it makes no sense to add values expressed in different units (without an appropriate type conversion).

staticassertion 10y ago

"Type errors" go way further than "Damn, I passed a string in where I expected an integer". Types are a way of expressing aspects of your code. You can avoid race conditions, you can ensure a program's state is always expected, you can avoid race conditions, you can avoid design errors by encoding the contracts of your design into your types. I think if you're used to a language like Java or C++ you may not see what types can really buy you, but that's because most languages have bad type systems.

xapata 10y ago
Static typing is one technique for designing safe, easy to use interfaces. Depending on the language, there may be other tools that are just as effective.
- staticassertion 10y ago
  Like what? I assume you're referring to testing. Tests are a way to ensure that for some set of inputs you will get some set of desired outputs. And this is assuming you wrote correct tests. Types are far more rigorous - you can ensure, with types, that your code behaves in a certain way given any input. Yes, this extends to "design" bugs ie: not just crashes - you can write a type that ensures that an API can only be used correctly, for example. You can encode logic like "Don't allow unauthenticated users to access this content" into your type system - and you no longer need tests. Of course, type systems don't prevent you from writing tests. They actually make it easier, you can generate test cases based on types, as an example.
  - jdmichal 10y ago
    A type checker is a formal proof system. A test determines correctness for a given input. A formal proof system determines correctness for all inputs.
    - xapata 10y ago
      The are limits to what a formal proof system can do (eg. The halting problem). I also have never met someone who claimed to never need tests because of a powerful type system.

mkonecny 10y ago

The biggest issue with dynamic programming for me is refactoring code. I feel very confident when refactoring a static code-base. With a dynamic code-base it 's much more risky - to the point where I avoid. Of course having great test coverage helps alleviate this, but it's very rare where a large project has 100% test coverage.