There are two reasons you may want to run a program that fails typechecking:
1. The program is in fact correct, but the typechecker can't prove the program is correct and so reports it as a failure (for contrast other typecheckers only report errors if it can prove that there is an error)
2. The type checker is correct in that the program is flawed in some way, but you are the middle of development and it would be more productive if you could observe the behavior of the program before fixing the types. Since your CI pipeline will fail on type errors it's not like you're going to be able to merge your changes before fixing them.
In that case, add a type that constrains the values to the expected user inputs. Now not only are you passing the type checking, you're strongly enforced this invariant at the point where it makes the most sense, you've future-proofed this code against possible future misuse where the expected inputs might change, and you've made the code essentially self-documenting.
I'm not sure many languages support the introduction of types such as:
* An integer that is sum of two primes.
* A string that is created between the hours of 2 pm - 4 pm on a Tuesday.
* A dictionary who's fields comprise a valid tax return.
What do you mean by future proving? If the new version of the code doesn't ship by 2 pm today, the company goes bankrupt and there is no future for the code.
> I'm not sure many languages support the introduction of types such as:
Any language with types can enforce any proposition you can reliably check, which you run as part of the type's constructor. There are multiple ways to do this, for instance in pseudo-ML:
> * An integer that is sum of two primes.
type SumOfPrimes
fn sumOfPrimes : Prime -> Prime -> SumOfPrimes
type Prime
fn primeOfInt : Int -> Maybe Prime
> * A string that is created between the hours of 2 pm - 4 pm on a Tuesday.
type Tuesday2To4String
fn whichString : Clock -> String -> Either String Tuesday2To4String
> * A dictionary who's fields comprise a valid tax return.
> What do you mean by future proving? If the new version of the code doesn't ship by 2 pm today, the company goes bankrupt and there is no future for the code.
Shipping broken code will not save the company from bankruptcy. It's also a myth that dynamically typed languages will get your code out faster.
I'm not sure how you intend to check the creation date of a string in memory since there is no information available to do that or that a tax return is valid given the thousands of rules involved.
Nevertheless let's move on.
It's not a myth, if you are using dynamic typing you will get three times the number of features out the door as someone who uses static typing.
It's just a fact.
1 dynamic typed programmer = 3 static typed programmers in productivity and output.
That is why people use dynamic typing.
From a commerical perspective, static typing does not make sense in most cases. You need something more than a typical business CRUD app to justify it. Usually you only need static typing for performance reasons. Like for a video game or image processing.
In practice, the shipped code doesn't have noticably more bugs. That just something which people who have never used dynamic typing properly like to believe.
If you ever read an article by Eve online where they say Python is their secret weapon or watched what Discord did by implementing everything in Python first. You will understand.
That is the correct end state, but there can be practical considerations for why you might want to run (and possibly even release) the software in this partially correct state, and fix the edge cases later.
I don't disagree, but most statically typed languages don't enforce a level of correctness where this would be an issue. We're not programming with theorem provers with an elaborate specification.
I somewhat agree with your point #2 which is why Haskell provides a deferred type checking mode for prototyping purposes[1]. I think this should be more common among typed languages, but this is not a very typical scenario either.
You presume that the program is able to determine that it is wrong.
One of the most annoying things moving from Ruby / Python into a language with static types that are checked at compile time is dealing with JSON from an external API.
I know, I know. The API could send me back a lone unicode snowman in the body of the response even if the Content-Type is set to JSON. I know that is theoretically possible.
But practically, the endpoint is going to send me back a moustache bracket blob. The "id" element is going to be an integer. The "first name" element is going to be a string.
You encode your assumptions as a structure, then you do your call, ask for the conversion, get notified that that can fail (and you can get an error if you but ask), and then you get your value knowing your assumptions have been confirmed.
It's definitely less "throw at the wall" than just
thing = get(some_url).json()
but it's a lot easier to manipulate, inspect, and debug when it invariably goes to shit because some of your assumptions were wrong (turns out `first_name` can be both missing and null, for different reasons).
For a 5 lines throwaway script the latter is fine, but if it's going to run more than a pair of time or need more than few dozen minutes (to write or run) I've always been happier with the former, the cycle of "edit, make a typo, breaks at runtime, fix that, an other typo, breaks again, run for an hour, blow up because of a typo in the reporting so you get jack shit so you get to run it again".
I haven't had problems with that in strongly-typed languages I've used (most notably, C#). If the response payload isn't JSON, or if it has a missing required field or something is the wrong type, then JsonSerializer.Deserialize(...) will throw an exception. I don't have to add more code just to make the type check pass or anything. (And if I did, _usually_ it's around nullability and the "!" operator would do the trick, or "?? throw new ImpossibleException(...)")
And within the bounds of pragmatism, it's nice that it actually checks this stuff and throws exceptions. In Ruby if the ID field is the wrong type, the exception won't happen at time of JSON.parse(...) but instead much later when you go to use the parsed result. Probably leading to more confusion, and definitely making it harder to find that it was specifically an issue with the JSON and not with your code.
"One of the most annoying things moving from Ruby / Python into a language with static types that are checked at compile time is dealing with JSON from an external API."
That doesn't make much sense - either the API has a well-defined schema, and you define your static types to match (which there are usually tools to do for you automatically, based on an OpenXML/Swagger schema, if there isn't already an SDK provided in your language of choice), or you use a type designed for holding more arbitrary data structures (e.g. a simple string->object Dictionary, or some sort of dedicated JsonObject or JsonArray type).
There are issues around JSON and static typing, e.g. should you treat JSON with extra fields as an error, date/time handling, how to represent missing values etc. (and whether missing is semantically different to null or even undefined), but I would hardly see it as "one of the most annoying things".
Edit: the other issue I forgot is JSON with field names that aren't valid identifiers, e.g. starting with numerals or containing spaces or periods etc. But again, not insurmountable. I'd actually be in favour of more restrictive variation of JSON that was better geared towards mapping onto static types in common languages.
Probably makes sense to make the "string" key "s" for minimal payload size impact, or this could also be done by converting standard JSON to this typed representation at runtime.
You should check what the external API returns anyway. If only because the format of any external API might break in subtler way than just returning a single Unicode snowman, and you'll want to ensure that all such failures are correctly detected as soon as practically feasible.
Likewise in Rust you can todo!() in incomplete functions. But it’s still much harder to run incomplete code than it is in javascript, because you still need to satisfy the type checker and borrow checker even for incomplete programs.
1. The program is in fact correct, but the typechecker can't prove the program is correct and so reports it as a failure (for contrast other typecheckers only report errors if it can prove that there is an error)
2. The type checker is correct in that the program is flawed in some way, but you are the middle of development and it would be more productive if you could observe the behavior of the program before fixing the types. Since your CI pipeline will fail on type errors it's not like you're going to be able to merge your changes before fixing them.