[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).

> 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.

> 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.

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?

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’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.

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

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.

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:

https://docs.kidger.site/jaxtyping/faq/

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'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.

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.

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