3 ms·

Integration tests are different, but I tend to believe that a strong enough type system should be able to negate the need for unit tests completely. If anyone

Integration tests are different, but I tend to believe that a strong enough type system should be able to negate the need for unit tests completely. If anyone can think of something a unit test could test for that an arbitrarily* complex/strong type system couldn't I'd be interested to hear it. It's possible, I just can't think of any.

pfdietz 3y ago
When I say adequately tested, I mean much more than unit tests. Unit tests aren't going to give you bulletproof code. They don't detect bugs that arise from interactions at a higher level. An arbitrarily complex type system, with dependent types, could detect any bug, since it's formally equivalent to requiring the program be proved correct. But using such a type system is so onerous that I don't know anyone who realistically does it in production. If you wrote such types, you're basically giving a formal specification of what the program is supposed to do. That could then be used, and likely much more easily, for high volume property-based testing.
bluGill 3y ago
Unit tests and types solve somewhat different problems. You can force a unit test to check everything a type system does with effort (mostly by throwing wrong types at your API and verifying you get an error), but I'm not sure how you would use the type system to enforce sort() actually sorts. Sure sort can take a listOfFoo and return a sortedListOfFoo - but that doesn't verify sortedListOfFoo is actually sorted - and in many cases I want an API that is find with listOfFoo but should handle sortedListOfFoo as well.
- skulk 3y ago
  With dependent types you can encode any proposition in first-order logic (?). You can indeed define an array type that is necessarily sorted. It won't be pretty but it's possible. More info here: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
_dain_ 3y ago
I like type systems as much as anyone but I can't see how your type system will check that sin(pi) == 0 if you have a type system expressive enough to do things like that, you've basically got another turing-complete layer on top of your existing language, which is itself ... dynamically typed.

pfdietz 3y ago

When I say adequately tested, I mean much more than unit tests. Unit tests aren't going to give you bulletproof code. They don't detect bugs that arise from interactions at a higher level. An arbitrarily complex type system, with dependent types, could detect any bug, since it's formally equivalent to requiring the program be proved correct. But using such a type system is so onerous that I don't know anyone who realistically does it in production. If you wrote such types, you're basically giving a formal specification of what the program is supposed to do. That could then be used, and likely much more easily, for high volume property-based testing.

bluGill 3y ago

Unit tests and types solve somewhat different problems. You can force a unit test to check everything a type system does with effort (mostly by throwing wrong types at your API and verifying you get an error), but I'm not sure how you would use the type system to enforce sort() actually sorts. Sure sort can take a listOfFoo and return a sortedListOfFoo - but that doesn't verify sortedListOfFoo is actually sorted - and in many cases I want an API that is find with listOfFoo but should handle sortedListOfFoo as well.

skulk 3y ago
With dependent types you can encode any proposition in first-order logic (?). You can indeed define an array type that is necessarily sorted. It won't be pretty but it's possible. More info here: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

_dain_ 3y ago

I like type systems as much as anyone but I can't see how your type system will check that sin(pi) == 0 if you have a type system expressive enough to do things like that, you've basically got another turing-complete layer on top of your existing language, which is itself ... dynamically typed.