[the_af]

> types [...] make only guarantees about the type of values

What do you think "type of values" means and encodes, and why do you think it's different from your handwritten tests?

I assume you do know that type checking is more than simply validating you're passing a string to a function that expects a string argument?

> Types also only catch certain classes of errors

Which classes of errors? Why do you think manually written unit tests are more complete?

[gleenn]

If I have a complicated set of business-logic functions that all return booleans, the type-checker can tell me I got a boolean back but not that in xyz scenario my result should be true and abc scenario it should be false. You must write a test for that, the types are only the most marginal at helping check correctness. There are many more examples like this. If I have to write the tests, why do I want to spend time writing all the types too if my tests cover the things I care about the the types only cover details like "you returned a number from a function marked boolean", that type of error is super easy to catch with a test, so I didn't need the types.

[the_af]

> the types only cover details like "you returned a number from a function marked boolean", that type of error is super easy to catch with a test, so I didn't need the types

Thanks for your reply, this is why I asked: this kind of typechecking you describe only scratches the basics of what a robust type-checking system can do.

In practice, it can cover much more than "you returned a number from a function marked as boolean", and so it saves you from writing lots of unit tests, leaving you free to write only the few tests that make sense for your business logic.

Once you have a proper type system in place, you can do much more than:

> [...] a complicated set of business-logic functions that all return booleans [...]

You can encode more useful things in the type of the functions than just "it returns a boolean". Of course if every function you write only returns a boolean you won't get much from the type system! But that's circular reasoning...

[gleenn]

It's not circular reasoning, I literally have piles of boolean-typed functions in business logic and there is no quantity of type-checking that will validate that (defn should-go [light-is-green? intersection-is-clear?] (and light-is-green? intersection-is-clear?)) is correct. That requires an actual test. Obviously my example is trivial but they quickly become non-trivial and the type-chrcker will never save me if I replace "and" with "or".

[the_af]

> I literally have piles of boolean-typed functions in business logic

Yes, but this is working with legacy code that wasn't written with a mature type-checking system in mind. The boolean type encodes very little meaning with it, and so there's not much you can reason about it, as you've noticed.

If your argument is "a modern type system cannot help me much with legacy code that didn't leverage it to begin with" I can understand you and even agree somewhat. But that's a different argument.

That's what I mean by circular reasoning: if you don't use the types, then yes, a type system won't be of much use. You'll spend time writing unit tests, which for legacy code seems like an adequate approach.

[dragonwriter]

If your type-checker is “mature" enough to encode the full value level semantics of the code it types (rendering the code itself superfluous, as then you’d just need to compile the type-level code to get your app), you then have the problem of validating the logic of the type-level code, and the natural solution to that problem is, again, testing.

[the_af]

Type checking is modeling + testing.

[gleenn]

I neither used the word legacy nor modern. I don't care how fancy your type checker is today or tomorrow, the arbitrarily deeply complicated boolean-typed function I write tomorrow gleans nearly zero value from type validation. It gains actual validation of correctness with real tests.

[the_af]

It's a legacy problem in the sense your system is a badly designed mess of functions that only return boolean. You could encode additional semantics in the types. Of course if you don't, the type system will be unhelpful.

This is a modeling problem at this point. Types can make your model better by encoding more things. It's often not easy or feasible to refactor the mess, so sometimes you're stuck with it.

[AnimalMuppet]

Depending on your language, some things may not be easy to encode in types. "Verify that the function handles gracefully the situation where the map it's passed doesn't contain that one magic entry." That won't be easy to encode in a type...

[the_af]

Of course not everything can be encoded in types, and also YMMV regarding the specific language you're using.

But you now why I asked the question: people who make claims like "types make only guarantees about the type of values" usually don't understand what modern type-checking can do or what can be encoded in types. People making these claims often believe type-checking is limited to validating that you only pass strings to a function expecting a string argument, or some minor variation of that.

[gleenn]

The fact remains that your type system can be turing-complete and still not validate the actual logic that I need checked/tested.

[the_af]

The same can be said of tests.

Types are just tests. By removing all the mindless, repetitive tests you write, typechecking can free you up to write the actual meaningful tests that you truly need to write.

It's not "pick one", it's "use type checking to help you only write the unit tests that matter".