Does it make sense?

In 1957 Noam Chomsky offered a sentence to show that grammar and meaning are different things: “Colourless green ideas sleep furiously.” Every word is in its place, and it means nothing. Programs have the same problem. wahoo(lifes) parses beautifully, but if the program only ever declared lives, it asks for something that does not exist. question lives { … } is grammatical, but a question block needs a yes-or-no answer and lives is a number.

The phase that catches these is semantic analysis. In Wahoo it is checker.rs, and its output is no longer a syntax tree but a smaller, stricter representation (the HIR) in which every name has been replaced by the thing it refers to and every expression carries its type. The optimizer and the code generator only ever see that form, and they can trust it.

§Names and scopes

The first question about a name is which thing it means. Wahoo, like almost every modern language, uses lexical scoping: a name refers to the nearest enclosing declaration in the text of the program. A coin declared inside a question block lives until that block's }; inside it, it may shadow a variable of the same name declared outside.

world 1-1 {
  coin x = 1
  question star {
    coin x = "inner"   // a different x, of a different type
    wahoo(x)           // inner
  }
  wahoo(x)             // 1
}

The checker keeps a symbol table as a stack of scopes: entering a block pushes an empty scope, a coin adds a name to the top one, leaving the block pops it, and looking a name up searches from the top down. Popping is also the right moment to notice a variable that was declared and never read, which Wahoo reports as a warning.

Pipes are handled in two passes. The first collects the signature of every pipe in the file (name, parameter types, return type); the second checks the bodies. That is what lets a pipe call one defined further down, or call itself: by the time any body is checked, every signature is known.

§Types

A type is a promise about which values an expression can produce, and therefore about which operations make sense on it. Wahoo has three: coins (whole numbers), switch (star or goomba) and text. The surprise is that at run time all three are the same thing, a 32-bit integer: a switch is 0 or 1, and a text is the memory address of its bytes (chapter 04). Nothing in the machine stops you from adding an address to a number. The type checker does, before the program exists.

Languages differ in when they check. Statically typed languages (Wahoo, C, Java, Rust, Haskell) check before running, so a type error is a compile error. Dynamically typed ones (Python, JavaScript, Ruby) attach types to values and check each operation as it happens. They also differ in how forgiving they are: JavaScript answers "1" + 1 with "11" and "1" - 1 with 0, converting silently, whereas Python raises an error.

Type rules are usually written as inference rules: if the facts above the line hold, the fact below it holds. e : T reads “expression e has type T”. These are four of Wahoo's:

The checker applies them bottom-up over the tree: the type of lives + 1 is computed from the types of lives and 1, and then compared with what its context needs. When a rule fails, the expression gets a special error type that is compatible with everything. Without it, one unknown name in nope + 1 > 2 would produce three errors (the name, the addition, the comparison); with it, the user sees one.

§Type inference

Wahoo never makes you write the type of a variable: in coin lives = 3 the checker infers coins from the value. You can still annotate it (coin lives: coins = 3), and then the checker verifies that the value agrees. Only pipe signatures require types, which is the usual compromise in Rust, Swift, Kotlin, Go, C# and modern C++: types at the boundaries, inference inside.

Some languages go much further. Roger Hindley (1969) and, independently, Robin Milner (1978) showed how to infer the most general type of every expression in a program with no annotations at all, by collecting equations between unknown types and solving them by unification. The Hindley–Milner algorithm is the heart of ML, OCaml, F# and Haskell: you can write map f xs without a single type and the compiler works out that it has type (a → b) → [a] → [b] for any types a and b.

§Errors for humans

A compiler's error messages are its user interface, and for decades they were dreadful. The change came from languages that treated them as a design problem: Elm's “compiler errors for humans” (2015) and Rust's diagnostics set a standard of plain sentences, the exact location, and a concrete suggestion. Wahoo follows the same recipe. Each diagnostic has a precise title, a label under the offending code (where the Mushroom Kingdom is allowed to speak) and, where possible, a hint:

error[E205]: unknown name `lifes`
 --> level.wahoo:3:9
  |
3 |   wahoo(lifes)
  |         ^^^^^ Bowser has never heard of it
  = hint: did you mean `lives`?

The suggestion comes from the edit distance (Levenshtein, 1965): the least number of single-character insertions, deletions or substitutions that turn one word into another. lifes is at distance 1 from lives, so if that name is in scope it is offered. A threshold that grows with the length of the name keeps the suggestions plausible.

§Checks that cannot be perfect

A pipe that promises a value must deliver it on every path. The checker walks each body and asks: does every way through it end in a flag? A flag does; a question with an else does if both branches do; a loop never counts, because it may run zero times. This pipe is rejected:

pipe sign(n: coins) -> coins {
  question n > 0 {
    flag 1
  } else question n < 0 {
    flag -1
  }
}                        // and when n is 0?

So, more surprisingly, is pipe one() -> coins { question 1 < 2 { flag 1 } }, which obviously always returns. The checker does not evaluate conditions; it only looks at the shape of the code. That is not laziness. By Rice's theorem (1953), every non-trivial question about what a program does is undecidable, so any checker must either reject some correct programs or accept some wrong ones. Type systems and flow checks choose to be conservative: when in doubt, refuse, and let the programmer add an else. Java's “missing return statement” and Rust's “mismatched types” make the same choice.

The same kind of analysis, run the other way, flags unreachable code (statements after a flag, reported as a warning) and division by a literal zero (“this falls into a pit when it runs”).

§Desugaring

Some constructs exist only for the programmer's convenience. The checker rewrites them into a smaller core, so that later phases have fewer cases to handle. In Wahoo:

• power_up x becomes x = x + 1, and damage x by 5 becomes x = x - 5;
• else question … becomes an else block containing a question;
• every variable becomes a numbered slot (shadowed variables get different numbers), and every pipe a numbered function;
• every text literal is stored once, so two identical texts are the same text.

After this phase the program is small, explicit and known to be well-formed. The compiler can finally start thinking about the machine.

§References

1. N. Chomsky (1957). Syntactic Structures. Mouton.
2. H. G. Rice (1953). “Classes of Recursively Enumerable Sets and Their Decision Problems”. Transactions of the American Mathematical Society, 74(2).
3. V. I. Levenshtein (1965). “Binary Codes Capable of Correcting Deletions, Insertions, and Reversals” (in Russian). Doklady Akademii Nauk SSSR, 163(4).
4. R. Hindley (1969). “The Principal Type-Scheme of an Object in Combinatory Logic”. Transactions of the American Mathematical Society, 146.
5. R. Milner (1978). “A Theory of Type Polymorphism in Programming”. Journal of Computer and System Sciences, 17(3).
6. B. C. Pierce (2002). Types and Programming Languages. MIT Press.
7. E. Czaplicki (2015). “Compiler Errors for Humans”. elm-lang.org blog.