Type system#

Nupp is gradually typed. Anything unannotated or unresolvable is any and checks silently, so an untyped LuaJIT program is a valid Nupp program that reports nothing. Annotations are what turn checking on, one declaration at a time.

That sentence is the design. Everything below follows from it.

What is inferred, and what is not#

 Position                     Inferred?
 ───────────────────────────  ────────────────────────────────────
 Local from its initializer   Yes; mutable bindings widen — see below
 Function parameters          No; an unannotated parameter is any
 Function return types        No; the body's returns go unchecked
 Short-function body          Yes, one inferred result
 Unknown global               any, silently

A function with no return annotation is not checked against its return statements at all. Annotating the return is what starts checking them.

Mutable locals widen#

This is the rule people trip over. A mutable binding with no annotation deliberately loosens, so that ordinary Lua keeps working:

A const binding keeps an inferred literal type, and an annotation keeps exactly the type you wrote:

An annotation can also keep a narrower type on a mutable binding:

The four widening cases are: a literal type on a mutable binding collapses to its base, integer widens further to number, a shape built from a table literal collapses to table, and nil becomes any. A shape returned by a call keeps its type — only mutable literal initializers widen.

The practical reading: annotate when you want the constraint, leave it off when you want the Lua behaviour. Both are supported positions.

The strict floor, and which files hold it#

Strict adds exactly three things:

  • NUPP2105 — unknown variable, for a name no project file answers to.
  • NUPP2106 — an exported declaration needs a type annotation, so nothing untyped crosses a module boundary.
  • NUPP2503 — the lossy-narrowing lint, on a narrow integer annotation initialized from a wider numeric type. This lint is unreachable without strict mode.

Everything else is checked identically either way.

Which files hold that floor is decided by their extension, so a file says what it is where anyone reading it can see it:

 Extension  Floor     What it means
 ─────────  ────────  ──────────────────────────────────────────────
 .nupp      strict    Ordinary Nupp.
 .g.nupp    gradual   The typed syntax, without the floor.
 .d.nupp    gradual   Describes an interface somebody else implements.
 .lua       gradual   Plain Lua, and the typed layer is refused there.

.g.nupp is the opt-out, and it is a whole file at a time on purpose: a per-declaration escape would be a second way to say any, which the language already has. The module name drops the marker — models.g.nupp is the module models, and require("models") finds it — so a file can change layer without anything that requires it noticing.

.d.nupp is exempt because a declaration file describes foreign code. LuaJIT's string.buffer.encode(v: any): string really does take any Lua value, and no annotation written here changes what LuaJIT accepts.

--strict overrides the lot, holding every file to the floor including the .g.nupp ones. That is the tool for finding out what adopting one would cost:

nupp check --strict

any, and the escape hatches#

any is compatible with everything in both directions. Reading a field of any gives any; calling it gives any with no arity or argument checks. It also swallows unions — any | string is any.

There is no unknown and no never, and no bottom type of any kind. Subtracting every member of a union leaves the union alone rather than producing an empty type.

as is an assertion the checker trusts completely, in both directions:

It erases at code generation. Use it where you know something the checker cannot; it will not warn you when you are wrong.

Deliberate unsoundness#

Four rules are unsound on purpose, because the sound version rejects too much ordinary Lua:

  • Arrays are covariant. {integer} is accepted where {number} is wanted.
  • Shape fields are covariant, not invariant, even though they are mutable.
  • table is gradual in both directions. Every table-shaped type is a table, and a table may be used where any of them is wanted. It is closer to "any, for tables" than to a top type.
  • A declared is edge is trusted rather than proved. If a record says is Closeable, it satisfies Closeable even before a runtime registrar has filled the members in.

Each is a place where the checker chose compatibility. Knowing which four they are is more useful than pretending they do not exist.

Type-system guides#

  • Primitive types — the builtin names, unions, optionals, collections, and aliases.
  • Records and structs — nominal tables and FFI cdata.
  • Interfaces — structural satisfaction, is, and metamethods.
  • Property capabilities — independent read and write views.
  • Unions — literal sets, tagged unions, and exhaustiveness.
  • Intersections — capability composition and provable emptiness.
  • Overloads and overrides — callable intersections, separate method bodies, interface defaults, and constructors.
  • Generics — type parameters, inference, and bounds.
  • Type-level computation — member transforms, const parameters, matching, template literal types, and guarded recursion.
  • Type packs — heterogeneous variadics, Lua value-list adjustment, protected calls, and coroutine protocols.
  • Narrowing — what proves what, and what does not.

For where a declaration lives and how modules see it, read declarations and modules.