[dnautics]

Elixir/ecto has something called schema changesets that are a very robust way of validating user input. I do test against bad values (not just types, out of range, correct type but unsupported value, etc), but only really at data ingress, and no where else.

Honestly if a sad path causes a typing error in elixir it's not the worst thing. Sentry will catch it, only the user thread crashes, and you go patch it later.

[valenterry]

> I do test against bad values

A type is literally a description of a set of valid values. So when you say you test with bad values, then the answer is: you could use types and would not need these tests anymore.

However, the more interesting question is: is your typesystem capable of expressing your type and, if so, is it worth the effort and implications to do so.

But on a more theoretical level, OP is right: you _can_ save the tests with, given a powerful enough typesystem.

[dnautics]

> you could use types and would not need these tests anymore.

No. These are not internal contracts, these are contracts with user input. In a statically typed language, You are still advised to write tests that your marshalling technique provides the expected error (and downstream effects) that you plan for, if say the user inputs the string "1.", For a string that should be marshalled as an integer.

> A type is literally a description of a set of valid values.

That is generally not the case. There are, for example cases where certain floating points are invalid inputs (either outside of the domain of the function or a singular points), and I don't know of a mainstream PL that lets you define subsets of the reals in their type system.

In go, or c, c++, or rust, you could have a situation where a subset of integers are valid values (perhaps you need "positive, nonzero integers", because you are going to do an integer divide at some point) and that is not an expressible set of value in that type system. Ironically, that is a scenario that IS typable in Elixir and erlang, which are dynamically typed languages.

[valenterry]

I think you are referring to concrete/mainstream languages - so what you are writing is correct from a practical perspective, i.e. I would do that. From a theoretical perspective however it is not necessary, even if such a type-system might not exist yet.

[dnautics]

You can retreat to your corner of theory if you wish, I'll actually build stuff. The real world has scary things like malicious actors that will send payloads designed to break your system through side channels like timing and cosmic rays that can flip bits on your disk and erase the guarantees that you believed you had in your type system.

[qsort]

You are being needlessly antagonistic. On HN of all places we should know that research in type theory isn't purely academic navel gazing.

[valenterry]

Isn't it great that we have both theory and practice and both impact each other? Makes our profession so much more fun! :)

[qsort]

> But on a more theoretical level, OP is right: you _can_ save the tests with, given a powerful enough typesystem.

Yes and no. The trick is building a type system simultaneously strong enough to encode the properties you want, and weak enough that it's statically decidable.

There will always be properties you can't encode in a (useful) type system.

It's a fine line to walk, really. There's an argument to be made that most of the times we don't actually need Turing-completeness, and we'd better off using only types to encode computations, but OTOH I don't really want to think about what coinductive types I must define to solve a problem that could be solved with five lines of javascript instead.

[valenterry]

> There will always be properties you can't encode in a (useful) type system.

If you define useful by "we know that the compiler will finish in finite time" then I agree. And that's indeed a good point! In practice, there will always be runtime tests, at least for how long any of us and our children will live. :)