Types 'n' Testing

Todays word of the day is.

There’s your value for long lived apps.

1 Like

I just realized I completely misread the line I quoted which is very embarrassing:

I read that as you write tests to ensure things don’t change in the future :rofl:

I’ve been sitting trying to figure out how to respond thinking, “WTH is going on here…” :rofl:

Anyway, yes, me too.

Yeah, most unit tests exist just to reduce the risk of regressions. As you yourself pointed out, they’re quite unnecessary otherwise.

Yeah, see my latest response—I’m just a dummy who can’t read :upside_down_face:

I cant write to save my live, good thing I chose to be a programmer :sweat_smile:

lol, naw you wrote perfectly clearly, I just misread. I’m also on the last day of a week off where I didn’t write any code but blabbed a lot on here. My brain isn’t in tip-top shape atm.

If you want a more philosophical exploration of this topic, check out this Gary Bernhardt talk from a couple years ago.

https://www.destroyallsoftware.com/talks/ideology

The gist of the talk is that with respect to type systems and tests, static language advocates have an underlying assumption that correctness can be proved exclusively by categories, which is false in the case of most static languages because you can’t define categories as precisely as you would need to given the limits of their type system. Whereas dynamic language advocates have an underlying assumption that correctness can be proved by examples, which obviously is also not true.

To me, the conversation about equivalency of type systems and tests fell out of the mainstream maybe four or five years ago, where I think most people today think about the value of type systems in their ability to create more powerful language servers for your IDE.

Now, of course, after you watch the Gary Bernhard talk, you’ll notice the flaw in even the current dialogue that is equivalent to the garbage collection example he gave at the end of his talk. The implication that a type system is required to make a powerful language server implies that there exists no better language server algorithm that can power these predictions. I think some of the great work Mitch Hanberg on elixirtools/next-ls is proving that.

The way I personally evaluate this topic is what system Is the least tedious to maintain and what most reliably catches breaking changes as I modify my code base. I think this is why the JavaScript community has so widely adopted TypeScript given its sweet spot of type inference and catching function invocations that violate the type specification.

For me personally, I try only to write integration tests that are end-to-end and unit tests of pure functions. Those help me ensure I don’t break any functionality as I change my code, whereas type systems help me do code-level refactors behind the outmost API, where most structure is in-flux, without having to constantly rewrite/fix broken tests

1 Like

I know and love this talk and have watched it several times (along with Gary’s other criminally under-rated talks that aren’t the “WAT”).

I have nothing against statically typed languages and I don’t personally believe that testing replaces types… at least not testing alone, but I really didn’t want to turn this thread into a debate :grimacing: I’ve played around with typed languages but have no professional experience with them and I haven’t even built a fleshed-out toy application with one. My questioned stemmed from the extreme stance that is taken online around static typing. In this particular case, I was talking about how I’ve read the phrase: “Static types replace a whole class of tests!” so many times online but examples of are never given (I never bothered asking because I didn’t want to get involved in a static typing debate on the internet). I was always skeptical and then I watched José’s talk where he said he doesn’t agree with this statement, so I was like, “Yay! Ok, so what are these tests people were writing that they stopped writing once they had types?”

I definitely see how it benefits LSPs. I guess it’s a “weird flex” as the kids say, but I don’t use them (though I love Mitch’s work in general).

I’ve seen lots of tests for typing in all different “untyped” languages (here are some examples in Rails’s ActiveRecord tests), but because it’s generally only useful where the (internal) interface is important you’ll see it almost exclusive in library code, rather than app code.

1 Like

Yes, this is another point that rarely comes up in many debates: the difference between app and library code.

Thanks for the link to the AR tests!

1 Like

Hello, and thanks for asking.

In my Elixir experience, I don’t miss a type system for the solo purpose of checking that the types of expressions are ok.

In fact, I never feared refactoring large amounts of code, and usually I get everything ok at first, or sometimes after fixing one or two type mismatches, which in general are very easy to find and fix.

I do not recommend to write test just to check for types. I think it is a nonsense.

