Type system#

Nupp is gradually typed: anything unannotated or unresolvable is any and checks silently, so an untyped LuaJIT program is already a valid Nupp program. An annotation is what turns checking on, one declaration at a time.

local total = 1
total = total / 2

local count: integer = 1
count = count / 2 -- NUPP2001: number is not a integer

Inference#

The checker infers a type where an initializer settles it, and nowhere else.

A function with no result annotation is not checked against its return statements at all, and its calls produce any:

local function area(w, h)
    return w * h
end

local label: string = area(2, 3) -- checks clean

Annotating the result is what starts checking both ends:

local function area(w: number, h: number): number
    return w * h
end

local label: string = area(2, 3) -- NUPP2001: number is not a string

So does writing the function where a callable is already expected. A literal passed as a callback argument, or initializing an annotated binding, takes its parameter types from that slot and its result types from what its return statements produce. A slot whose result is a generic's binder is bound by the body, and a slot whose result is fixed is checked against it:

local function map<A, B>(xs: {A}, f: function(A): B): {B}
    local out: {B} = {}
    for i, x in ipairs(xs) do
        out[i] = f(x)
    end
    return out
end

local labels = map({1, 2}, function(n) return tostring(n) end) -- {string}
local build: function(): string = function() return 1 end -- NUPP2001

Mutable locals widen#

An unannotated mutable binding loosens, so that ordinary Lua keeps checking:

local i = 1
i = i / 2

local m = {a = 1}
m.b = 2

local n = nil
n = {}
print(n.field)

That is every case. 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. Only a mutable literal initializer widens, so a shape returned by a call keeps its type.

A const binding cannot be reassigned, so it keeps the literal it was given:

const tag = "ready" -- the literal type "ready"

A string literal's type is the bytes it denotes rather than the source that spells them, so two spellings of one string are one type:

const escaped: "\65" = "A" -- one byte, written two ways

An annotation keeps exactly the type you wrote, on a mutable binding too:

local j: integer = 1
j = j / 2 -- NUPP2001: number is not a integer

local shaped: {
    a: number
} = {a = 1}
shaped.b = 2 -- NUPP2004: no field "b" in {a: number}

Strict floor#

Strict adds two rules on top of what every file is checked for:

• An unknown variable is reported, for a name no project file answers to.
• An exported declaration needs a type annotation, so nothing untyped crosses a module boundary.

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:

.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, so models.g.nupp is the module models and require("models") finds it. A file can therefore 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

Gradual escape hatches#

any is compatible with everything in both directions, with one exception: a generic body's type parameter. A T stands for one unknown-but-fixed type there, and any is no more that type than a string is, so a value of any cannot be returned or stored as a T; narrow it or cast it. Reading a field of any gives any; calling it gives any with no arity or argument checks. It swallows unions too, so any | string is any:

local config: any = require("settings")
print(config.missing.deeper()) -- checks clean

as is an assertion the checker trusts completely, in both directions, and it erases at code generation:

local n = ("5" as any) as number -- checks clean

Use as where you know something the checker cannot. It reports nothing when you are wrong.

Where a value is genuinely untyped rather than deliberately unchecked, reach for unknown instead. Everything fits into it and it fits nowhere else, so each use has to narrow or cast first. See unknown, the top type for more information.

Deliberate unsoundness#

Some boundaries deliberately trust gradual or externally supplied information:

local ints: {integer} = {1, 2}
local nums: const {number} = ints -- a read-only view may widen
local writable: {number} = ints -- NUPP2001: a wider writer could corrupt ints

Mutable arrays and tuples preserve their element types through aliases. A fresh array literal may take the type of its context; an existing array widens only through a read-only view.

• 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 nupp.Closeable, it satisfies nupp.Closeable even before a runtime registrar has filled the members in.

Each is a place where the checker chose compatibility over proof. See is is a claim, not a proof for what a declared edge promises and what it does not.

Type-system guides#

One page per idea, in the order they build on each other:

• Primitive types: the builtin names, unions, optionals, collections, and aliases.
• Records and structs: nominal tables and fixed reifiable layouts.
• Affine types: compile-time type construction, exact cleanup identities, transfer-only values, and capability-preserving generics.
• Ownership: moves, borrows, aggregates, pinning, and lexical destruction.
• Interfaces: structural satisfaction, is, and metamethods.
• Refinements: the satisfies test a declaration carries.
• 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.
• Comptime types: member transforms, const parameters, matching, template literal types, and guarded recursion.
• Type packs: heterogeneous variadics, Lua value-list adjustment, protected calls, and coroutine protocols.
• Associated types: the types an interface leaves for its implementors to name.
• Narrowing: what proves what, and what does not.

FAQ#

When should a value be unknown instead of any?#

Reach for any when the code is deliberately unchecked, such as a boundary that has not been annotated yet. Reach for unknown when the value genuinely has no known type, such as a JSON decode or a pcall result, because it forces every later use to narrow or cast. See unknown, the top type for the tests that reach it.

Are Nupp types nominal or structural?#

Both, and the declaration decides which. A record and a struct are nominal, so two with identical fields are different types, while an interface and a table shape are satisfied structurally by anything carrying the members. See satisfaction is structural for what that admits.

Does anything survive to run time?#

Almost nothing. Annotations, aliases, interfaces, and as are erased, so generated Lua carries no type tags; record, struct, and interface default implementations emit the tables that ordinary Lua would have written by hand. See strictness.md for the two exceptions.