[ty developer here]
We are happy with the attention that ty is starting to receive, but it's important to call out that both ty and pyrefly are still incomplete! (OP mentions this, but it's worth emphasizing again here.)
There are definitely examples cropping up that hit features that are not yet implemented. So when you encounter something where you think what we're doing is daft, please recognize that we might have just not gotten around to that yet. Python is a big language!
I am not well versed in python programming, this is just my opinion as an outsider.
For anyone interested in using these tools, I suggest reading the following:
https://www.reddit.com/r/Python/comments/10zdidm/why_type_hi...
That post should probably be taken lightly, but I think that the goal there is to understand that even with the best typing tools, you will have troubles, unless you start by establishing good practices.
For example, Django is large code base, and if you look at it, you will observe that the code is consistent in which features of python are used and how; this project passes the stricter type checking test without troubles. Likewise, Meta certainly has a very large code base (why develop a type checker otherwise?), and they must have figured out that they cannot let their programmers write code however they like; I guess their type checker is the stricter one for that reason.
Python, AFAIK, has many features, a very permissive runtime, and perhaps (not unlike C++) only some limited subset should be used at any time to ensure that the code is manageable. Unfortunately, that subset is probably different depending on who you ask, and what you aim to do.
(Interestingly, the Reddit post somehow reminded me of the hurdles Rust people have getting the Linux kernel guys to accept their practice: C has a much simpler and carefree type system, but Rust being much more strict rubs those C guys the wrong way).
The top comment in that post shuts down the whole nonsense pretty quickly and firmly:
> If you have a super-generic function like that and type hinting enforced, you just use Any and don't care about it.
It's a stupid example, but even within the context of a `slow_add` function in a library: maybe the author originally never even thought people would pass in non-numeric values, so in the next version update instead of a hardcoded `time.sleep(0.1)` they decide to `time.sleep(a / b)`. Oops, now it crashes for users who passed in strings or tuples! If only there were a way to declare that the function is only intended to work with numeric values, instead of forcing yourself to provide backwards compatibility for users who used that function in unexpected ways that happened to work.
IMO: for Python meant to run non-interactively with any sort of uptime guarantees, type checking is a no-brainer. You're actively making a mistake if you choose to not add type checking.
As the author of that post, I'd like to point out the example was meant to be stupid.
The purpose was to show different ideologies and expectations on the same code don't work, such as strict backwards compatibilities, duck typing, and strictly following linting or type hinting rules (due to some arbitrary enforcement). Although re-reading it now I wish I'd spent more than an evening working on it, it's full of issues and not very polished.
> If you have a super-generic function like that and type hinting enforced, you just use Any and don't care about it.
Following the general stupidness of the post: they are now unable to do that because a security consultant said they have to enable and can not break RUFF rule ANN401: https://docs.astral.sh/ruff/rules/any-type/
> Following the general stupidness of the post: they are now unable to do that because a security consultant said they have to enable and can not break RUFF rule ANN401: https://docs.astral.sh/ruff/rules/any-type/
Okay, then your function which is extremely generic and needs to support 25 different use cases needs to have an insane type definition which covers all 25 use cases.
This isn't an indictment of the type system, this is an indictment of bad code. Don't write functions that support hundreds of input data types, most of which are unintended. Type systems help you avoid this, by the way.
> Don't write functions that support hundreds of input data types
But by it's nature, duck typing supports an unbounded number of input types and is what Python was built on.
You've already decided duck typing is wrong and strict type adherence is correct, which is fine, but that doesn't fit the vast history of Python code, or in fact many of the core Python libraries.
> But by it's nature, duck typing supports an unbounded number of input types and is what Python was built on.
You're trying to shove a square peg into a round hole. It's not about right or wrong. Either you want your function to operate on any type, attempt to add the two values (or perform any operation which may or may not be supported, i.e. duck typing), and throw an runtime error if it doesn't work--in which case you can leave it untyped or use `Any`--or you want stronger type safety guarantees so you can validate before runtime that nobody is calling your method with incorrect arguments, in which case you have to represent the types which you accept somehow.
If you want to have a method that's fully duck typed, you're supposed to use `Any`. That's exactly why it exists. Inventing contrived scenarios about how you can't use `Any` is missing the point. It's like complaining C doesn't work if you're not allowed to use pointers.
You're right that historically Python code was written with duck typing in mind, but now even highly flexible libraries like Pandas have type definition support. The ecosystem is way different from even 5-6 years ago, I can't think of any well-known libraries which don't have good typing support by now.
> You're trying to shove a square peg into a round hole
Yeah, that's literally the point of my Reddit post
Duck typing is great, for example to support a range of numeric inputs - say fixed-precison integers, floats, dynamic precision integers, and numpy arrays, pandas series, tensorflow/pytorch tensor. That duck typing can support functions with unbounded types, dos not mean that it is necessary, not generally sensible, for a particular function to support unbounded types.
Duck typing is great and Python’s type system has powerful support for it. You can for instance restrict a function to only objects with a frobnicate() method, without in any way constraining yourself on which implementation you accept. Type checking plus duck typing is very precise and powerful, and it helps me sleep at night.
Stupid is okay. _Nonsense_ is not. Your example was nonsense, it was absurd. The moment I saw the first example I was like, this should be add_ints and should only take ints.
Imagine I say "the human body is dumb! Here's an example: if I stab myself, it bleeds!" Like is that stupid or absurd?
And yet, some Python users insistent on type hinting very dynamic Python code while trying to keep how dynamic it is.
But there was a conceivable way (maybe not in Python) to make a `slow_add` function very generic, yet only be defined over structures where any conceivable `+` operation is defined.
You just have to say the type implements Semigroup.
Yes, this would work if the arguments are lists, or integers, or strings. And it won't pass the typecheck for arguments that are not Semigroups.
It may not work with Python, but only because it's designers weren't initially interested in typechecking.
Challenge accepted.
from dataclasses import dataclass
from typing import Protocol, Self, TypeVar
class Semigroup(Protocol):
def __add__(self, other: Self) -> Self:
...
T = TypeVar("T", bound=Semigroup)
def join_stuff(first: T, *rest: T) -> T:
accum = first
for x in rest:
accum += x
return accum
@dataclass
class C:
x: int
@dataclass
class D:
x: int
def __add__(self, other: Self) -> Self:
return type(self)(self.x + other.x)
@dataclass
class E:
x: int
def __add__(self, other: Self) -> Self:
return type(self)(self.x + other.x)
_: type[Semigroup] = D
_ = E
def doit() -> None:
print(join_stuff(1,2,3))
print(join_stuff((1,), tuple(), (2,)))
print(join_stuff("a", "b", "c"))
print(join_stuff(D(1), D(2)))
print(join_stuff(D(1), 3))
print(D(1) + 3) # caught by mypy
print(D(1) + E(3)) # caught by mypy
print(join_stuff(1,2,"a")) # Not caught by mypy
print(join_stuff(C(1), C(2))) # caught by mypy
doit()
However, it will correctly tell you that it can't accept arguments that don't define addition at all, and that's better than nothing.
Pretty cool that you got this far though!
I think at this point one starts to fight against Python, which wasn't designed with this in mind. But cool nonetheless.
Thanks! My approach is to stop once it starts to hurt, and figure out what I should expect the type checker to miss. The type system and I are both getting better at it as time goes by. It’s not perfect, but it’s way better than not having it.
One thing that post does do though is very clearly highlight the difference between Python's type system and say ... TypeScript's.
TypeScript's goal is to take a language with an unhinged duck type system that allows people to do terrible things and then allow you to codify and lock in all of those behaviours exactly as they're used.
Mypy (and since it was written by GVM and codified in the stdlib by extension Python and all other typecheckers)'s goal is to take a language with an unhinged duck type system that allows people to do terrible things and then pretend that isn't the case and enforce strict academic rules and behaviours that don't particularly care about how real people write code and interact with libraries.
If you include type hints from the very beginning than you are forced to use the very limited subset of behaviours that mypy allow you to codify and everything will be "fine".
If you try to add type hints to a mature project, you will scream with frustration as you discover how many parts of the codebase literally cannot be represented in the extremely limited type system.
At this point I'm fairly convinced that the effort one would spend trying to typecheck a python program is better spent migrating away from python into a language that has a proper type system, then using interop so you can still have the bits/people that need python be in python.
Obviously that isn't always possible but you can spend far too long trying to make python work.
I think you're forgetting how easy type annotation is.
I occasionally spend like 2h working on some old python code. I will spend say 15 minutes of that time adding type annotations (sometimes requires some trivial refactoring). This has an enormous ROI, the cost is so low and the benefit is so immediate.
In these cases migrating code to a proper language and figuring out interop is not on my radar, it would be insane. So having the option to get some best-effort type safety is absolutely fantastic.
I can definitely see your point, it's a useful analysis for projects under heavy development. But if you have a big Python codebase that basically just works and only sees incremental changes, adding type annotations is a great strategy.
If you're supposedly good at software and you spent too long trying to make python work consider the possibility that you're not good at software?
Python has flaws and big ones at that, but there's a reason it's popular. Especially with tools like pydantic and fastapi and uv (and streamlit) you can do insane things in hours what would take weeks and months before. Not to mention how good AI is at generating code in these frameworks. I especially like typing using pydantic, any method is now able to dump and load data from files and dbs and you get extremely terse validated code. Modern IDEs also make quick work of extracting value even from partially typed code. I'd suggest you just open your mind up to imperfect things and give them a shot.
Six month into learning to build a modern python app, with linters, type systems, tests, venvs, package managers, etc… I realized that the supposed difficulty of rust is drastically less than coming to speed and then keeping up with the python “at scale” ecosystem.
My strong suspicion is that such a story depends a great deal upon the personalities of the developers much more than any {tool chaos + type chaos} --- {new syntax + lifespan annotations} spectrum
I don't understand this point at all. I've worked on Django codebases which have a huge set of typing problems... and while it's not 100% I get a lot of value out of type checking.
You annotate enough functions and you get a really good linter out of it!
Unfortunately with us being in the middle of the AI hype cycle, everyone and their dog is currently busy migrating to python.
I don't see why AI hype means more Python code.
State of the art AI models are all closed source and accessible through an API anyways. APIs that any language can easily access.
AAa for AI model development in itself, yes it's mostly Pyython, but niche.
I think you are underestimating the massive amounts of Python code that is built around these things. Also, a lot of businesses are not really interested in using an API for an LLM, instead they will modify and fine-tune their own models and deploy in their own data-centers (virtual or physical), and that means even more Python code.
Sure, a system that only relies on token factory LLM APIs can be written in any language, but that is not the full width and breadth of the AI hype.
> Also, a lot of businesses are not really interested in using an API for an LLM, instead they will modify and fine-tune their own models and deploy in their own data-centers
You realize model training cost millions right? "a lot of businesses" doesn't pass sniff test here.
I'm not even counting the large swaths of data required to train. And the expensive specialists.
And then you'll have to retrain outdated models every so often.
There's a reason that AI has only a handful of players delivering SoTA models and these players are all worth $5B+.
SOTA LLM model training costs a lot, yes. But fine-tuning and training of smaller models is a lot cheaper.
I've trained useful vision-models that delivered business value for industrial applications on a MacBook overnight.
Because everyone and their dog thinks they need to be ready to develop their own models, in python.
This is honestly a thing, at least in the startup world.
I’d be surprised if _anyone_ is migrating server code to Python because of AI.
If you do that you need to compile, which means you can't just distribute a text file with your python program. You need a build infrastructure for every python version, every architecture and every OS.
Have fun with that!
> Python, AFAIK, has many features, a very permissive runtime, and perhaps (not unlike C++) only some limited subset should be used at any time to ensure that the code is manageable. Unfortunately, that subset is probably different depending on who you ask, and what you aim to do.
I'll get started on the subset of Python that I personally do not wish to use in my own codebase: meta classes, descriptors, callable objects using __call__, object.__new__(cls), names trigger the name mangling rules, self.__dict__. In my opinion, all of the above features involve too much magic and hinder code comprehension.
There's a time and a place for each of them:
* Meta classes: You're writing Pydantic or an ORM.
* Descriptors: You're writing Pydantic or an ORM.
* Callable objects: I've used these for things like making validators you initialize with their parameters in one place, then pass them around so other functions can call them. I'd probably just use closures if at all possible now.
* object.__new__: You're writing Pydantic or an ORM.
* Name mangling: I'm fine with using _foo and __bar where appropriate. Those are nice. Don't ever, ever try to de-mangle them or I'll throw a stick at you.
* self.__dict__: You're writing Pydantic or an ORM, although if you use this as shorthand for "doing things that need introspection", that's a useful skill and not deep wizardry.
Basically, you won't need those things 99.99% of the time. If you think you do, you probably don't. If you're absolutely certain you do, you might. It's still good and important to understand what they are, though. Even if you never write them yourself, at some point you're going to want to figure out why some dependency isn't working the way you expected, and you'll need to read and know what it's doing.
I never understood why pydantic reimplemented attrs, but doing it much slower, instead of just using attrs.
> Basically, you won't need those things 99.99% of the time
That's kind of my point. If you don't need a language feature 99.99% of the time perhaps it is better to cut it out from your language altogether. Well unless your language is striving to have the same reputation as C++. In Python's case here's a compromise: such features can only be used in a Python extension in C code, signifying their magic nature.
I don't need my car's airbags 99.99% of the time.
I think it's fine to have those if it makes API design and better. In my mind, there's "code you should write" and there's "code only libraries should write".
A lot of people want pydantics and orms.
You should try Go!
It should be banned by the geneva convention.
Can you share a little bit about what makes you form opinions when you are not even using the language? I think its fascinating how especially discussions about typing makes people shake their fists against a language they don't even use - and like your post make up some contrived example.
>I think that the goal there is to understand that even with the best typing tools, you will have troubles, unless you start by establishing good practices.
Like - what makes you think that python developers doesn't understand stuff about Python, when they are actively using the language as opposed to you?
Indeed, I'm not a regular Python practitioner. I had to use it from time to time because it's the language chosen by the tools I happened to use at that time, like Blender, or Django. In the former case, it wasn't very enjoyable (which says a lot about my skills in that area, or rather lack thereof), while in the latter case I found it quite likeable. So that's my background as far as python goes.
I must admit that I largely prefer static typing, which is why I got interested in that article. It's true that trying to shoehorn this feature in the Python ecosystem is an uphill battle: there's a lot of good engineering skill spent on this.
Perhaps there's a connection to make between this situation and an old theorem about incompleteness?
https://copilot.microsoft.com/shares/2LpT2HFBa3m6jYxUhk9fW
(was generated in quick mode, so you might want to double check).
As someone who has been writing python for years the worst mistake I have ever seen people make is not add type hints and not using a type checker.
To try to tl;dr that rather long post:
> When you add type hints to your library's arguments, you're going to be bitten by Hyrum's Law and you are not prepared to accurately type your full universe of users
That's understandable. But they're making breaking changes, and those are just breaking change pains - it's almost exactly the same if they had instead done this:
def slow_add(a, b):
throw TypeError if !isinstance(a, int)
...
The only real difference here is that it's a developer-breaking change, not a runtime-breaking one, because Python does not enforce type hints at runtime. Existing code will run, but existing tools looking at the code will fail. That offers an easier workaround (just ignore it), but is otherwise just as interruptive to developers because the same code needs to change in the same ways.
---
In contrast! Libraries can very frequently add types to their return values and it's immediately useful to their users. You're restricting your output to only the values that you already output - essentially by definition, only incorrect code will fail when you do this.
> ty, on the other hand, follows a different mantra: the gradual guarantee. The principal idea is that in a well-typed program, removing a type annotation should not cause a type error. In other words: you shouldn’t need to add new types to working code to resolve type errors.
The gradual guarantee that Ty offers is intriguing. I’m considering giving it a try based on that.
With a language like Python with existing dynamic codebases, it seems like the right way to do gradual typing.
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:
def example(x) do
{Integer.to_string(x), Atom.to_string(x)}
end
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.
Profile it and see how much slower it gets :)
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.
Unless you're doing greenfield, gradual typing is really the only way. I've incorporated type hinting in several legacy Python code bases with mypy and really the only sensible way is to "opt-in" one module at a time. If pyrefly doesn’t support that I think its use will be pretty limited. Unless maybe they are going for the llm code gen angle. I could see a very fast and strict type checker being useful for llm generating python scripts.
It reminds me of the early days of Typescript rollout, which similarly focused on a smooth on-boarding path for existing large projects.
More restrictive requirements (ie `noImplicitAny`) could be turned on one at a time before eventually flipping the `strict` switch to opt in to all the checks.
Although I'm paid to write (among other things) Python and not Rust, I would think of myself as a Rust programmer and to me the gradual guarantee also makes most sense.
This is a big turnoff for me. Half the point of adding type annotations to Python is to tame its error-prone dynamic typing. I want to know when I've done something stupid, even if it is technically allowed by Python itself.
Hopefully they'll add some kind of no-implicit-any or "strict" mode for people who care about having working code...
> my_list = [1, 2, 3]
> pyrefly, mypy, and pyright all assume that my_list.append("foo") is a typing error, even though it is technically allowed (Python collections can have multiple types of objects!)
> If this is the intended behavior, ty is the only checker that implicitly allows this without requiring additional explicit typing on my_list.
EDIT: I didn't intend my comment to be this sharp, I am actually rooting for ty to succeed :)
ORIGINAL: I am strongly against ty behaviour here. In production code you almost always have single type lists and it is critical that the typechecker assumes this, especially if the list already has same-type _literal_ items.
The fact that Python allows this has no bearing at all. To me having list[int | str] implicitly allowed by the typechecker seems like optimizing for beginner-level code.
> I am strongly against ty behaviour here.
[ty developer here]
Please note that ty is not complete!
In this particular example, we are tripped up because ty does not do anything clever to infer the type of a list literal. We just infer `list[Unknown]` as a placeholder, regardless of what elements are present. `Unknown` is a gradual type (just like `Any`), and so the `append` call succeeds because every type is assignable to `Unknown`.
We do have plans for inferring a more precise type of the list. It will be more complex than you might anticipate, since it will require "bidirectional" typing to take into account what you're doing with the list in the surrounding context. We have a tracking issue for that here: https://github.com/astral-sh/ty/issues/168
I hope I didn't come off as angry or anything, I was just very surprised by the behaviour :)
I am talking from some experience as I had to convert circa 40k lines of untyped code (dicts passed around etc) to fully typed. IIRC this behaviour would have masked a lot of bugs in my situation. (I relied on mypy at first, but migrated to pyright about 1/4 in).
But otherwise it's good to hear that this is still in progress and I wish the project the best of luck.
> I hope I didn't come off as angry or anything, I was just very surprised by the behaviour
Not at all! :-) Just wanted to clarify for anyone else reading along
So, how does that relate to this quote from the article?
>ty, on the other hand, follows a different mantra: the gradual guarantee. The principal idea is that in a well-typed program, removing a type annotation should not cause a type error. In other words: you shouldn’t need to add new types to working code to resolve type errors.
You could have a `list[int | str]` but then you need to check the type of the elements in the list on usage to see if they are `int` or `str` (if you are actually trying to put the elements into a place that requires an `int` or requires a `str` but wouldn't accept an `int | str`...).
If your code doesn't do that then your program isn't well typed according to Python's typing semantics... I think.
So you can have lists of multiple types, but then you get consequences from that in needing type guards.
Of course you still have stuff like `tuple[int, int, int, str]` to get more of the way there. Maybe one day we'll get `FixedList[int, int, int, str]`....
There are ways to type invariant generics more precisely that still meet the gradual guarantee. E.g.:
x = [] # list[Unknown]
x.append(A()) # list[Unknown | A]
takes_list_of_a_or_b(x) # list[A | B]
Have you all looked at how Pyrefly does it, or are your methods incompatible?
Well ours is not yet implemented, so it's too early to say whether they're compatible. :-)
But less snarkily, we do talk to them often (and the authors of other tools like mypy and pyright) to make sure we aren't introducing gross incompatibilities between the different type checkers. When there are inconsistencies, we want to make sure they are mindful rather than accidental; for good reasons; spec-compliant; and well documented.
I don't think it's optimizing for beginner-level code, I think it's optimizing for legacy code. Introducing a type checker to a large existing untyped codebase is a big lift, but becomes less of one if almost all existing code is accepted.
Well then support an option to enable that kind behaviour? Make it an explicit decision by the devs. I think running in a type error and then adding an exception to your config is safer than silently pass and only learn about the mixed types in a production bug
I think this should be handled by a type assisted linter not typechecker.
Imo a type checker in a dynamic language should is primarily there to avoid runtime errors. In a list with multiple types the typechecker should instead force you to check the type before using an element in that list.
If you want static types python is the wrong language
The tool doesn't have a version number yet, its in preview. Chill.
list[int | str] might usually be a mistake, but what about
my_list = [BarWidget(...), FooWidget(...)] ?
my_list.append(BazWidget(...))
my_list.append(7)
Wouldn't it be nice if the type checker could infer the type hint there, which is almost certainly intended to be list[Widget], and allow the first append and flag the second one?
The problem with the pyrefly behavior is that if you have a large codebase that isn't using any sort of Python typechecking, you can't just adopt this tool incrementally. You have to go fix up all of these issues. So you need to get widespread support for this migration.
For an internal tool at Meta, this is fine. Just make all your engineers adopt the style guide.
For introducing a tool gradually at an organization where this sort of change isn't one of the top priorities of engineering leadership, being more accepting is great. So I prefer the way ty does this, even though in my own personal code I would like my tool to warn me if I mix types like this.
>The fact that Python allows this has no bearing at all. To me having list[int | str] implicitly allowed by the typechecker seems like optimizing for beginner-level code.
Yes, lets base our tooling on your opinion rather what is allowed in python.
I am strongly for ty's behaviour here. working python code should not raise type errors unless the user explicitly opts in to a more static subset of the language by adding type annotations.
> and it is critical that the typechecker assumes this
Why is it critical though? If having a `list[int]` was a requirement I would expect a type error where that's explicit.
Because to me this seems like a fantastic example of a highly possible mistake that a typechecker _should_ catch. Without defined types in this situation a couple of things could happen: 1) it gets printed or passed to some other Any method and the typechecker never yells at you and it crashes in production 2) the typechecker catches the error somewhere long down the line and you have to backtrack to find where you might be appending a str to a list[int].
Instead it could mark it as an error (as all the other checkers do), and if that's what the user really intended they can declare the type as list[str | int] and everything down the line is checked correctly.
So in short, this seems like a great place to start pushing the user towards actually (gradually) typing their code, not just pushing likely bugs under the rug.
It depends on what happens with the list after that. Are there int specific operations applied or it is just printed? What if it is fed into objects with a str attribute where the ints could be cast to str?
I don't know. I would argue that since type checking in python is optional, the type checkers shouldn't care unless the programmer cares. A more interesting case would be my_list.append(2.45) or my_list.append(Decimal("2.0")). Those cases would be "numbers" not just "ints".
In the real world, a row of CSV data is not type checked -- and the world hasn't pushed the spreadsheet industry to adopt typed CSV data.
Astral tooling is great and brings new energy into python land but what is the long game of all astral projects? Integrate them into python natively? Be gone in 5 years and leave unmaintained tooling behind? Rug pull all of us with a subscription?
They'll most likely pursue some sort of business source licensing, where you will not be allowed to deploy apps in production using their tooling without the business paying some kind of subscription. I understand that none of their existing products fit this use case, but it will probably be a similar approach. VCs are not charities.
As a Redditor said:
> The standard VC business model is to invest in stuff that FAANG will buy from them one day. The standard approach is to invest in stuff that's enough of a threat to FAANG that they'll buy it to kill it, but this seems more like they're gambling on an acqui-hire in the future.
I have never seen a FAANG company buy a pure programming-language based tooling startup.
Facebook acquired Monoidics in 2013; they were the startup that created Infer[0].
Why would they do that when they can just fork for free?
They also get a shot at the engineers who wrote the product.
I don’t think any of these questions are specific to Astral and can be applied to pretty much any project. ‘Be gone in 5 years and leave unmaintained tooling’ seems particularly plausible with regard to Facebook’s tooling.
Use any of them at your own risk I suppose.
The announcement talked about selling services built on top of the tools: https://astral.sh/blog/announcing-astral-the-company-behind-...
I think I heard somewhere that they are working on other tools that only big enterprises need like a hosted private package registry.
I really wish they get first class Django support. Sadly, its ORM architecture is impossible to type and impossible to change now. Django is one of the most important use cases for Python, having fast full type checking with Django is a dream, but it does require some special casing from the type checker.
I'm with you. I regularly hit errors with its ORM that make me think: "I thought I cast this class of errors aside years ago". I go over my query code very carefully, since the MK-1 eyeball is important here for spotting typos etc.
(I'm not commenting on it being possible or not to fix; but the current status)
What makes the Django ORM impossible to type check?
It uses a huge amount of what I’m terming “getattr bullshit”: many/most fields of ORM objects are only determined at runtime (they’re technically determinABLE at early runtime during Django initialization, but in practice are often not actually visible via reflection until they are first used due to lazy caching).
What fields are present and what types they have is extremely non uniform: it depends heavily on ORM objects’ internal configuration and the way a given model class relates to other models, including circular dependencies.
(And when I say “fields” here, I’m not only referring to data fields; even simple models include many, many computed method-like fields, complex lazily-evaluatable and parametrizable query objects, fields whose types and behavior change temporally or in response to far-distant settings, and more).
Some of this complexity is inherent to what ORMs are as a class of tool—many ORMs in all sorts of languages provide developer affordances in the form of highly dynamic, metaprogramming-based DSL-ish APIs—but Django really leans in to that pattern more than most.
Add to that a very strong community tendency to lazily (as in diligence, not caching) subclass ORM objects in ways that shadow computed fields—and often sloppily override the logic used to compute what fields are available and how they act—and you have a very thorny problem space for type checkers.
I also want to emphasize that this isn’t some rare Django power-user functionality that is seldom used, nor is it considered deprecated or questionable—these computed fields are the core API of the Django ORM, so not only are they a moving target that changes with Django (and Django extension module) releases, but they’re also such a common kind of code that even minor errors in attempts to type-check them will be extremely visible and frustrating to a wide range of users.
None of that should be taken as an indictment of the Django ORM’s design (for the most part I find it quite good, and most of my major issues with it have little to do with type checking). Just trying to answer the question as directly as possible.
It's possible to write a Django typecheck shim using descriptors. There's some annoying stuff on the edges though, and for example if you are changing up fields in `__init__` then those aren't going to show up in your types.
Ultimately you can get typing for the usual cases, but it won't be complete because you can outright change the shape of your models in Django at runtime (actions that aren't type safe of course)
Isn't that largely on the shoulders of Django maintainers?
I’ve built a few typecheckers (in different languages) that hew closer to Pyrefly’s behaviour than Ty’s behaviour.
If you have a large codebase that you want to be typesafe, Pyrefly’s approach means writing far fewer type annotations overall, even if the initial lift is much steeper.
Ty effectively has noImplicitAny set to false.
As they're described here, Pyrefly's design choices make more sense to me. I like the way Typescript does type inference and it seems like Pyrefly is closer to that. Module-level incrementalism also seems like a good tradeoff. Fine-grained incrementalism on a function level seems like overkill. Performance should be good enough that it's not required.
I hope some typechecker starts doing serious supported notebook integration. And integration for live coding, not just a batch script to statically check your notebook. Finding errors with typing before running a 1-60 minute cell is a huge win.
Do you use Jupyter notebooks in VSCode? It uses the same pylance as regular python files, which actually gets annoying when I want to write throwaway code.
Anyone reading this, if you're like me and prefer the open source version of VSCode where Microsoft disables Pylance, I'd encourage you to try BasedPyright instead.
BasedPyright is much better than pyright! Must use.
I echo the other response here. You absolutely should switch to using notebooks in VSCode with their static typenchecker. Language Servers do exactly what you are wanting, with both notebook integration and «live coding».
I think I prefer Pyrefly's stronger type inference. It can be a pain on Projects with a lot of dynamism, but I'll personally make the tradeoff
Nice, I'm using basedpyright right now, both as a type checker in my IDE as well as in GitHub actions. It's good and mainly does what I want.
I'm not very fond of mypy as it struggles even with simple typing at times.
for decades, big tech contributed relatively little in the way of python ecosystem tooling. There’s Facebooks Pyre, but that’s about it. Nothing for package/dependency management, linting, formatting, so folks like those at Astral have stepped up to fill the gap.
why is type checking the exception? with google and facebook and astral all writing their own mypy replacements, i’m curious why this space is suddenly so busy
Coming from a Meta background (not speaking on behalf of Meta):
"package/dependency management" - Everything is checked into a monorepo, and built with [Buck2](https://buck2.build/). There's tooling to import/update packages, but no need to reinvent pip or other package managers. Btw, Buck2 is pretty awesome and supports a ton of languages beyond python, but hasn't gotten a ton of traction outside of Meta.
"linting, formatting" - [Black](https://github.com/psf/black) and other public ecosystem tooling is great, no need to develop internally.
"why is type checking the exception" - Don't know about Astral, but for Meta / Google, most everyone else doesn't design for the scale of their monorepos. Meta moved from SVN to Git to Mercurial, then forked Mercurial into [Sapling](https://sapling-scm.com/) because simple operations were too slow for the number of files in their repo, and how frequently they receive diffs.
There are obvious safety benefits to type checking, but with how much Python code Meta has, mypy is not an option - it would take far too much time / memory to provide any value.
Instagram built a linter with the ability to fix errors which is an improvement over flake8 & pylint: https://github.com/Instagram/Fixit
But Ruff is an even greater improvement over that
Probably because a large amount of AIs are churning out Python code, and they need type-checkers to sanitize/validate that output quickly. Dynamic languages are hard enough for people to make sense of half the time, and I bet AI agents are struggling even more.
What was not immediately obvious to me (but should have been) is that these are dev-time type checkers -- I think. (I think, both from from the github descriptions which focus heavily on editing, and from the article.) That's really useful because type inference is lacking, to me, in-editor. I tend to ask Copilot: 'add type annotations'.
So in complement to this can I share my favorite _run-time_ type checker? Beartype: this reads your type annotations (ie I see this is where Pyrefly and Ty come in), and enforces the types at runtime. It is blazingly fast, as in, incredibly fast. I use it for all my deployed code.
https://beartype.readthedocs.io/en/latest/
I suspect either of Pyrefly or Ty will be highly complementary with Beartype in terms of editor additions, and then runtime requirements.
The docs also have a great sense of humour.
beartype is great, but I only find it useful at the edges. Runtime checks aren't needed if you have strict typing throughout the project. On a gradually-typed codebase, you can use beartype (e.g. is_bearable) to ensure the data you're ingesting has the proper type. I usually use it when I'm dealing with JSON types.
Why isn’t it necessary? Do you mean that with edit-time type checking, you can catch all errors, so no need for runtime verification the edit-time type decls match?
What about interacting with other libraries?
If you have strict static type checking, type errors can't creep in, so you don't need runtime checking. pyright (type checker) will tell you when a runtime check is redundant. For example, if you already have `var` annotated (or inferred) as `str`, then `if isinstance(var, str)` is statically guaranteed to be true.
Of course, that's only if you trust all the types in your code. You still have escape hatches, such as Any and cast, that can break this guarantee. There are lints (from ruff) and pyright options to help with this. Concerning external libraries, I either use libraries that are 100% typed (which is common these days), or write my own type-safe wrappers around the others.
Any progress in the Python ecosystem on static checking for things like tensors and data frames? As I understand it, the comments at the bottom of this FAQ still apply:
I have a problem with Python's `Optional` type. For example for this following code:
from typing import Optional, Union
def square(
a: Union[int, float],
b: Optional[int] = 2
) -> float:
c = a**b
return c
I think that's a genuine error, since as you say, `None` is a possible value for `b` according to your signature.
To handle this you would need to use "narrowing" to separately handle the case where `b` is `None`, and the case where it is not:
def square(a: Union[int, float], b: Optional[int] = 2) -> float:
if b is None:
return 0
else:
c = a**b
return c
(This is not specific to ty, that narrowing check should work in most Python type checkers.)
I'd like to experiment with writing a reflection based dynamic type annotator for one of these. Just as a toy. Imagine a module which monkey patches every function, class in the parent module it is loaded into, then reflects on the arguments at run time slowly building up a database of expected type signatures. The user would then pick through the deltas approving what made sense.
This is a neat idea, but for large systems it could take a long time to fully exercise every code path with all possible input data. (If this sounds way too excessive, that's because normal people don't do this.)
Unless you mean something like record prod for a few weeks to months, similar to how Netflix uses eBPF (except they run it all the time).
I think my main use case would be to run it on unit tests, and then to provide a human-in-the-loop way to slowly hydrate small to medium sized code bases with types. Maybe progressive refactor tools aren't something anyone actually wants to use or maintain, because I just don't see them around that much.
Are any of these already useful as LSPs for code editors such as Neovim? I run pyright in my Neovim config but I could certainly use something faster.
Not yet tbh. I would realistically expect at least a year or more before you can expect any kind of parity with eg; pyright/basedpyright. Type checkers are hard and have a long tail of functionality that must be implemented.
ty is definitely not ready to be a pyright replacement yet. But it is usable as an LSP for simple things like go to definition, and deeper LSP features are on the roadmap for the eventual beta and GA releases.
https://github.com/astral-sh/ty/blob/main/docs/README.md#oth...
What's the plan for ruff? Will it be part of ty one day?
The current plan is that they will remain separate tools, but will work together nicely if you are using both. For instance, we want to add type-aware and multi-file lints to ruff at some point down the line.
What kind of codebases cause performance problems?
I've been using pyright with neovim for years and have never experienced any kind of noticeable lag.
Ty will have lower barrier of entry, similar to the early days of Typescript.
I'm curious to see which way the community will lean to.
it is sad to see how painful typed python is … i prefer a language where (gradual) types were designed infrom the get go … https://raku.org
As someone who has added type hints to two huge code bases that had nine. It's not that painful. Something much more painful is realizing the code base you are adding type hints to is irreconcilably bugged by design, which would not have been possible had type checking been used.
Really loving those markdown style tests. I think it's a really fantastic idea that allows the tests to easily act as documentation too.
Can you explain how you came up with this solution? Rust docs code-examples inspired?
That concept has been formalized as part of the Python standard library.
https://docs.python.org/3/library/doctest.html
Ah very nice! Did not realize this was a part of the standard library!
It's been there since Python v2.1 https://docs.python.org/release/2.1/lib/module-doctest.html
Here is the first announce of doctest I can find (1999) I think it's Python 1.5 time.
https://groups.google.com/g/comp.lang.python/c/DfzH5Nrt05E/m...
Elixir has this.
https://hexdocs.pm/elixir/main/docs-tests-and-with.html
I use this in my books to show the output but also to "test" that the code found in my books actually works.
I love doctest as it works so well with a REPL but unfortunately it hasn't really gained traction anywhere I've seen.
surfacing revealed types as `@TODO` made me laugh, but thinking about it it's actually a pretty neat touch!
It really helps in our mdtests, because then we can assert that not-implemented things are currently wrong but for the right reasons!
Totally orthogonal question, but since you're deep in that side of Rust dev -
The subject of a "scripting language for Rust" has come up a few times [1]. A language that fits nicely with the syntax of Rust, can compile right alongside rust, can natively import Rust types, but can compile/run/hot reload quickly.
Do you know of anyone in your network working on that?
And modulus the syntax piece, do you think Python could ever fill that gap?
[1] https://news.ycombinator.com/item?id=44050222
I don't know that I'd want the scripting language to be compiled, for reasons that are outside the scope of this reply. So removing that constraint, the coolest thing I've seen in this space recently is kyren's Piccolo:
https://kyju.org/blog/piccolo-a-stackless-lua-interpreter/
> And modulus the syntax piece, do you think Python could ever fill that gap?
I would never ever want a full fledged programming language to build type checking plugins, and doubly so in cases where one expects the tool to run in a read-write context
I am not saying that Skylark is the solution, but it's sandboxed mental model aligns with what I'd want for such a solution
I get the impression the wasm-adjacent libraries could also help this due to the WASI boundary already limiting what mutations it is allowed
There's Gluon, which doesn't share Rust's syntax but does have a Hindley-Milner-based type system and embeds pretty seamlessly in a Rust program.
https://github.com/gluon-lang/gluon
Please no
Most of the time, you want the type to be dynamic in a scripting langage, as you don't want to expose the types to the user. With this in mind, rhai and rune are pretty good. On the python front, there was also the pyoxidizer thing, put it seems dead.
Not necessarily!
These are the strong vs weak, static vs dynamic axes.
You probably want strong, but dynamic typing. eg., a function explicitly accepts only a string and won't accept or convert a float into a string implicitly or magically.
You're free to bind or rebind variables to anything at any time, but using them in the wrong way leads to type errors.
JavaScript has weak dynamic typing.
Python has strong dynamic typing (though since types aren't annotated in function definitions, you don't always see it until a type is used in the wrong way at the leaves of the AST / call tree).
Ruby has strong dynamic typing, but Rails uses method_missing and monkey patching to make it weaker though lots of implicit type coercions.
C and C++ have weak static typing. You frequently deal with unstructured memory and pointers, casting, and implicit coercions.
Java and Rust have strong static typing.
If the language has types at all, they're exposed to the user, even if the time of exposure is a runtime failure. I suspect you want inferred types, which can be had in statically-typed languages.
I am very interested in both of these. Coming from the TypeScript world I'm really interested in the different directions (type inference or not, intersections and type narrowing...). As a Python developer I'm wearily resigned to there being 4+ python type checkers out there, all of which behave differently. How very python...
Following these projects with great interest though. At the end of the day, a good type checker should let us write code faster and more reliably, which I feel isn't yet the case with the current state of the art of type checking for python.
Good luck with the project!