[dcreager]

> 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

[kuratkull]

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.

[dcreager]

> 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

[Epa095]

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.

It seems like `ty`'s current behaviour is compatible with this, but changing it won't (unless it will just be impossible to type a list of different types).

[rtpg]

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

[_carljm]

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]

We haven't decided yet if this is what we want to do, though. It's also possible that we may decide to compromise on the gradual guarantee in this area. It's not an ironclad rule for us, just something we're considering as a factor.

[ijustlovemath]

Have you all looked at how Pyrefly does it, or are your methods incompatible?

[dcreager]

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.