The earlier a mistake is caught, the less it costs to fix. In X_eTaL it can be caught as you type it; when the compiler expands the macros, first inside a code string and then by a macro reading its own text; when the types are checked; when a lint reads the program; when a test finds that its output has changed; while it runs; or never, as an answer that is quietly wrong. X_eTaL is designed to push every mistake as early on that list as it can. This post goes down that ladder one rung at a time, with a real example of each, and then tells what happened when a new library slipped to the bottom rung.

Resource Link
The language X_eTaL · its lints
The libraries X_eTaL-libraries
The thread #11: equations · #12: pipelines
Comments Discord

The ladder

When What catches it Example below
as you type the editor a brace left open
when the macros expand the compiler, inside a code string a misspelled name or a wrong type in X_eTaL handed to a macro
when the macros expand a macro checking its own text an equation or a pipeline written wrong
before the program runs the type checker a whole number divided by a decimal
when asked the linter a lambda that only passes its argument on
when the tests run a regression test a fixed bug coming back
while the program runs a check written into the code an index outside its array, a broken shape promise
never nothing three equations that summed the wrong thing

The higher a mistake is caught, the cheaper it is: an error before the program runs costs a moment, an error while it runs may throw away work already done, and a wrong answer costs whatever was built on it.

As you type

The X_eTaL live demo: the drawn form of a line pasted into the ASCII pane, and below it error[non-ascii] at main.xtl:1:11 with the column marked
The live demo, as you type: the drawn form pasted in as source is refused at its first character that is not ASCII, line 1, column 11. Click to enlarge.

The earliest check is in the editor. xetal edit shows a file as typed on the left and drawn on the right, and below them the types of its definitions or, when there is one, the first error, marked in both panes, updated on every keystroke. A brace left open is found before the line is finished, with the message xetal run would print:

error[unclosed]: this `{` is never closed
 --> syn.xtl:1:12
  |
