7 ms·

> you have to pollute your projects with noisy defensive code that double checks the type of everything coupled with extra manually written tests, with no guara

> you have to pollute your projects with noisy defensive code that double checks the type of everything coupled with extra manually written tests, with no guarantee you didn't miss something. A common misconception. In tests, you test that values are correct, the types take care of themselves. Types being correct does not imply values being correct, so you will have to write those tests anyhow, although you maybe be fooled by the safyness of static typing[1] that you don't have to. Values being correct does imply that the types are correct, so if your tests pass, then your types are also obviously correct. (If a==3 then I don't have to check if a is of type pink elephant, it obviously isn't). So that's the in-principle argument. And it turns out that this is completely supported in practice as well: neither the defensive code nor the extra type-based tests that you propose must be the result actually occur in dynamic code-bases with any frequency. That said, static types certainly have their uses, particularly in being machine-checked documentation and also for producing faster code without going through crazy amounts of extra effort. [1] https://blog.metaobject.com/2014/06/the-safyness-of-static-typing.html https://blog.metaobject.com/2014/06/the-safyness-of-static-t...

gpderetta 5y ago
Unless you can exhaustively check your function for its whole domain, you really can't . Your function could indeed return pink elephants when passed unicorns.
- dragonwriter 5y ago
  > Unless you can exhaustively check your function for its whole domain, you really can't. If I generate values within a function that are arguments to a constructor call, and the make the constructor call and return the result with no further manipulation, I can—without exhaustive, or even any—testing be quite confident that the function will return the type for which the constructor so called is the constructor any time it returns, and fail otherwise.
  - seanwilson 5y ago
    > and return the result with no further manipulation, I can—without exhaustive, or even any—testing be quite confident But when you start having loops, conditions, arrays, nullable references etc. you can't be so confident any more unlike with proper type checking where you can be fully confident.
  - gpderetta 5y ago
    right, but it is not the unit test that is giving you that confidence and the unit test will not help you if the function is later modified. What you have, after manual inspection of the code, is some sort of informal and not written down correctness proof. A machine tested proof would be better and types help with that.
seanwilson 5y ago
> A common misconception. > In tests, you test that values are correct, the types take care of themselves. How can you be sure your function e.g. returns an integer for all values and never undefined for some values? Unit tests cannot check this exhaustively unlike type checkers. > Types being correct does not imply values being correct, so you will have to write those tests anyhow, although you maybe be fooled by the safyness of static typing[1] that you don't have to. As I said, types compliment tests, they don't replace them but types do reduce some of the burden on writing tests for you. To nitpick: type checking can prove values are correct when the type system is powerful enough (i.e. dependent types) but this isn't practical enough for mainstream yet.
- kaba0 5y ago
  I agree with you, except for the nitpick. Unfortunately due to formal verification not scaling, dependent types will likely not be the solution :/
  - chriswarbo 5y ago
    Dependent types are already very useful. If we're willing to avoid formal verification, then we don't need a full correctness proof for our application; in which case, there's no need to avoid dependent types just because they don't scale. They still allow us to prove correctness for parts of an application (e.g. a tricky, performance-sensitive algorithm), which is better than nothing. In particular, we can use dependent types to place much tighter constraints on critical pieces of code, but 'cut short' a full correctness proof by simply punting to an error case when it's convenient. For example, say we need to manipulate the Nth element of a collection. We can express indices with a type 'Fin X', whose values are equivalent to 1, 2, ..., X, e.g. f1 : (c: List Foo) -> (n: Fin (length c)) -> BAR Within this 'f1' function, we know that the index 'n' will appear in the list 'c' (as a corollary, we also know that 'c' is non-empty, since empty lists have no indices!); this lets us specify the intended behaviour more precisely, lets us satisfy the requirements of other functions we may want to call, lets the compiler spot more problems for us, perhaps avoids the need for certain bounds checks, etc. Yet this places a burden on anyone who calls this 'f1' function: they need to prove that the index appears within the list (and, in doing so, prove that the list is non-empty). This might be very difficult in the general case, yet a full correctness proof would require it. However, we don't need a full correctness proof; so we can just check if we're in bounds, and return an error if not: f2 : List Foo -> Int -> Either String BAR f2 c i = case mkFin (length c) i of Just i -> Right (f1 c i) Nothing -> Left ("Index " + show i + " not in list of length " + show (length c)) where mkFin : (n: Nat) -> (i: Int) -> Maybe (Fin n) mkFin Z _ = Nothing mkFin _ i | i < 0 = Nothing mkFin (S n) 0 = Just fZ mkFin (S n) i = map fS (mkFin n (i - 1)) Calling a function like 'f2' may end up hitting the error case, so this doesn't prove our entire application is correct; but we can still prove all sorts of things about 'f1', and hence have a lot of confidence in what happens whenever this initial error branch is avoided. Also, anticipating an error up-front is usually preferable to hitting one half-way through processing. Dependent types are really useful for propagating error conditions 'backwards' through the code like this. When practical, I much prefer this to propagating error conditions 'forwards', by returning Maybe, etc. Most applications start with some sort of parsing step, which is a great place to perform such checks, if we can manage to propagate them back that far. Otherwise, we just handle these error cases just like we would any others (dependent types or not).
