Comment by rendaw
3 months ago
Gradual typing means that an implicit "any" (unknown type) anywhere in your code base is not an error or even a warning. Even in critical code you thought was fully typed. Where you mistakenly introduce a type bug and due to some syntax or inference limits the type checker unexpectedly loses the plot and tells you confidently "no problems in this file!"
I get where they're coming from, but the endgame was a huge issue when I tried mypy - there was no way to actually guarantee that you were getting any protection from types. A way to assert "no graduality to this file, it's fully typed!" is critical, but gradual typing is not just about migrating but also about the crazy things you can do in dynamic languages and being terrified of false positives scaring away the people who didn't value static typing in the first place. Maybe calling it "soft" typing would be clearer.
I think gradual typing is an anti-pattern at this point.
> Gradual typing means that an implicit "any" (unknown type) anywhere in your code base is not an error or even a warning. Even in critical code you thought was fully typed. Where you mistakenly introduce a type bug and due to some syntax or inference limits the type checker unexpectedly loses the plot and tells you confidently "no problems in this file!"
This is a good point, and one that we are taking into account when developing ty.
The benefit of the gradual guarantee is that it makes the onboarding process less fraught when you want to start (gradually) adding types to an untyped codebase. No one wants a wall of false positive errors when you first start invoking your type checker.
The downside is exactly what you point out. For this, we want to leverage that ty is part of a suite of tools that we're developing. One goal in developing ty is to create the infrastructure that would let ruff support multi-file and type-aware linter rules. That's a bit hand-wavy atm, since we're still working out the details of how the two tools would work together.
So we do want to provide more opinionated feedback about your code — for instance, highlighting when implicit `Any`s show up in an otherwise fully type-annotated function. But we view that as being a linter rule, which will likely be handled by ruff.
This makes sense to me and is exactly what TypeScript does. Implicit `any`s do not raise TypeScript errors (which, by definition, is expected), but obviously that means if there is an `any`, it's potentially unsafe. To deal with this, you can turn on `noImplicitAny` or strict mode (which 99% of projects probably have enabled anyway).
Difference here that strict mode is a tsc option vs. having this kind of rule in the linter (ruff), but the end result is the same.
Anyway, that was a long winded way of saying that ty or ruff definitely needs its own version of a "strict" mode for type checking. :)
Could there ever be a flag to turn off the gradual guarantee and get stricter behavior?
"use strict";
You could give a score to different folders or files to indicate a level of "type certainty" and allow people to define failure thresholds.
> Gradual typing means that an implicit "any" (unknown type) anywhere in your code base is not an error or even a warning.
That depends on the implementation of gradual typing. Elixir implements gradual set-theoretic types where dynamic types are a range of existing types and can be refined for typing violations. Here is a trivial example:
Since the function is untyped, `x` gets an initial value of `dynamic()`, but it still reports a typing violation because it first gets refined as `dynamic(integer())` which is then incompatible with the `atom()` type.
We also introduced the concept of strong arrows, which allows dynamic and static parts of a codebase to interact without introducing runtime checks and remaining sound. More information here: https://elixir-lang.org/blog/2023/09/20/strong-arrows-gradua...
How is this function definition (or maybe just its parameter x) "untyped"? There is enough information to deduce that the type of parameter x is empty and the type of the function doesn't matter because there is an error.
If the body of the function contained only the first or the second call, the verdict would have been that x is respectively an Integer or an Atom and the type of the function is the type of the contained expression.
For us type inference is the same as type checking where all parameters are given the dynamic type. So even if you explicitly added a signature that said dynamic, we would still find a violation, where others would not. The point is that dynamic does not have to mean “anything goes”.
ty also implements gradual set-theoretic types, and can represent "ranged" dynamic types (as intersections or unions with Any/Unknown). We don't currently refine dynamic type based on all uses, as suggested here, though we've considered something very much like this for invariant generics.
In your example, wouldn't `none()` be a type for `x` that satisfies both `Integer.to_string(x)` and `Atom.to_string(x)`? Or do you special-case `none()` and error if it occurs?
Oh, that’s exciting to hear! I would love to exchange notes and I know one of the lead researchers of set theoretic types would love to learn more about your uses too. If that sounds fun to you, you can find me on Gmail (same username).
In our case, we implement a bidirectional system where before applying x to Integer.to_string, we compute the domain of Integer.to_string (which is integer) and pass it up. If x is a dynamic type, then we refine it. So on the first call, x refines to `dynamic & integer`, then we apply it.
The second refinement fails because it becomes none, so we discard it, but it means the application on Atom.to_string will fail anyway. So yes, we check for emptiness and discard none.
As mentioned in other comments - in TypeScript which follows this gradual typing there is a number of flags to disable it (gradually so to speak). No reason ty wouldn't do it.
Responding to your gradual typing anti-pattern bit: Agree that dynamic language behaviors can be extreme but it’s also easy to get into crazy type land. Putting aside a discussion of type systems, teams can always add runtime checks like pydantic to ensure your types match reality.
Sorbet (Ruby typechecker) does this where it introduces a runtime checks on signatures.
Similarly in ts, we have zod.
> teams can always add runtime checks like pydantic to ensure your types match reality.
That's the problem with bugs though, there's always something that could have been done to avoid it =)
Pydantic works great in specific places, like validating user supplied data, but runtime checks as a replacement for static type checkers are not really feasible.
Every caller would need to check that the function is being called correctly (number and position of args, kwarg names, etc) and every callee would need to manually validate that each arg passed matches some expected type.
Pydantic also takes CPU time and doesn't do anything till runtime.
Type checking is real time in the IDE and lets you fix stuff before you waste fifteen minutes actually running it.
To be clear, I myself prefer sound type systems.
But the reality is that teams have started with untyped Python, Ruby, and Javascript, have been productive, and now need to gradually add static types to remain productive.
> Every caller would need to check that the function...
The nice part here is where the gradual part comes in. As you are able to type more of your code, you're able to move where you add your runtime validation, and eventually you'll be able to move all validation to the edges of your system.
pydantic does have @validate_call for this use-case.
1 reply →
In code where you really want to have these guarantees you turn on errors lke "no implicit any" in mypy and tighten the restrictions on the files you care about.
You still have the "garbage in/garbage out" problem on the boundaries but at the very least you can improve confidence. And if you're hardcore... turn that on all over, turn off explicit Any, write wrappers around all of your untyped dependencies etc etc. You can get what you want, just might be a lot of work
Yeah, I’m torn because, in my experience, gradual typing means the team members who want it implement it in their code and the others do not or are very lax in their typing. Some way of swapping between gradual and strict would be nice.
15 seconds after doing "man mypy": --disallow-any-expr
Less than it took you to write all that.