Additional library code that is not written in the Wuffs programming language. See the auxiliary code note for more details.
A named rule for asserting new facts. See the assertions note for more details.
A compile-time directive that introduces a new fact (or fails to compile, if the assertion cannot be proved). See the assertions note for more details.
An API restriction that e.g. the foo method needs to be called before the
bar method. Out of order calls may result in a "#bad call sequence" error.
A function that can suspend execution and, when called again later, resume where it left off, in the middle of the function body. See the coroutines note for more details.
A type that depends on another value. For example, a variable n's type might
be "the length of s", for some other
slice-typed variable s. Dependent
types are a way to implement compile-time bounds
checking, but they're not the only way, and
there's more to programming languages than their type systems. Wuffs does not
use dependent types.
An extension of the type system, such as purity (freedom from side effects), applied to functions. See the effects note for more details.
Syntactically, effects are the exclamation and question marks, ! and ?, at
function definitions and function calls. These denote impure and
coroutine functions.
A boolean expression (e.g. x > y) that is guaranteed to be true at a given
point in a program. See the facts note for more details.
A unit of time. One flick (frame-tick) is
1 / 705_600_000 of a second.
A function that can modify only local state (to store the result of computation), not global or system state. See the hermeticity note for more details.
Arithmetic on numerical ranges. See the interval arithmetic note for more details.
A function whose first argument (the receiver) has special syntactic support.
For example, an expression like foo.bar(etc) might effectively be a function
call whose first argument is foo and whose remaining arguments are the etc.
It is syntactic sugar for type_of_foo__bar(self: foo, etc). On the callee
(not the caller) side, that implicit argument is often named self or this,
depending on the language (e.g. Wuffs per se uses this, but Wuffs transpiled
to C uses self to avoid confusion with C++'s this). Wuffs has no free
standing functions, only methods.
Arithmetic that wraps around at a certain modulus, such as 256 for the
base.u8 type. For example, if x is a base.u8 with value 200, then (x + 70) has value 270 and would overflow, but (x ~mod+ 70) has value 14.
A ranking of arithmetic operators so that an expression like a + b * c is
unambiguous (for the computer), equivalent to exactly one of (a + b) * c or,
more conventionally, a + (b * c). While good for brevity, Wuffs does not have
operator precedence: the bare a + b * c is an invalid Wuffs expression and
the parentheses must be explicit. The ambiguity (for the human) can be a source
of bugs in other security-conscious file format
parsers.
Some binary operators (+, *, &, |, ^, and, or) are also
associative: (a + b) + c and a + (b + c) are equivalent, and can be written
in Wuffs as a + b + c.
A basic type further constrained to a subset of its natural
range. For example, if x has type base.u8[0 ..= 99] then it is an unsigned 8-bit integer whose value must be less than
100. Without the refinement, x could be as high as 255.
Bounds may be omitted, where the base integer type provides the implicit bound.
base.u8[0 ..= 99] and base.u8[..= 99] are the same type.
base.u8[0 ..= 99] and base.u32[0 ..= 99] are two different types, as they
have different unrefined types. They can have different run-time
representations.
Non-nullable pointer types can be thought of as a refinement of regular pointer
types, where the refined range excludes the nullptr value.
Arithmetic that stops at certain bounds, such as 0 and 255 for the
base.u8 type. For example, if x is a base.u8 with value 200, then (x + 70) has value 270 and would overflow, but (x ~sat+ 70) has value 255.
The set of facts at a given point in a program.
A programming language mechanism (e.g. an unsafe keyword or package) to
circumvent the language's safety enforcement, typically used for performance or
very low level programming. Unlike some other memory-safe languages, Wuffs
doesn't have such an 'escape hatch'.
An empty struct (with no fields) used as a placeholder. Every written-in-Wuffs function is a method: the receiver is mandatory. A Wuffs utility type's methods are to its package what C++ or Java's static methods are to its class.
"Utility type" is merely a Wuffs naming convention. For example, Wuffs' base
package has a type called base.utility, similar to how the zlib package has
a type called zlib.decoder. Unlike "dependent type" or "refinement type",
"utility type" is not a phrase used in programming language type theory.
Scratch space in addition to the primary destination buffer. For example, in image decoding, the primary destination buffer holds the decoded pixels, but while decoding is in progress, a decoder might want to store additonal state per image column.
Wuffs' codecs can state the (input dependent) size of their work buffer needs as a range, not just a single value. Callers then have the option to trade off memory for performance.