Learn

Phase 0 learning path (no formal ML background assumed)

Companion, not part of the formal spec. Use this before or alongside examples-walkthrough.md if the spec feels abstract.

1. What problem Phase 0 is solving (without ML jargon)

Programs that crunch lots of numbers usually organize them in arrays: a grid with one axis (a list), two axes (rows and columns), three axes (for example: batch × position × feature), and so on. Bugs often come from mixing up those axes or assuming two arrays “line up” when they do not.

This project’s Phase 0 is a small, strict language design for describing those arrays (called tensors here) so that a compiler can check, before you run the program, that operations make sense for the shapes you declared. It also attaches optional logical facts about dimensions (for example “this length is at least 1”) and uses an automatic theorem prover (Z3) to check consistency.

You do not need coursework in machine learning. You only need comfort with:

Lists of integers as “sizes along each axis.”
Functions that take arrays and return arrays.
The idea that a compiler can reject a program when types do not match.

2. One picture: three knobs on every tensor type

Every tensor type in Phase 0 has three parts (see phase-0/01-type-system-foundation.md §2):

Part	Plain-language question	What to remember
Dtype	What kind of number (or bool) is in each cell?	Examples: `F32` (32-bit float), `I32` integer.
Shape	How many axes, and how long is each?	Written like `[B, S, D]`: three axes, lengths given by symbols or constants. Order matters: `[2, 3]` is not the same as `[3, 2]`.
Refinements	What extra facts do we know about those lengths?	Example: `B ≥ 1`. Used for safety and reasoning; checked with Z3 when needed.

Subtyping (later, Section 3) mostly says: same dtype, same shape structure, but stronger refinements can be used where weaker ones are required (“if I know B ≥ 100, I can treat it as satisfying B ≥ 1”).

Changing dtype or the actual shape layout is not free subtyping: you need an explicit operation in the IR (cast, broadcast, reshape, transpose).

3. Core IR vs surface syntax

Phase 0 commits to a core IR (S-expression style in the docs): what the type checker actually analyzes.
“Surface” examples in companions look like a nicer language; that is illustrative. Real user-facing syntax is Phase 7 in the roadmap.

Learning tip: When you read examples-walkthrough.md, compare the Surface and Core IR blocks. The IR is the honest artifact; the surface is “how it might feel someday.”

4. Suggested first week (gentle order)

You do not have to read phase-0/ from file 01 to 05 on day one.

Day	Read	Goal
1	`phase-0/README.md` — Key commitments table	Know the “constitution” in one pass.
2	`phase-0/01-type-system-foundation.md` §2 Grammar, §3 Presburger (skim proofs; read “what we get / lose”)	Understand the three knobs and why Z3 is there.
3	`phase-0/03-subtyping-and-coercion.md` §2 Subtyping vs coercion, §3.3 Tensor subtyping	This is the clearest “how to think” section.
4	`phase-0/02-core-operations-and-typing.md` §3 Operation set, then §6 Binary and §7 Matmul	See typing rules attach to the three knobs.
5	`phase-0/01-type-system-foundation.md` §4 Formation, §6 Shape variables	Understand contexts and symbolic dimensions.
6	`examples-walkthrough.md` §2–4	Ask per example: which knobs changed? Where is broadcast explicit?
7	`phase-0/04-operational-semantics.md` §7.0 only (optional)	How “assume reshape volumes match” interacts with runtime.

Then loop: pick one open issue from Section 1 §9 or Section 2 §16 and read the paragraph slowly.

5. Mental exercises (no ML required)

Answer with the three-knob picture:

Same shape [B, S], refinements B ≥ 100 vs B ≥ 1. Can the first be used where the second is expected?
Yes — refinement is stronger; this is subtyping (Section 3).
Same shape, but dtypes F32 vs BF16. Subtype?
No — need an explicit cast (coercion).
You want to add a one-axis array to a two-axis array “so they line up.” Can the core IR do that without a broadcast-style operation?
No — Phase 0 forbids implicit broadcasting; the walkthrough’s linear layer shows explicit broadcast.

These mirror real bugs (wrong layout, wrong dtype, silent broadcasting); Phase 0 makes the fixes visible in the IR.

6. Glossary (minimal)

Term	Here it means
Tensor	A typed multi-dimensional array; type = dtype + shape + refinements.
Axis / dimension	One level of the shape; length can be symbolic (`B`) or constant.
Refinement	A logical constraint on shape symbols, proved/disproved with Z3 when the spec says so.
IR	Intermediate representation: the explicit core language the spec defines.
Subtyping	Using a “more informative” type where a “less informative” one is expected, without changing data (refinements only in Phase 0).
Coercion	An operation (cast, reshape, …) that may change bits or layout.
SMT / Z3	Solver that checks whether constraints can be satisfied; used for refinements and shape equalities.

7. Where to go next

Examples with more detail: examples-walkthrough.md.
Patterns closer to large models (still readable without ML courses): real-world-examples.md — use for comparison tables; skip sections that feel too domain-heavy and come back later.
Formal source of truth: phase-0/ in numerical order when you are ready for full precision.

If the spec ever contradicts this companion, the Phase 0 spec wins.