Pyrefly vs. Ty: Comparing Python's two new Rust-based type checkers

That concept has been formalized as part of the Python standard library.

https://docs.python.org/3/library/doctest.html

Elixir has this.

https://hexdocs.pm/elixir/main/docs-tests-and-with.html

It really helps in our mdtests, because then we can assert that not-implemented things are currently wrong but for the right reasons!

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

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.

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/

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.

Unfortunately with us being in the middle of the AI hype cycle, everyone and their dog is currently busy migrating to python.

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.

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

> 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

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

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.

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.

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.

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

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.

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.

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?

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.

What's the plan for ruff? Will it be part of ty one day?