1 | u:m_ean := { v -> ('+ r_/ v) / f_loat t_ally v
  |            ^

The live demo’s editor does the same in the browser. It also refuses text that is not source at all: the drawn form, pasted in, is an error at its first character that is not ASCII, because the drawing is only ever output. The grammar helps here too: it never guesses between two readings, so text it cannot read one way is an error where it was typed, not a different program. A language server, so that any editor could do the same, is on X_eTaL’s wish list.

Looking inside a string, before any macro runs

A macro’s arguments are strings, and to every tool a string is opaque: whatever X_eTaL is written inside one, the type checker and the linter see only quoted text. A mistake in it surfaces only when the macro has run and its expansion is checked. That is still before the program runs, but it needs a run of the macros, and the linter alone never sees it.

A code string, c"...", changes that. Its value is the same string, but the c tells every tool its inside is X_eTaL, and a macro says in its contract which of its sides take code. The system macro i̲f< takes code on both. So the inside is now read with the rest of the file, and where a macro takes code it is also checked on its own, before any macro runs: as the body of a function over the names it uses, with the program’s functions in scope. A misspelled function is found where it was written:

c"n = 0" i̲f< c"ᵘn̲ope 1◆ 2"

error[undefined-name]: this name is never defined
 --> p.xtl:2:17
  |
2 | c"n = 0" i_f< c"u:n_ope 1; 2"
  |                 ^^^^^^^

So is a value of the wrong type, with its hint:

error[type-mismatch]: expected a number, found Char
 --> p.xtl:2:17
  |
2 | c"n = 0" i_f< c"1 + \"a\"; 2"
  |                 ^^^^^^^^
  |                     ---- a string: a vector of Char
  = note: `+` has type Num a => a -> a -> a
  = help: a string is text, not a number: write a number without quotes

The linter does the same check without running anything, as a lint of its own, code-check, which is an error by default, and it runs the ordinary lints on the inside too: a lambda that only passes its argument on, written inside a code string, is reported at its column inside the string, the same redundant-lambda as in code outside one. Writing the same call with plain strings still works, and running it still finds the misspelled name; but the linter alone finds only a suggestion, the string-kind lint:

warning[string-kind]: i_f< takes code on its right: write it as a code string, c"...", so it is drawn and checked as X_eTaL

The check inside a string is partial by design. It knows what holds for any value the macro might give the names it binds, an unknown name, a wrong number of arguments, a type that cannot fit, but not what the macro will actually pass; that is still checked on the expansion. And it applies only where a macro takes code. A pipeline’s string mixes X_eTaL with the pipeline’s own notation, and an equation’s string is a notation altogether; those are only read with the file, and their macros check them as they expand.

Macros check their own text

A macro that reads a notation checks it when the program is compiled, and refuses a call it cannot read, at the call:

"Y[o,h,w] | O Ho Wo" ᵉe̲q< "sum c:=0..C - 1, sum h:=0..1 | X[c,h,w]"
error[bad-equation]: an index is bound once: o, h, w, c, h

@ ᶠˡᵒʷp̲ipe< c"x ▷ 3"
error[bad-pipeline]: a stage is a function (nn:r_elu, [f_ g_], '{ x -> ... }) or an expression naming the previous value it (or a name bound before it): 3

The equation library has twenty-eight tests of such refusals, the pipeline library (Flow, in X_eTaL-ML) sixteen. They do the type checker’s job for the notations it cannot see inside, because to the language a notation is just a string, and they do it earlier, while the macros expand.

Types

After the macros have expanded, X_eTaL infers the type of every name before the program runs, and refuses a program whose types do not fit. Ask it what it inferred:

$ xetal type mean.xtl
u:m_ean : Float -> Float

Here is a program with a mistake in its last line: a 2 by 2 array of whole numbers divided by a decimal.

a ← 2 2 r̲eshape 1 2 3 4
s ← 2.0
p̲rint! 100
a ÷ s

$ xetal run type.xtl
error[type-mismatch]: expected Int, found Float
 --> type.xtl:4:1
  |
4 | a / s
  | ^^^^^
  | - `a` is an Int
  |     - `s` is a Float
  |
1 | a := 2 2 r_eshape 1 2 3 4
  |      -------------------- `a` gets its type here
  |
2 | s := 2.0
  |      --- `s` gets its type here
  = note: `/` has type Num a => a -> a -> Float
  = help: Int and Float do not mix: `f_loat n` makes a Float of an Int, `f_loor x` or `c_eiling x` an Int of a Float

The 100 on the line before is never printed: the program is refused before it starts. That is the latest rung a mistake should land on. And the message does the rest of the work: where, which name is which type, where each got its type, and how to convert. That message is new this week. Until a few days ago the same mistake was reported as expected Int, found Float at 47..52, a range of bytes, with no line, no source and no hint; writing this post found it, and it was rewritten. Writing a ÷ 2.0 works, because a number written in the program takes whichever type it is needed as; a name already bound as a whole number does not change type, so (f̲loat a) ÷ s is how to say it.

Lints

xetal lint reads a program for things that are legal but probably not meant. It has thirty-one lints in six groups, from correctness and suspicious to pedantic, each with a default level, and each one explains itself with xetal lint --explain. Two of them:

ᵘn̲egAll ← { v → '{ x → n̲eg x } m̲ap v }
warning[redundant-lambda]: this lambda only passes its arguments to `n_eg`: write `'n_eg` at lint.xtl:1:22

ᵘc̲lip ← { v → (t̲ally v) ? v◆ 0 r̲eshape 0 }
warning[int-condition]: this guard's condition is an Int, which fails at run time unless it is 1 or 0: write the comparison meant, as `0 < n` or `0 != n` at ic.xtl:1:20

The second is a lint about a later rung: a guard on a count works while the count is 0 or 1, and stops the program the first time it is 2. Where a fix is certain, xetal lint --fix makes it, and it refuses to touch a file git could not restore:

$ xetal lint --fix fixme.xtl
fixed 1 finding(s) in fixme.xtl
ᵘn̲egAll ← { v → 'n̲eg m̲ap v }

The libraries are kept lint clean, and findings can also be written as JSON, one per line, so an editor can show where they are.

Tests

Some mistakes are not in new code but in a change to code that worked. The libraries’ tests are regression baselines: each test is a program with its expected output pinned beside it, and a test whose output changes fails. The equation library’s refusals are tested this way. This one pins the bug told below, so that it cannot come back:

⍝ Text after a reference is refused, never dropped (y[i]2 once gave the plain sum).
"e:" u̲se< "Equations"
y ← f̲loat 1 2 3 4
"L[] | " ᵉe̲q< "sum i:=0..3 | y[i]2"

error[bad-equation]: an array reference ends with its closing bracket; nothing follows it: y[i]2
 --> reject-trailing.xtl:5:17
  |
5 | "L[] | " e:e_q< "sum i:=0..3 | y[i]2"
  |                 ^^^^^^^^^^^^^^^^^^^^^

A test catches a mistake only after it is made and only where someone thought to look, which is why it sits below the checks that need no test written.

Checked while running

Some mistakes only the data can show. Then the check is written into the code, and it stops the program with everything needed to find the cause, never a silent wrong read. The equation macro checks every subscript it reads:

error[index]: X axis 1: index 2 is outside 0..1 (from c)
error[rank]: X[c,h+r] indexes 2 axes, but X has rank 3

And a pipeline stage that promises a shape is checked against it:

@ ᶠˡᵒʷp̲ipe< c"x ▷ 2 × it ▹y [n] ▷ y + 1"
error[shape]: stage 2 (y): shape 4, expected 3

These are better than wrong answers and worse than errors before running. X_eTaL’s shape lint can move such a mistake up a rung: it proves a mismatch before the program runs where a shape is written as a check, r̲equireShape. The equation and pipeline macros check their shapes in code of their own, which the lint does not read, so for now theirs are caught while the program runs.

A silent wrong answer

Writing the equations post meant trying equations the library had not been tested on. With y of 1 2 3 4 and p of 1.5 2 2 4, three gave wrong answers with no error anywhere:

Summand Gave Should have
(y[i] - p[i])^2 0.5, the sum of y − p given 1.25
y[i]2 10 been refused
y[i] % 2 10, the % 2 gone been refused

Worse, the LaTeX the same call returned showed the square, so the printed math and the computed value disagreed, which is the one thing the library promised could not happen.

The cause was in the macro’s reader, the code that takes its string apart. A term starting with a parenthesis was read by dropping its first and last characters, without checking that the last one was the closing parenthesis, so (y[i] - p[i])^2 lost its 2. A reference like y[i] was read from the first [ to the last ], without checking that the ] ended the term, so whatever followed it vanished. Nothing checked that every character had been used.

It was fixed the same morning, in three layers. Every rule of the reader now uses all of its text or refuses the call. Only the notation’s own characters may appear, so % is refused by name. And every call is now read three ways from one grammar, as the value, as the LaTeX and as a plain reprint, and the reprint is compared with what was written: a rule that dropped a character, any rule, now makes the call fail when the program is compiled. A differential test now also generates random equations and checks each against the same computation written by hand.

What changes so it cannot happen again

The fix covered one library. The class of bug, a reader that uses part of its text and drops the rest, can happen in any macro that reads a notation, and more of them are coming. Three changes go further, from narrow to broad:

  • The pipeline macro was written to the rule from the start, with a test for each kind of text it refuses, the equation library’s three cases among them, and a macro, ᶠˡᵒʷt̲ext<, that writes back what it read.
  • A parsing library for macro writers, whose every piece uses all of its text or refuses, with the reprint check built in, so a new macro does not have to learn this lesson again. It has been written, and it is the subject of a planned post.
  • A check in the language itself, now built. A macro declares a contract in its documentation, how it is called and whether it copies its text into its expansion or parses it. For a macro that copies, the default, the macro runner checks that every name and number of the call’s text reaches the expansion, and refuses the call otherwise. A toy macro that forgets the power:
@ q:s̲quare< "3 ^ 2"
error[unused-argument]: q:s_quare< did not use 2 of the text on its right; a macro that copies its text writes every name and number of it (## uses: copied)

A macro that parses a notation, such as the equation and pipeline macros, says ## uses: parsed, and for those the reprint check is the guard. Either way, the mistake that started this is now caught while the macros expand, near the top of the ladder.

What is still rough

The ladder is right; the rungs are being made comfortable one message at a time, as the type error above shows. One rough place was fixed while this post was being written: a code string given to an equation, which takes notation rather than code, used to fail in the lexer with a message about a number. Now it is the string-kind error, at the string, with the fix: drop the c, the value is the same (3df8443). Two places are still rough, and both are planned work:

  • Errors inside a notation. A type mistake in an equation, such as a whole-number array times a float integral, is a type error before the program runs, but it underlines the whole call rather than the term inside the string that is wrong.
  • Shape and rank. They are still checked mostly while the program runs. A shape lint already proves some mismatches before it runs, where the extents are written down; equations and pipelines check theirs as they run.