You are not wrong but strong static typing will force the programmers to think about these. Which is often a good thing.
dimitarvp
lucaong
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
adw632
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
dimitarvp
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! 
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
lucaong
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
adw632
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
dimitarvp
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?
0
adw632
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.
0
adw632
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).
0
dimitarvp
Gleam is statically typed.
It’s hard for me to extract an actual argument from your comments because they seem to be strongly held opinions and are at places non-factual.
0