Instead, write tests to be sure that the code does what is supposed to do, and type-checking will come along the way.

Obviously, if your test coverage is not wide enough, then you probably are not testing a part of the code where a type mismatch is hidden … and this is where a static type system will help you avoid these hidden type mismatches. But if someone is not covering well the code with tests, then probably they don’t care for that code’s quality too, so you get as much as you put in.

What I expect of a kind of static type system that is really worth to use is that of a dependent type system. I have no experience with these, but I suspect they may help avoid writing large swathes of tests in exchange of writing proofs about what is expected from the code. For example, I think this kind of type systems can avoid peppering the code with assertions by providing proofs about what we want to assert.

The advantage of proofs is that they ensure a kind of “100% test coverage” of the code you prove. However, some say proofs are frequently (generally?) more difficult to write in comparison to tests.

Property-based testing can help you more than case-based testing, because it automatically tests on a large range of inputs, thus raising coverage, however it cannot provide full guarantees like proofs do.

I think these are all tradeoffs, and I look forward one day to experiment with such a dependent type system, to have a more complete view of this topic.

Hope this helped you.

2 Likes

You are not wrong but strong static typing will force the programmers to think about these. Which is often a good thing.

My view is that testing and strong typing both help with lowering the cost of change, but they do so in different ways, and are therefore not a substitute of each other.

Strong typing pins down the basic interface of each callable function, defining what is expected as input and output. If a change breaks such expectation, the type system tells us. Additionally, when used properly, types also provide documentation, specifying explicitly what a function takes as input and what it returns as output.

Good tests pin down invariant properties of the system behavior, so that if a change breaks such invariants, the test tells us. Ideally, a test would assert an invariant property without restricting the specific implementation, so that one could change the implementation and still pass the tests, if the invariant is respected.

Here’s a toy example to illustrate what I mean. Suppose I want to implement a sort of key-value store, with two functions: set(key, value) that sets a key to a value, and get(key), that gets the value associated to a certain key, if any.

The type system can specify what keys and values are supposed to be, and even what happens if I try to get a key that is not associated to any value.

On the other hand, types won’t help in ensuring that if I set a certain key K to a certain value V, and then get the key K, I get exactly the value V and not another one of the same type. For that, we need a test like “set K to V. Then get K, and assert that the result is V”.

Such test asserts an invariant that the system should respect, without specifying what the implementation should be. Under the hood the system could be implemented as a hash map, as a database call, etc. without failing the test. This is easier said than done in more realistic cases, but that’s the aspiration.

Sometimes, a bug is discovered, and a test can be added to ensure that a similar bug cannot be re-introduced with future changes. That’s protecting against regressions, and again, ideally it would pin down some invariant that should hold for some corner case, rather than a specific implementation.

I don’t think that tests (or types) help much with ensuring correctness. What really matters for me is to lower the cost of change, and both tests and a good type system help, in complementary ways.

3 Likes

If we think a bit deeper, where do the constraints and expectations come from?

Our Elixir programs do not really care what the types are, they only care that there is a matching function for the combination of argument values provided, and that function return values match expectations. Anything else is by definition invalid as without any static types it will generate a runtime exception and crash (as the Erlang gods intended).

I want to point out that our functional code goes beyond static type semantics to value semantics. So we can do better than static types.

If a future “type” system can infer “bottom up” the value constraints from the leaves of the call graph and propogate them up the call graph, then that is all that is needed to identify the possible call paths that permit unconstrained values to flow into those functions where the value constraints are violated.

I prefer to think of this kind of system as a value constraints system and therfore superior to a static type system that needs the developer to constantly remind the compiler “top down” that this thing is a string, this a string, it really is a string over and over and over…

The only thing that matters is that at some point in the code the only available matching function(s) require a string then right there, the value constraint exists AND NOWHERE ELSE.

What we really want are the value constraints to automatically propagate up/out all of the code paths that can arrive at that function so that we can catch conflicts so that we can decide if there is merit in specifically dealing with it earlier in the call graph. Since we have safe let it crash semantics we can code the happy path, avoid polluting our code with types and sad path defensive coding paradigms of other languages and runtimes that do not have the automatic let it crash and cleanup luxury we have in BEAM languages.

