AtlasLang: Three Types and One Honest Limitation

int, bool, str. That is the whole type system: no floats, no arrays, no user-defined types, no generics, no null. Each absence removes a genuinely hard problem, and the resulting system is small enough that every typing rule fits on a screen.

Annotations are optional on `let` and required on parameters and return types. That split is the most common design in modern statically typed languages, and it is not arbitrary. A let has an initializer sitting right there, so the type is locally derivable and writing it adds nothing. A parameter has no initializer, and inferring it would require looking at every call site — which turns a local check into a whole-program analysis and makes an error at one call site report at the function definition. Requiring the annotation makes a function signature a contract that can be checked independently of its callers, which is what makes separate compilation and good error locality possible at all.

Where a let does carry an annotation, it is checked against the initializer rather than ignored: let b: bool = 5; reports "b is declared bool but its initializer has type int", with the help "Change the annotation or the initializer so they agree." The symbol records whether its type was written or inferred, which is what lets a hover or a dump distinguish the two.

The operator rules are a table plus two special cases. Arithmetic — + - * / % — takes two int and yields int. Comparison — < <= > >= — takes two int and yields bool. Logical — && || — takes two bool and yields bool. The first special case is equality, which is defined for any two operands of the *same* type and is the one polymorphic operator here. The second is + on two str, which is concatenation — the same symbol meaning two different operations, which is exactly the ad-hoc polymorphism a checker has to resolve rather than an ambiguity it can push downstream.

A function declared to return int must return an int on every path. Checking that requires deciding whether a statement list definitely returns, and AtlasLang's alwaysReturns does it on the tree, before any CFG exists.

It is three rules. A return statement definitely returns. A block definitely returns if its statements do. An if definitely returns if it has an else and both arms do. That is all. A while never counts, because the checker does not evaluate the condition and therefore cannot know the body runs even once.

The consequence is that fn f(): int { while (true) { return 1; } } is rejected: "Not every path through f returns a value." Every human reading it knows the loop is entered and the function returns 1. The analysis does not, because to know it, it would have to evaluate the condition — and once an analysis starts evaluating conditions to decide reachability, it is asking a question that is undecidable in general.

This is the textbook shape of a sound but incomplete static analysis, and it is worth being precise about the two words. *Sound*: it never accepts a function that can fall off the end without returning — no false negatives, which is the direction that would produce a miscompilation. *Incomplete*: it rejects some functions that are actually fine — false positives, which are an inconvenience. Every useful static analysis makes exactly this trade, and which direction it errs in is the design decision. Erring towards rejection means a user occasionally has to restructure correct code; erring towards acceptance means the guarantee is not a guarantee.

Real languages make the same choice and produce the same complaint. Java rejects a method that ends in a while (true) without a return unless the condition is a compile-time constant, and the special case for constants is precisely an admission that the general question is not answerable. Rust, C# and Go all have their own version of this line, drawn in slightly different places, and every one of them generates the same bug report from users every year.

The checker reports and keeps going rather than throwing. That requires a mechanism, because the obvious implementation produces a flood: a variable that does not exist makes its enclosing expression untypeable, which makes *its* enclosing expression untypeable, and one mistake generates a message per enclosing node.

The mechanism is an absorbing error type. When a check fails, the node is given type error and a diagnostic is reported. Every rule that sees an error operand yields error and reports nothing. So print(nope + 1 * 2); where nope is undefined produces exactly one diagnostic — "Cannot find nope in this scope" — rather than one for the lookup, one for the addition and one for the print.

The same pass also offers suggestions, with a budget. On an unresolved name it computes edit distance against every visible name and suggests the closest — but only if the distance is within one edit for short names, or a third of the length for longer ones. Beyond that it says nothing, because a confidently wrong suggestion that happens to compile is worse than no suggestion at all. That budget is the whole of [[suggested-fixes]] in one number.

A third detail worth noticing: an if or while condition must be bool, and the diagnostic says so with the help "AtlasLang has no truthiness; write an explicit comparison." The language chose not to have truthiness, and the error message is where that choice is explained to the person who did not know it. Diagnostics are where language design decisions get communicated, and a message that only says "type error" wastes the opportunity.

The reason to care about any of this is what the rest of the compiler is then allowed to assume. Lowering never checks whether + has integer operands; the checker guaranteed it. The optimizer never checks whether a branch condition is a boolean; the checker guaranteed it. The VM never checks whether a MUL has two numbers on the stack. Every one of those checks would otherwise have to exist somewhere, at some cost, or be an unchecked assumption that a malformed program could violate.

This is the concrete form of a claim that is easy to state abstractly: a type system is not primarily a service to the programmer, it is a contract between compiler phases. The programmer-facing benefit — catching mistakes early — is real, and it is the same guarantee viewed from the other side.

It is also worth being clear about the limit, because it is the most misstated claim in this whole domain. A static type system proves the properties it models and nothing else. AtlasLang's proves that operators receive operands of the types they are defined for. It does not prove that a program terminates, that a division has a non-zero divisor, or that an integer stays in range — and let a = 10; let b = 0; print(a / b); type-checks perfectly and faults at run time. The type system was never asked about it.