chriswarbo 5y ago
> Types being correct does not imply values being correct, so you will have to write those tests anyhow, although you maybe be fooled by the safyness of static typing[1] that you don't have to. Urgh, that reference is such a shallow, straw-man facade of static typing. This is especially evident with its link to https://www.sans.org/top25-software-errors/ https://www.sans.org/top25-software-errors/ and claim that those "don't look like type errors to me", a list which includes: - 16 even says 'type' in the title: "Unrestricted Upload of File with Dangerous Type"! Phrased as a type error, this would be "savePicture: Required argument of type 'Either[PNG, JPEG]', given 'Array[Byte]' instead" - 2, 3, 6, 11, 18 are all injection attacks, which are classic type errors (AKA "stringly typed programming"). Phrased as a type error, these would be "+: Cannot append 'Foo' with 'FormInput'", where 'Foo' might be 'SQL', 'ShellCommand', etc. - NULL pointer dereference is Tony Hoare's 'billion dollar mistake', which as type error would be "Expected 'Foo', given 'null'" - integer over/underflow, buffer over/underflow, out-of-bounds access, etc. can all be mitigated with types like 'Maybe', 'Try', etc. at the cost of a bounds/flag check. If we don't want runtime checks, we can instead track memory usage bounds in the types, and have the compiler check that we're allocating enough. So many of these problems are avoidable with types, even before we go into fancy stuff like dependent types, linear types, etc. In particular, most of the burden to getting this right is on languages and libraries, not application developers. For example, if a database library can only be queried by an 'SQL' type, and the only way to construct that type is via literals and a 'withParam[T]: SQL -> T -> SQL' function, then application developers are unable to introduce injection attacks; the library forces them to do the right thing. Instead we get 'dbQuery: String -> ...', 'runShell: String -> ...', 'response.withBody: String -> ...', etc. and draw the conclusion that types can't help :(
- simiones 5y ago
  The problem is that often getting rid of these type-unsafe idioms requires much more sophisticated types OR much more tedious code than expected. For example, a language without NULL references must rely on something like Optional/Maybe. Optional requires generic types (kind-1 types) to be usable, and it also requires some kind of pattern matching or monad comprehensions - otherwise, code using Optional is neither type safe nor readable. The SQL case is much more complex. SQL is such a non-standardized language in practice, and such a complex one, that trying to offer a generic SQL library that presents an AST as the API for even the most popular RDBMSs quickly gets complex. So, you end up with convenient string->SQL converters, and then people stick untrusted input in those strings. Not to mention, your fancy AST library still needs to spit out SQL text to talk to most DBs, so you end up needing to sanitize identifiers in your own SQL->string conversion.

gpderetta 5y ago

Unless you can exhaustively check your function for its whole domain, you really can't . Your function could indeed return pink elephants when passed unicorns.

dragonwriter 5y ago
> Unless you can exhaustively check your function for its whole domain, you really can't. If I generate values within a function that are arguments to a constructor call, and the make the constructor call and return the result with no further manipulation, I can—without exhaustive, or even any—testing be quite confident that the function will return the type for which the constructor so called is the constructor any time it returns, and fail otherwise.
- seanwilson 5y ago
  > and return the result with no further manipulation, I can—without exhaustive, or even any—testing be quite confident But when you start having loops, conditions, arrays, nullable references etc. you can't be so confident any more unlike with proper type checking where you can be fully confident.
- gpderetta 5y ago
  right, but it is not the unit test that is giving you that confidence and the unit test will not help you if the function is later modified. What you have, after manual inspection of the code, is some sort of informal and not written down correctness proof. A machine tested proof would be better and types help with that.

seanwilson 5y ago

> A common misconception. > In tests, you test that values are correct, the types take care of themselves. How can you be sure your function e.g. returns an integer for all values and never undefined for some values? Unit tests cannot check this exhaustively unlike type checkers. > Types being correct does not imply values being correct, so you will have to write those tests anyhow, although you maybe be fooled by the safyness of static typing[1] that you don't have to. As I said, types compliment tests, they don't replace them but types do reduce some of the burden on writing tests for you. To nitpick: type checking can prove values are correct when the type system is powerful enough (i.e. dependent types) but this isn't practical enough for mainstream yet.

