Benchmark for Type Narrowing (aka Occurrence Typing, aka Type Refinement).
Type narrowing is a feature of static type systems that refines the type of a variable based on the result of type tests. Occurrences of the variable that appear after a type test have a more precise type.
The benchmark is deeply inspired by the motivating examples from the following paper, which provides a formal model for type narrowing as realized in Typed Racket:
@inproceedings{tf-icfp-2010,
title = {Logical Types for Untyped Languages},
booktitle = {{ICFP}},
author = {Tobin--Hochstadt, Sam and Felleisen, Matthias},
pages = {117--128},
publisher = {{ACM}},
doi = {10.1145/1863543.1863561},
year = {2010}
}For some instances, see
- Typed Racket guide on occurrence typing
- TypeScript documentation on narrowing
- Flow documentation on type refinements
- Mypy documentation on type narrowing
- Pyright documentation on type narrowing
See HowToRun.md.
From the examples, we can summarize the common features or "API"s that one would expect from a gradual type checker that supports occurrence typing. Each feature, with a brief description, the guarantee it provides, and the examples that demonstrate it, forms a benchmark item. All the benchmark items are listed below.
If the predicate is true, the type of the variable is refined to a more specific type with the information that the predicate holds.
define f(x: Top) -> Top:
if x is String:
return String.length(x) // type of x is refined to String
else:
return x
define f(x: Top) -> Top:
if x is String:
return x + 1 // type of x is refined to String, adding a number to a string is not allowed
else:
return x
If the predicate is false, the type of the variable is refined to a more specific type with the information that the negation of the predicate holds.
define f(x: String | Number) -> Number:
if x is String:
return String.length(x)
else:
return x + 1 // type of x is refined to Number, namely (String | Number) - String
define f(x: String | Number | Boolean) -> Number:
if x is String:
return String.length(x)
else:
return x + 1 // type of x is refined to Number | Boolean, thus not allowing addition
When the result of a predicate test is bound to an immutable variable, that variable can also be used as a type guard. When the result of a predicate test is bound to a mutable variable, that variable can be used as a type guard only if it is not updated.
define f(x: Top) -> Top:
let y = x is String
if y:
return String.length(x) // type of x is refined to String
else:
return x
define f(x: Top) -> Top:
let y = x is String
if y:
return x + 1 // type of x is refined to String, adding a number to a string is not allowed
else:
return x
define g(x: Top) -> Top:
var y = x is String // y is mutable
y = true
if y:
return String.length(x) // since y is updated, type of x is not refined
else:
return x
When a predicate is a conjunction of multiple predicates, the type of the variable is refined to the intersection of the types refined by each predicate. When a predicate is a disjunction of multiple predicates, the type of the variable is refined to the union of the types refined by each predicate. When a predicate is a negation of another predicate, the type of the variable is refined to the complement of the type refined by the negated predicate.
define f(x: String | Number) -> Number:
if not (x is Number):
return String.length(x)
else:
return 0
define g(x: Top) -> Number:
if x is String or x is Number:
return f(x) // type of x is refined to String | Number, thus allowing the call to f
else:
return 0
define h(x: String | Number | Boolean) -> Number:
if not (x is Boolean) and not (x is Number):
return String.length(x)
else:
return 0
define f(x: String | Number) -> Number:
if not (x is Number):
return x + 1 // type of x is refined to String, adding a number to a string is not allowed
else:
return 0
define g(x: Top) -> Number:
if x is String or x is Number:
return x + 1 // type of x is refined to String | Number, thus not allowing addition
else:
return 0
define h(x: String | Number | Boolean) -> Number:
if not (x is Boolean) and not (x is Number):
return x + 1 // type of x is refined to String | Boolean, thus not allowing addition
else:
return 0
When a conditional statement is nested inside the body of another conditional statement, the type of the variable is refined to the intersection of the types refined by each conditional statement.
define f(x: String | Number | Boolean) -> Number:
if not (x is String):
if not (x is Boolean):
return x + 1 // type of x is refined to Number
else:
return 0
else:
return 0
define f(x: String | Number | Boolean) -> Number:
if x is String | Number:
if x is Number | Boolean:
return String.length(x) // type of x is Number
else:
return 0
else:
return 0
When a conditional statement is nested inside the condition of another conditional statement, the type of the variable is refined to the intersection of the types refined by each conditional statement.
define f(x: Top, y: Top) -> Number:
if (if x is Number: y is String else: false)
return x + String.length(y) // type of x is refined to Number, type of y is refined to String
else
return 0
define f(x: Top, y: Top) -> Number:
if (if x is Number: y is String else: y is String)
return x + String.length(y) // type of x is not clear here, thus not allowing addition
else
return 0
When a custom predicate is true, the type of the variable is refined to a more specific type with the information that the predicate holds. When a custom predicate is false, the type of the variable is refined to a more specific type with the information that the negation of the predicate holds.
define f(x: String | Number) -> x is String:
return x is String
define g(x: String | Number) -> Number:
if f(x):
return String.length(x) // type of x is refined to String
else:
return x // type of x is refined to Number, namely (String | Number) - String
define f(x: String | Number) -> x is String:
return x is String
define g(x: String | Number) -> Number:
if f(x):
return x + 1 // type of x is refined to String, adding a number to a string is not allowed
else:
return x // type of x is refined to Number, namely (String | Number) - String
When a custom predicate is true, the type of the variable is refined to a more specific type with the information that the predicate holds. When a custom predicate is false, the type of the variable is not refined. This is helpful for predicates that are underapproximations.
define f(x: String | Number) -> implies x is Number:
return x is Number and x > 0
define g(x: String | Number) -> Number:
if f(x):
return x + 1 // type of x is refined to Number
else:
return 0
define f(x: String | Number) -> implies x is Number:
return x is Number and x > 0
define g(x: String | Number) -> Number:
if f(x):
return x + 1 // type of x is refined to Number
else:
return String.length(x) // type of x is not refined, thus not compatible with the return type
The type checker checks that the assertion made by a custom predicate is compatible with the type of the variable, instead of just accepting what the programmer asserts.
define f(x: String | Number) -> x is String:
return x is String
define g(x: String | Number) -> Number:
if f(x):
return String.length(x) // type of x is refined to String
else:
return x // type of x is refined to Number, namely (String | Number) - String
define f(x: String | Number) -> x is Boolean: // should not type check
return x is Boolean
define g(x: String | Number) -> Number:
return true // not really checking the type of x, should not type check
Partially refine the type of objects, that is, when the predicate is applied to an object property, refine the type of the object property.
struct Apple:
a: Top
define f(x: Apple) -> Number:
if x.a is Number:
return x.a // type of x.a is refined to Number
else:
return 0
struct Apple:
a: Top
define f(x: Apple) -> Number:
if x.a is String:
return x.a // type of x.a is refined to String, thus not allowing the return
else:
return 0
When appropriate predicates are applied to the elements of a tuple, refine the type of the elements of the tuple. Note that this can be generalized to other data covariant data structures like lists, function results, etc.
define f(x: Tuple(Top, Top)) -> Number:
if x[0] is Number:
return x[0] // type of x[0] is refined to Number, type of x is refined to Tuple(Number, Top)
else:
return 0
define f(x: Tuple(Top, Top)) -> Number:
if x[0] is Number:
return x[0] + x[1] // type of x[0] is refined to Number, but type of x[1] is not clear
else:
return 0
When refining a variable with the type as a union of tuple types, refine the type of the variable by the length of the tuple.
define f(x: Tupleof(Number, Number) | Tupleof(String, String, String)) -> Number:
if Tuple.length(x) is 2:
return x[0] + x[1] // type of x is refined to Tupleof(Number, Number)
else:
return String.length(x[0]) // type of x is refined to Tupleof(String, String, String)
define f(x: Tupleof(Number, Number) | Tupleof(String, String, String)) -> Number:
if Tuple.length(x) is 2:
return x[0] + x[1] // type of x is refined to Tupleof(Number, Number)
else:
return x[0] + x[1] // type of x is refined to Tupleof(String, String, String), thus not allowing addition
When multiple branches where the type of a variable is refined to different types are merged, the type of the variable is refined to the union of the types refined by each branch, instead of joining the types, that is, taking the common supertype.
define f(x: Top) -> String | Number:
if x is String:
String.append(x, "hello") // type of x is refined to String
else if x is Number:
x = x + 1 // type of x is refined to Number
else:
return 0
return x // type of x is refined to String | Number; a bad implementation will refine to Top
define f(x: Top) -> String | Number:
if x is String:
String.append(x, "hello") // type of x is refined to String
else if x is Number:
x = x + 1 // type of x is refined to Number
else:
return 0
return x + 1 // type of x is refined to String | Number
Below is a table for all benchmark items as a quick reference.
| Benchmark | Description |
|---|---|
| positive | refine when condition is true |
| negative | refine when condition is false |
| alias | track test results assigned to variables |
| connectives | handle logic connectives |
| nesting_body | nested conditionals with nesting happening in body |
| nesting_condition | nested conditionals with nesting happening in condition |
| predicate_2way | custom predicates refines both positively and negatively |
| predicate_1way | custom predicates refines only positively |
| predicate_checked | perform strict type checks on custom predicates |
| object_properties | refine types of properties of objects |
| tuple_elements | refine types of tuple elements |
| tuple_length | refine union of tuple types by their length |
| merge_with_union | merge several types with union instead of joining |
The benchmark is performed on the following gradual type checker implements.
- Typed Racket
- TypeScript
- Flow
- mypy
- Pyright
The result is as follows.
| Benchmark | Typed Racket | TypeScript | Flow | mypy | Pyright |
|---|---|---|---|---|---|
| positive | O | O | O | O | O |
| negative | O | O | O | O | O |
| alias | O | O | x | x | O |
| connectives | O | O | O | O | O |
| nesting_body | O | O | O | O | O |
| nesting_condition | O | x | x | x | x |
| predicate_2way | O | O | O | O | O |
| predicate_1way | O | x | O | O | O |
| predicate_checked | O | O | O | O | O |
| object_properties | O | O | O | O | O |
| tuple_elements | O | O | O | O | O |
| tuple_length | x | O | O | O | O |
| merge_with_union | O | O | O | x | O |
O means passed, x means not passed.
see issue #7, also see flow document.
In Typed Racket, Listof(T) has unknown length, while List(T ...) has known length. A length test should narrow Listof to List.
This does not make sense without known length types. Do any migratory languages besides TR have these?
The following is a benchmark item extracted from an example from mypy. Original code:
from typing import TypeGuard # use `typing_extensions` for `python<3.10`
def is_set_of[T](val: set[Any], type: type[T]) -> TypeGuard[set[T]]:
return all(isinstance(x, type) for x in val)
items: set[Any]
if is_set_of(items, str):
reveal_type(items) # set[str]"Official" docs on what type(T) means as an annotation, here argument must be a class. And this pattern works because classes are values and types in Python. It may be impossible in TypeScript because types are erased before runtime.
A custom predicate can take extra arguments that are not refined, but helps in refining the type of the variable.
TODO: use isinstanceof(x, type(b))
define f(x: Listof(Top), t: Type) -> x is Listof(t):
return x.all(lambda y: y is t)
define f(x: Listof(Top), t: Type) -> x is Listof(t):
return x.all(lambda y: y is Number) // should not type check
This would be a convenient feature to have, but it is not clear if any existing gradual type checker supports this.
When a custom predicate is true, the type of the variable is refined to a more specific type with the information that the predicate holds. When a custom predicate is false, the type of the variable is refined to a more specific type with the information that the negation of the predicate holds.
define f(x: String | Number, y: String | Number) -> x is String and y is Number:
return x is String and y is Number
define g(x: String | Number, y: String | Number) -> Number:
if f(x, y):
return String.length(x) + y // type of x is refined to String, type of y is refined to Number
else:
return 0 // a problem would be that, here we know little about x and y
define f(x: String | Number, y: String | Number) -> x is String and y is Number:
return x is Number and y is String
define g(x: String | Number, y: String | Number) -> Number:
if f(x, y):
return String.length(x) + y // type of x is refined to Number, type of y is refined to String
else:
return 0
This seems to be too trivial to be a benchmark item. It just seems essential for a type checker that has explicitly named program constructs.
Refine supertypes to subtypes in a nominal subtyping scheme.
struct A:
a: Number
struct B extends A:
b: Number
define f(x: A) -> Number:
if x is B:
return x.b // type of x is refined to B
else:
return x.a // type of x is refined to A
struct A:
a: Number
struct B extends A:
b: Number
define f(x: A) -> Number:
if x is B:
return x.a
else:
return x.b // type of x is refined to A which does not have a property b
Thanks to Eric Traut for pointing out an issue concerning narrowing and subclass of primitive types in Python.