Assertions with as

x as T claims that x already has type T. T may give a shape, a domain, a dtype, or several. It is the only way to tell the checker something it can’t prove, and it always compiles to a run-time check (Runtime checks).

Statically, an as must be possible:

• A shape must have the same number of axes, and no axis may have a known size that differs from a known size of x’s (E0410). Symbolic sizes are accepted: rows as [196 D] on a [?k D] is fine. The result has the asserted axes, with their names.
• A domain must not contradict what is known about the values (E0410): a Mask asserted to be numbers or the other way round, a range that doesn’t meet the known range, Additive for values bounded below, Binary for values that can’t be 0 or 1, Index[V] for non-integers or a different V, or Prob for Logit over the same axis. Asserting a range keeps whatever is known that’s narrower: relu(x) as Unit is [0, 1] and sigmoid(x) as Pos keeps the sigmoid’s range where it’s narrower.
• A dtype must be of the same kind (bool, integer or float) as x’s (E0410); to change it, use to. A different dtype of the same kind is accepted.
• as [n] bool asserts a Mask, as x: [n] bool declares one.

The parts of the element type that T doesn’t write are kept: x as [b C] keeps x’s domain, and x as Unit keeps its shape. A domain written without a shape, such as x as Prob over C, finds C among x’s axes. Sizes in T must be in scope or written as ?k (Axis names).

A Python value, whose shape is unknown, gets the asserted type: torch.load("w.pt") as [D 3*D].