kaba0 5y ago
I agree with you, except for the nitpick. Unfortunately due to formal verification not scaling, dependent types will likely not be the solution :/
- chriswarbo 5y ago
  Dependent types are already very useful. If we're willing to avoid formal verification, then we don't need a full correctness proof for our application; in which case, there's no need to avoid dependent types just because they don't scale. They still allow us to prove correctness for parts of an application (e.g. a tricky, performance-sensitive algorithm), which is better than nothing. In particular, we can use dependent types to place much tighter constraints on critical pieces of code, but 'cut short' a full correctness proof by simply punting to an error case when it's convenient. For example, say we need to manipulate the Nth element of a collection. We can express indices with a type 'Fin X', whose values are equivalent to 1, 2, ..., X, e.g. f1 : (c: List Foo) -> (n: Fin (length c)) -> BAR Within this 'f1' function, we know that the index 'n' will appear in the list 'c' (as a corollary, we also know that 'c' is non-empty, since empty lists have no indices!); this lets us specify the intended behaviour more precisely, lets us satisfy the requirements of other functions we may want to call, lets the compiler spot more problems for us, perhaps avoids the need for certain bounds checks, etc. Yet this places a burden on anyone who calls this 'f1' function: they need to prove that the index appears within the list (and, in doing so, prove that the list is non-empty). This might be very difficult in the general case, yet a full correctness proof would require it. However, we don't need a full correctness proof; so we can just check if we're in bounds, and return an error if not: f2 : List Foo -> Int -> Either String BAR f2 c i = case mkFin (length c) i of Just i -> Right (f1 c i) Nothing -> Left ("Index " + show i + " not in list of length " + show (length c)) where mkFin : (n: Nat) -> (i: Int) -> Maybe (Fin n) mkFin Z _ = Nothing mkFin _ i | i < 0 = Nothing mkFin (S n) 0 = Just fZ mkFin (S n) i = map fS (mkFin n (i - 1)) Calling a function like 'f2' may end up hitting the error case, so this doesn't prove our entire application is correct; but we can still prove all sorts of things about 'f1', and hence have a lot of confidence in what happens whenever this initial error branch is avoided. Also, anticipating an error up-front is usually preferable to hitting one half-way through processing. Dependent types are really useful for propagating error conditions 'backwards' through the code like this. When practical, I much prefer this to propagating error conditions 'forwards', by returning Maybe, etc. Most applications start with some sort of parsing step, which is a great place to perform such checks, if we can manage to propagate them back that far. Otherwise, we just handle these error cases just like we would any others (dependent types or not).

chriswarbo 5y ago

> Types being correct does not imply values being correct, so you will have to write those tests anyhow, although you maybe be fooled by the safyness of static typing[1] that you don't have to. Urgh, that reference is such a shallow, straw-man facade of static typing. This is especially evident with its link to https://www.sans.org/top25-software-errors/ https://www.sans.org/top25-software-errors/ and claim that those "don't look like type errors to me", a list which includes: - 16 even says 'type' in the title: "Unrestricted Upload of File with Dangerous Type"! Phrased as a type error, this would be "savePicture: Required argument of type 'Either[PNG, JPEG]', given 'Array[Byte]' instead" - 2, 3, 6, 11, 18 are all injection attacks, which are classic type errors (AKA "stringly typed programming"). Phrased as a type error, these would be "+: Cannot append 'Foo' with 'FormInput'", where 'Foo' might be 'SQL', 'ShellCommand', etc. - NULL pointer dereference is Tony Hoare's 'billion dollar mistake', which as type error would be "Expected 'Foo', given 'null'" - integer over/underflow, buffer over/underflow, out-of-bounds access, etc. can all be mitigated with types like 'Maybe', 'Try', etc. at the cost of a bounds/flag check. If we don't want runtime checks, we can instead track memory usage bounds in the types, and have the compiler check that we're allocating enough. So many of these problems are avoidable with types, even before we go into fancy stuff like dependent types, linear types, etc. In particular, most of the burden to getting this right is on languages and libraries, not application developers. For example, if a database library can only be queried by an 'SQL' type, and the only way to construct that type is via literals and a 'withParam[T]: SQL -> T -> SQL' function, then application developers are unable to introduce injection attacks; the library forces them to do the right thing. Instead we get 'dbQuery: String -> ...', 'runShell: String -> ...', 'response.withBody: String -> ...', etc. and draw the conclusion that types can't help :(

simiones 5y ago
The problem is that often getting rid of these type-unsafe idioms requires much more sophisticated types OR much more tedious code than expected. For example, a language without NULL references must rely on something like Optional/Maybe. Optional requires generic types (kind-1 types) to be usable, and it also requires some kind of pattern matching or monad comprehensions - otherwise, code using Optional is neither type safe nor readable. The SQL case is much more complex. SQL is such a non-standardized language in practice, and such a complex one, that trying to offer a generic SQL library that presents an AST as the API for even the most popular RDBMSs quickly gets complex. So, you end up with convenient string->SQL converters, and then people stick untrusted input in those strings. Not to mention, your fancy AST library still needs to spit out SQL text to talk to most DBs, so you end up needing to sanitize identifiers in your own SQL->string conversion.