In Elixir we do not have to be exhaustive in handling every possibility in our code as that is quite literally exhausting and proven to not be as reliable as BEAM languages and systems. Static types and defensive programming/exhaustiveness are in my view in conflict with coding the happy path and “let it crash”, the more productive path forward is in my view value constraint propagation to aid the developer to identify potential problems they may need to handle.

Value constraints can be more than a simple string type, it may be a constraint that the string be no longer than 12 characters and start with a capital letter. These value constraints can again be propogated up/out all code paths with no need for fixing type annotations throughout the code.

Imagine typing a function call in your favourite IDE and it pops up the value constraints on each function argument without you having to maintain types on everything, all derived through elixir pattern matching which collectively express the value constraints that exist in our programs.

Perhaps some business rules change and the code needs to alter the constraint, I don’t need to tell the compiler all through the code, I only need to implement the constraint at the function definition where the actual constraint is necessary. There is no need to be reminding the compiler on every possible call path, creating a refactoring mess, and we get value constraint expressiveness that goes far beyond the static type checking in most languages.

What I have described above is my hope for an enhanced value checking system in the BEAM (i.e. beneath Elixir) so that it helps the compiler to generate optimal code as well as help the developer identify potential constraint violations in the boundary layers of our programs or libraries.

2 Likes

Neither of both is “superior” to the other, they should and they do complement each other (example: in Rust you have a statically strongly typed struct that you can deconstruct via pattern-matching, and you have 80% of the tools that Elixir has to do so. Same in OCaml).

This way of discourse – pitting stuff against each other – is unproductive. Or your claims about what is “proven” and you should really know better than to not post links showing the alleged “proof”.

The value semantics that Erlang / Elixir have are extremely valuable and nobody in this community is saying that they are not. Some of us however, me included, claim that adding optional strong static typing will make them even more efficient. Nothing else is being claimed. All of us here love the “let it crash” thing. Stuff yells at us in our APM system, we then proceed to add one more defensive clause in the code, problem solved, and we have the best of both worlds.

Elixir’s amazing mix of dynamic typing plus pattern-matching / deconstruction allows you to only opt-in for more static checking when you choose to do so (via guards) and that’s an enormous productivity booster and I understand why people fond of Elixir don’t want a static typing system. Well good news, nobody is currently rewriting the BEAM to be statically strongly typed under your feet! :smiley: Rejoice!

IMO general discussions on the topic are fairly unproductive and tend to devolve into semi-religious wars. It’s always discouraging to see somebody coming in and expressing a strong opinion. Historically, all of these abstractions have their place.

2 Likes

If you mean to say that pattern matching is more expressive than a static type system, by all means I agree. But that does not invalidates the benefits of static typing. Of course, like everything, there are also costs: writing and maintaining static types takes effort. Therefore, whether static typing helps or hinders ultimately depends on the specific type system, project, team skills, etc.

I do think that, while a good type system has clear virtues, the benefits are often exaggerated. Definitely, however powerful, a type system does not replace a good test suite. And definitely there is expressiveness in a programming language way beyond static types.

I should also have added, the type system tells us about broken expectations at compile time. Then, how important it is to discover issues at compile time versus runtime depends heavily on the specific project. On a web applications with a good test suite, where “runtime” often means “when running tests”, monitoring errors is easy, and fixing the occasional bug is just a deployment away, it might not matter too much. On an embedded project, where a runtime issue happens on a user device, possibly hidden from the developer, and fixing a bug involves getting all devices to upgrade, the difference between compile time and runtime can be huge.

2 Likes

I have to respectfully disagree but I think we are both wanting similar outcomes from compile time checking and in fact at the developers fingertips when entering code in their IDE.

My view is that anything that requires developer overhead whilst detecting fewer problems is objectively inferior.

