Lesson 6.1

Why Add a Type System?

What goes wrong without types. What Monk's checker catches before your program ever runs.

concepts 10 min read

A spell checker that understands meaning.

A spell checker catches typos. A grammar checker catches structural mistakes. A type checker is one level up from both: it catches mistakes in the meaning of your program.

"Add this number to that string" is syntactically valid Monk. The lexer and parser accept it without complaint. But it doesn't mean anything. A type checker rejects it before the program runs -- turning a crash you'd discover at 2am into a compile error you discover immediately.

Monk's type checker runs between the parser and the code generator. Every program that passes the checker is guaranteed to not fail from type errors. That guarantee is worth more than any runtime check.

What breaks without a checker.

Before Phase 6, Monk compiled and ran anything that parsed. Here are some programs that would have compiled, only to crash or silently misbehave at runtime:

Type mismatch on reassignment:

let count = 0
count = "hello"    // was int, now string -- silent drift

Missing return on a non-none function:

let double = (n int) int {
    if n > 0 {
        return n * 2
    }
    // if n <= 0, falls off the end -- undefined behavior in C
}

Wrong shape record:

type Point { x int, y int }
let p Point = { x: 1 }    // missing y -- runtime access to uninitialized memory

Meaningless equality:

if 5 == "5" {    // always false, but no error -- silent logic bug
    show("equal")
}

Each of these programs parses cleanly. The mistake is in the semantics -- the meaning -- not the syntax. That's exactly the class of errors a type checker is designed to catch.

What Monk's checker catches.

Monk's checker enforces a specific set of rules. Each one prevents a real class of bug:

1

Type inference and reassignment consistency.

The first assignment to a variable fixes its type. Reassigning a different type is a compile error. No silent drift.

2

Array element homogeneity.

int[] only holds ints. Assigning a string to an index, or appending the wrong type -- compile error. Homogeneous arrays are enforceable.

3

Record shape enforcement.

Missing fields, extra fields, wrong-type fields on a typed record literal -- all caught. The struct you build matches the type you declared.

4

All-paths return.

Every function declared to return a non-none type must return on every control flow path. Falling off the end of a function is a compile error.

5

Cross-type equality.

5 == "5" is a type error. So is comparing arrays, records, or functions with ==. Monk has no deep-equality semantics -- and the checker enforces that.

6

Function arity and argument types.

Wrong number of arguments, wrong type for a parameter -- caught at the call site. Including functions passed as arguments to higher-order functions.

What it intentionally doesn't catch.

Monk's checker is not trying to prove your program correct. It's trying to eliminate a specific, high-value class of bugs. Some things are deliberately left to runtime:

–

Out-of-bounds array access. The checker doesn't track the length of arrays, so arr[100] when the array has 3 elements is a runtime panic, not a compile error.

–

None access. Reading a property from a none value, or accessing an optional without checking it -- runtime error. The checker knows a value is optional, but doesn't enforce unwrapping.

–

Builtins with flexible return types. Functions like length work on both arrays and strings -- the checker types these as Any in slots where it can't express union types, so they flow through without complaint.

These are known limits, not oversights. A more powerful type system could close them -- but that's a future phase. The current checker catches the bugs that matter most without requiring a PhD to understand its rules.

Where the checker fits in the pipeline.

The checker is a new pass inserted between the parser and the code generator. The pipeline is now four stages: 

Source text
    ↓ Lexer     (tokens)
    ↓ Parser    (AST)
    ↓ Checker   (typed AST + error or ok)
    ↓ Codegen   (C source)

If the checker finds an error, it prints a message with line and column, and compilation stops. No C is generated. No binary is produced. The error is specific and actionable: 

error: hello.monk:3:9: cannot assign string to int variable 'count'

All three commands -- monk build, monk run, and monk check -- run the checker. You can't accidentally bypass it.

Key takeaways

1

Type errors are compile errors in Monk. They surface immediately, with a location, not at runtime after deployment.

2

The checker runs after the parser, before codegen. All three commands run it -- there's no way to skip it.

3

The checker catches inference drift, missing returns, wrong-shape records, array violations, cross-type equality, and call mismatches.

4

The checker's type information is also used by the code generator -- it's the foundation for scalar unboxing (lesson 6.4).