Unification and the size solver
Size symbols
Each size symbol is one of four kinds:
| Kind | Example | Equal to |
|---|---|---|
| dim | D | Its value |
| rigid | a generic n, inside its function | Only itself |
| unknown | ?k | Only itself |
| solvable | a callee’s n at a call, a new name in a pattern group, ?k in a return type while checking the body | Whatever the equations say |
A function’s generic axes are rigid in its body: nothing is assumed about them, so n doesn’t unify with 196, and two different generics never unify with each other.
Solving
The checker states facts about sizes as equations, lhs = rhs, where lhs may contain solvable variables. Equations come from:
- each axis of each argument at a call, against its parameter’s axis (Generic calls);
- each axis of a returned value, against the return type;
- a pattern group such as
(gh p1), against the axis it binds to (Pattern operations); - the
Index[V]sizes of arguments, after their shapes.
The solver substitutes dims by their values, then repeatedly looks for an equation with exactly one unsolved variable that appears in it linearly (not squared), and solves it: from var * a + b = 0, var = -b / a, which must be exact. It goes round until no equation makes progress. So linear equations and products with one unsolved factor are solved: (gh 16) against 224 gives gh = 14, and (gh p1) with p1 known gives gh.
Solver failures
Each equation fails at most once, with one of four codes:
| Failure | Code | Example |
|---|---|---|
| The two sides can never be equal, or would need a variable to be negative | E0401 | n against 196 in the body of fn f(x: [n]) |
| Solving needs a division that isn’t exact | E0402 | (gh 16) against 225 |
| Variables are left that no equation determines | E0409 | (a b) against 12 with neither known |
| A size overflows | E0414 |
A message says which axis failed and why, as in “axis 1: ?k is not known to equal 196” or “(p1 p2 c) = 16*16*3 = 768, not D = 512”.