If you can obtain both the the strong type and value constraint because the compiler is able to propagate those constraints, you don’t have to keep telling it all the time because you already did within the code where the constraint was neccesary. There is no need to repeat a poor approximation of the value constraint all over the code base. The compiler is able to provide constraint violation warnings with more more detail than a type.

Inferred value constraints are stronger than static type constraints and don’t require developer effort to obtain the benefit. They reflect the true constraints in our code, not approximations to them, and therefore we are able to detect both type and value errors at compile time.

Agree. However any argument or desire you have in favour of manual approximate static typing is eclipsed by automatic stronger value constraint checking at compile time.

If you can prove your code obeys all the value constraints because the compiler checks it, you can eliminate a whole range of tests and focus on the stuff that matters.

In fact you would have to disable constraint checking on tests to be able to call functions with bad values in order to test the runtime handling of boundary conditions. Imagine having to turn off static type checking in your other languages just to be able to compile tests and that will give you some idea of the relative strength that value constraint checking provides over static types.

1 Like

Your insistence on framing this as a duel between both things is very puzzling. I’ll ask you again: why not both?

Example:

Dynamic typing + pattern matching gives f.ex. 50% value.
Static typing bolted on top gives f.ex. another 20% value.

The 70% sum is still bigger than 50%.

You will have to explain why do you keep framing this as an either-or. I don’t see the need for that.

I don’t get you. How is static typing “repeating a poor approximation of the value constraint all over the code base”, exactly? Can you give examples?

Are you describing something that exists today in Elixir’s ecosystem? If so, can you provide a link to it?

Everything we do is towards the goal of correct and available systems. Static types (which may be useful in some language paradigms), are incidental to the stated goal, as all software has defects, and a robust strategy for dealing with and cleaning up from faults which may caused by software errors/bugs, or other operational conditions including node failures, trumps static typing.

I will turn this around, and ask you to name a language and runtime that has proven to provide concurrency, fault isolation, fault tolerance and live code evolution exceeding that of BEAM languages.

History has proven that BEAM languages do provide the essential foundations for the most dependable systems all without requiring static types or requiring type annotations.

I also think the discussion is missing the nuance between strong typing vs static typing. You don’t need static typing to get strong typing and nor does static typing result in maintainable strongly typed code bases.

If we can accept that strong typing is the goal and static typing is just one (non optimal) approach to it, then I think we can agree that we all share a common goal, we want strongly typed code bases and as many errors detected at compile time as is practical such that it provides a net increase to productivity.

It just happens that I want the strongly typed system to detect value errors also and I don’t want to pay for any of it by reminding the compiler of the expectations. I want don’t repeat yourself - DRY.

An example of what I am referring to with strong typing and type inferencing on the BEAM is the Gleam language. It accomplishes what static typing does without requiring any type annotations, in fact type annotations / are optional and do not impact the compiler type checking, the compiler will however check that the annotation documentation is consistent with the inferred type constraint. There is nothing wrong with using annotations for documentation if you really want the maintenance burden, the key point is the annotations have zero impact on the strong type safety which is 100% inferred with zero developer overhead to get it.

Gleam is the style of strong typing I want for Elixir but actually taking it to the level of value constraints and preferably built into the BEAM VM so it can benefit all BEAM languages.

Think of the way we can match on binaries and then think of those value level constraints being propagated up as inferred types without having to type any annotations anywhere.

Now if I have a set of values that are passed into some chain of functions that do allow reaching a non-matching clause then I want to know what function call chains in my code allow that and either accept it (let it crash) or take action to test or sanitize it so that only values meeting the constraints can flow down that code path.

This is the ideal and any way we can get closer to it will enable use to detect more defects at compile time and ideally as we are coding without any need to decorate our code with annotations (the IDE presents the type and. value constraints to us, and for automated documentation generation the type and value constraints can be similarly produced.)

Gleam comes very close to the idea, it is strongly typed without being statically typed, but it stops at types and doesn’t go as far as value constraints.

Still I would welcome Gleam style strong typing in Elixir even without value constraints checking if we didn’t lose compatibility (e.g. Gleam requires homogeneous lists).