TypeForm: Spelling for a type annotation object at runtime

Typing
26

@davidfstr, thanks for continuing to push this idea forward.

When the idea for TypeForm was initially suggested, my intuition was that it would be a pretty straightforward feature to spec and implement, but it has proven to be much more problematic than I anticipated. This is my attempt to identify and explain the issues that I see with the current formulation.

Let me start by reviewing some relevant static typing concepts.

Most programming languages that are statically or gradually typed make a clear distinction between “type expressions” and “value expressions”. Type expressions can appear only in certain locations within the grammar, and they serve a distinctly different purpose from value (runtime) expressions. In Python, these concepts were not clearly delineated in PEP 484. This led to ambiguities, confusion, and inconsistencies between type checkers. We’ve recently made significant progress (thanks in large part to @Jelle’s efforts) to define “type expression”, specify where type expressions can be used, what syntactical and semantic limitations are imposed on them, and how they should be interpreted by a static type checker. For details, refer to this section of the typing spec.

Type expressions and value expressions are treated very differently by static type checkers. They serve two very different purposes. Type expressions provide a way to “spell” a type in the type system. When a static type checker evaluates a type expression, its goal is to determine “what type is this spelling”? By contrast, when a static type checker evaluates a value expression, its goal is to determine “what is the type of this expression?”, or put another way, “what type describes the set of values that this expression can potentially produce at runtime?”. In the context of a type expression, it doesn’t really make sense to ask “what is the type of this expression?”.

Distinctly different rules are used for evaluating the two categories of expressions. Consider the following expressions and how differently they are treated by a type checker when evaluated as a type expression and a value expression.

  • When int appears in a type expression, it spells the type that represents the set of all instances of int (or subclasses thereof). As a value expression, int refers to the built-in class object named int, and its type is evaluated as type[int].

  • When ”bool” (with quotes) appears in a type expression, it spells a type that represents instances of the bool class. As a value expression, ”bool” is a str instance, and its type is Literal[“bool”].

  • When list[int] appears in a type expression, it spells a type that represents the set of all instances of list (or subclasses thereof) that have been specialized with a type argument of int. As a value expression, list[int] is an instance of GenericAlias, and its type is type[list[int]].

  • When int | str appears in a type expression, it spells a type that represents the union of the sets described by type expressions int and str. As a value expression, int | str is an instance of UnionType, and its type is UnionType.

The types used in the static type system are an abstraction. These abstract types should not be confused with the classes and objects that are used to implement type expressions and the other machinery of the type system at runtime. The runtime details of GenericAlias, UnionType, and ForwardRef are not part of the type abstraction. They don’t appear anywhere in the typing spec today, nor should they. They are implementation details that are hidden from users and not part of the mental model for static typing. The two concepts should not be confused.

Now, let’s take a deeper look at the proposal for TypeForm.

As I mentioned above, we recently made headway in defining the term “type expression” and specifying unambiguously where type expressions are used in the language. This clarity allows static type checkers to use type-expression evaluation rules in those cases and use value-expression evaluation rules in all other cases.

This draft proposal significantly muddies the waters, which I consider a big step backward. This draft says that any expression used in an assignment statement or as an argument in a call expression may need to be evaluated as either a type expression or a value expression — and perhaps both. And it doesn’t clearly explain the circumstances under which each of these evaluation rules should be used.

It has been suggested that a static type checker could use the inference context (the “expected type”) to determine whether type-expression evaluation rules should potentially be applied. For example, if a type checker encounters x: TypeForm = <expression>, it could first attempt to evaluate <expression> using type-expression evaluation rules (presumably suppressing any errors or warnings it encounters along the way). If that fails, it could then re-evaluate the same expression using value-expression evaluation rules. At first blush, this approach sounds reasonable, but it presents many problems. Here are a few of the issues I’ve identified so far.

  1. If errors are detected in both cases, which error message should be presented to the user? How should it be presented (which text range), and how should the message be worded to guide the user to a fix?
  2. What if the inference context is ambiguous, such as x: TypeForm | str = “list[int]”?
  3. How would this work for ternary expressions like x: TypeForm = int if condition else get_typeform() where int is a legal type expression but get_typeform() is not, even though it may return a value of type TypeForm? I’ll note that ternary expressions are not allowed for type expressions.
  4. What would a type checker do with this: x: TypeForm = list[reveal_type(“int”)]? It’s normally nonsensical to ask a static type checker to evaluate the type of a type expression (or a subexpression within a type expression), but here we’re blurring the lines between type and value expressions, so it’s not clear.

I’ll also note that the notion of an “inference context” (or “bidirectional type inference”) appears nowhere in the typing spec currently. Inference behaviors are generally left as details to each type checker. If this new feature relies on the notion of an “inference context”, we may need to incorporate some aspects of inference behavior into the spec.

I suspect the above list of issues will continue to grow as we further explore the current formulation. These may seem like edge cases that we can just sweep under the rug, but I find that edge cases are where we often get into the most trouble when implementing new type features.

The draft PEP says "A variable of type TypeForm[T] where T is a type, may only be assigned a class object or special form…”. There are a set of syntactic and semantic rules that a static type checker applies when evaluating a type expression. Are all of these same rules applied here? For example, can a variable be used in the expression? Can the expression contain a reference to an out-of-scope TypeVar? There are dozens of specific checks like this that apply to type expressions but not to value expressions. Do all of these checks apply here? Do we need to enumerate them all in the spec? Presumably so, since they would affect the type evaluation behavior.

The current draft indicates that this is allowed:

IntTreeRef: TypeForm = ForwardRef('IntTree')  # OK

This conflates the type abstraction used in type expressions and the internal implementation details used to implement type expressions at runtime, so this doesn’t make sense to me. The assigned expression is neither a valid type expression, nor is it a value expression that evaluates to TypeForm, so I don’t see how this could be allowed.

There has been some discussion about whether special forms that are considered “type qualifiers” should be allowed in a type form expression (e.g. Required[int] or Final[str]. I think the answer is clearly “no”. That can’t possibly work if we want TypeForm to be a generic class that accepts a type argument. First, there’s no way to spell these types since TypeForm[Final[str]] is not a legal type expression. Second, subtyping rules are not defined for type qualifiers, so it’s not clear whether TypeForm[Final[str]] is compatible with TypeForm[str], etc.

The issues that I discuss above lead me to think that we should take a step back and explore alternative solutions (or variants to the proposed solution) that avoid these problems but still address the use cases enumerated in this “motivations” section.

Here’s one idea for consideration. Maybe we should require that a TypeForm constructor be called.

x = TypeForm(int | str)
reveal_type(x)  # TypeForm[int | str]

y = TypeForm("Foo | Bar")
reveal_type(y)  # TypeForm[Foo | Bar]

This TypeForm call could then be added to the list of places where type expressions can appear. This would eliminate all of the ambiguities and would compose well with all existing type features. Admittedly, it makes the feature a bit more cumbersome to use, but maybe that’s a reasonable tradeoff.

I’m open to other ideas, but I have significant misgivings about the proposal as it’s currently framed.

8 Likes