# Typing Summit 2024
Anyone is free to take notes here!
## 10:20 am - Typing Council
Structure: 5 members
- Indefinite terms
- Replacements appointed by fiat
Mandate: Make the type system
- Useful
- Usable
- Stable
Roles:
- PEP review
- Specification
- Conformance tests
- User-facing guide
Typing specification
- Building and improving the spec
- Conformance tests
- Documentation at https://typing.readthedocs.io
- Help wanted!
Q&A
**Are there are things we cannot in typing that can be nice but would make usability more complicated?**
The challange is the division between academia and industry. Wanting to type every obscure corner case that might occur when calling functions that return functions etc. presents a challange and may not be worth trying to type it right.
One of the things we can do is provide more scrutiny to new features to be sure they are usable.
Another source of tension is that there are various typecheckers. We have to consider backwards compatibility and usability by making the type system usable.
**For codebases are 99% typed. Depending on the level of coverage in your projet, how do you balance expressiveness and coverage?**
We have to balance between expressiveness and usability. So This is a consideration for typing features. For features that are seen by end users, we would be okay with more complexity.
Getting to 100% coverage is not a goal. We want to be able to catch errors. It is not always valuable to have 100% coverage. Since Python has runtime checks, soundness may not actually be a goal. Getting errors because the type system is not expressive enough can be frustrating.
**Different typecheckers can be confusing for users in terms of pros and cons. Do you think it's desirable to simplify the spec?**
Conformance tests help with this. Different typecheckers are good at different things and can use different approaches. We focused on standardizing annotations but not the type behavior.
**How to simplify error messages for complicated functionalities?**
This is a tooling issue. We need good tooling which simplifiers error messages that get displayed to the user.
Some code has been written without types in mind, such as overloads, which can do many things based on various parameters. This helps for easy prototyping. Those things are complicated to type.
Being understood by static typecheckers limits the design space for building new things such as dataclasses.
**Conformance tests are the emphasis of the typing counsil currently. what is the next step?**
We captured a lot of features. The plan is to improve the spec. Also the user facing reference. Anyone can contribute to this.
**What do you think about defining a backwards compatibility policy?**
We have not thought about it explicitly. We do not have an obvious backwards compatability guarantee in Python. We don't think Python is ready for an absolute guarantee.
**What's the relationship between typing counsil and python steering counsil and is there frictions between each of their goals?**
The echo system at large is not ready for types to drive feature development. If a new language feature is proposed and it works well with type annotations. If the feature solves a real problem but there is no good typing solution, then the typing world will have to solve that problem.
**We want typing to be simple for the general user and not too complex. I agree with that but don't feel like it should detract away from having complex types. If those types are not there to help them to make sure their code has no errors, then they're going to not want to use that language. **
We want simple things to have simple typing. We are adding new type system features but every feature has a cost in terms of tooling.
## 11:05 am - Alex Waygood: Rust and Python
- Missing from Rust: Union (but it's unsafe and not widely used); use Enum instead
- Set theory of types: types are sets of values
- But this falls short of the mark
- We can consider the cardinality (how many values of a type)
- Some types are sets of infinite cardinality (e.g., str)
- But some aren't (e.g., bool)
- We can also consider the number of possible subtypes
- Many Python types (e.g. non-final classes) can have
infinite subtypes
- In Rust (outside the trait system) there are *no* subtypes
- Advantages of the Rust model
- Less user code is valid, so mistakes are easier to catch
- Example: if you emulate Rust Enums with a class
hierarchy, you can't seal it today.
- This means a new subclass could extend it and cause an error
- How to apply to Python?
- Sealed proto-PEP
- @final decorator
- But you have to add it everywhere
- Verbose and error-prone
- We can only get sum types by avoiding inheritance
- Sealed PEP suggests limiting inheritance to only classes in the current module
- So type checker can treat sealed class as closed union of subclasses
- But this PEP has received resistance from type checker authors worried about implementation
- Where do we go from here?
- Do we want a new typing construct or just cleaner syntax?
-
## 11:45 am - Carl Meyer: Theory of Type Hints, Revisited
- Lots of improvements over the past year
- Want to unblock intersection PEP
- The spec uses "consistent with" but does not define it
- PEP 483 defines some terms like "consistent with"
- But it was not added to the spec
- The spec should provide a "theory of types"
- Kevin Millikin provided a draft spec https://bit.ly/python-subtyping. Very similar in content to PEP 483. Both are useful resources.
- Thesis I: The spec should define its foundational concepts and ground them in a theory of types
- Should be informal, as a formal model is beyond our capacities
- Benefit of an informal theory is to provide an intuition about the meaning of types. This lets us make the system more consistent.
- PEP 483 should also be brought into the spec
- What theory of types?
- Semantic subtyping: types are sets of possible values
- Alternative: syntactic subtyping but skipping
- Thesis II: Typing spec should be based on semantic subtyping
- Gradual semantic types?
- Combining gradual and semantic types is relatively recent. Python was at the bleeding edge.
- What is Any?
- "Abstracting Gradual Typing": Any is the set of all static types
- "Gradual Typing: A New Perspective": Any is an existentially-qualified type variable
- Is there a type we could substitute Any with to make it valid?
- Personally I find thinking of Any as a standin for a type variable most intuitive
- They agree:
- Any is not a static type or a set of values
- It represents an unknown static type
- It is not a subtype or supertype of anything
- There is a "consistency" or "materialization" relation between Any and other static types
- Examples related to Any
- Any as sets of types; attributes on unions and intersections
- Python has intersections!
- Type checkers synthesize intersections on isinstance() calls
- But type checkers do not treat Any & ConcreteType the way you'd expect based on theory
- Violates the Gradual Guarantee
- Violates the definition of Any we came up with
- Type checkers are saying Any & C == C
- But that violates our definitions!
- This implies also Any & C == Any
- But only pyre does that
- Type checkers should change here: they should treat Any & C as irreducible
- Could be a practical argument for current behavior, but Carl argues this is exactly what Any is for
- What is the motivation?
- Intersection types: blocked on this code example
- Thesis III: Spec should follow gradual semantic types literature and both Any | T and Any & T should be irreducible
- Description of Any as both at the top and bottom is not enough for understanding how Any works
- Ethan Smith: What is the practical impact of changing behavior?
- Martin DeMello: What is user intuition? Treat isinstance() as a cast?
- Sam Goldman: support for Carl's approach to incorporating theory
## 12:15 pm - David Foster: Type Form
A TypeForm is a type expression
- This is different from a `type[T]` because `type[T]`
has to refer to a class
- It is also different from a type annotation expression because
annotations can include context-dependent "qualifier" information
that is not itself a type, e.g. `Required[T]` or `Final[T]`
- But all type expressions are valid runtime `object` instances,
and runtime type checkers rely on this.
One use case, `isassignable` which behaves like `isinstance` but
can understand more types such as `TypedDict`. But to make this
work for refinement, we need it to behave as if it reutrns
`TypeIs[T]`. But we need a way to relate a `T` appearing in
the argument type expression to the return value.
```
def isassignable(value: object, ty: TypeForm[T]) -> TypeIs[T]: ...
```
Other use cases also exist for a way to understand that a
type expression "tags" a type that is valid for some value.
Many open questions
- name (`TypeExpr`?)
- behavior for `Annotated`
- behavior for stringified type expressions (allow?)
- is pattern matching for subexpressions worthwhile (no?)
- how implementable is this?
Q&A
- Q: how would you actually write a `TypeForm` use case like
`isassignable`?
- A: You handle a subset that you understand, and you need
to produce good errors on other cases
- Q: what would we want from type checkers here?
- A: we want the ability to use type variables and support
narrowing for `TypeIs` and `TypeGuard`
- A: we probably aren't asking for checking of the body
of such a function
- Q: what is the appetite for moving away from type strings?
- A: PEP 649 in 3.14 will hopefully make them much rarer
- A: they are likely not going away, and much existing code
will use them for years to come
## Sign up for lightning talks
1. Steven - Typing Meetups?
2. Adrian - Annotated type checking
- Pydantic supports annotated-types to narrow types
- But there's no static support
- Want some way to check that metadata matches type
4. Maggie - type use in practice
5. We have a lot of discussion about type features
6. But not much about how to use types in practice
7. Will have an open space about this
6. Alex Grönholm - abstract types
7. Raising awareness about an issue: mypy only allows concrete types for type\[\]
## 12:45 pm - Lightning talks
Sign in with Wallet
Connect another wallet