Skip to main content

MEP 4. Type System

FieldValue
MEP4
TitleType System
AuthorMochi core
StatusInformational
TypeInformational
Created2026-05-08

Abstract​

Mochi has a small structural type system with nominal records and unions. This MEP documents the type kinds present in the implementation today, the equality and unification rules used by the checker, and the numeric tower that drives binary operator typing.

Motivation​

The type system is the contract between the checker and the runtime. A single misunderstanding about whether int and int64 are equal, or whether any is a top type or a bottom type, can produce a soundness gap that is difficult to track down. Documenting the kinds and their relationships up front makes future changes deliberate.

Specification​

The Type interface​

types/check.go:12-14. Every type kind implements:

type Type interface {
    String() string
}

There is no equality method on the interface. Equality is computed externally by equalTypes in types/infer.go and structural unification is done by unify in types/check.go:148-387. Two types are considered equal when their String() representations agree, with carve-outs for variance and any.

Kinds present today​

Listed in source order at types/check.go:16-148.

Primitive kinds:

  • IntType. Default integer width. Backed by Go int64 at runtime but the surface type is int.
  • Int64Type. Distinguished only where the runtime needs it, for example the result type of now(). Unifies with IntType for arithmetic.
  • FloatType. IEEE 754 double precision.
  • BigIntType. Arbitrary precision integer.
  • BigRatType. Arbitrary precision rational.
  • StringType. UTF-8 byte sequence.
  • BoolType. true or false.
  • VoidType. Result type of statement-only operations like print.

Structural kinds:

  • ListType{Elem Type}. Homogeneous ordered sequence.
  • MapType{Key Type, Value Type}. Hash map keyed by Key.
  • OptionType{Elem Type}. Declared but not produced by inference today. See MEP 10.
  • GroupType{Key Type, Elem Type}. Internal type carried by the into Name clause of a group by query.
  • StructType{Name, Fields, Order, Methods}. Nominal record. Order preserves the declaration sequence so output and JSON encoding are deterministic.
  • UnionType{Name, Variants}. Nominal sum of struct-shaped variants. Variants is a map but the iteration order should be stable: the variant order from the declaration is captured when the type decl is processed.

Function kind:

  • FuncType{Params, Return, Pure, Variadic}. The Pure flag is computed but not enforced anywhere yet. The Variadic flag is exercised by builtins like concat and range.

Polymorphism kinds:

  • TypeVar{Name}. Carried by generic function declarations. Not yet used for full inference. See MEP 12.

Top kind:

  • AnyType{}. Unifies with everything in both directions. This is the primary unsoundness escape hatch and is documented in detail in MEP 10 and MEP 11.

What is missing​

The list of kinds the language does not have today:

  • No nominal alias kind. type Id = int is collapsed at resolve time to its target.
  • No tuple kind. A heterogeneous fixed-length sequence has no surface type.
  • No record subtype kind separate from StructType. Width subtyping is decided by name plus field set, not by an explicit row variable.
  • No effect kind. The Pure flag is on the function type, not a separate kind.
  • No reference kind. Mutability is a property of the binding (var versus let), not of the type.
  • No existential or universal kind beyond TypeVar for generics.
  • No first-class type kind. Types cannot be passed as values.

Typing judgement​

We use the standard form Γ ⊢ e : τ where Γ is the lexical environment. Mochi's Γ carries:

  • Variable bindings with mutability flag (Env.SetVar).
  • Type bindings (Env.SetType).
  • Function bindings (Env.SetFunc).
  • Stream and agent bindings.

Environments are linked. A child environment delegates lookups to its parent and shadows on write. See types/env.go for the API.

Equality and unification​

Two types are equal when they are structurally identical at every level. The exact rules in equalTypes (search types/infer.go):

  • Two primitives are equal iff their kinds match. IntType and Int64Type are not equal here, although arithmetic widens between them.
  • Two list types are equal iff their element types are equal.
  • Two map types are equal iff key and value types are equal.
  • Two function types are equal iff they have the same arity, the same parameter types pairwise, the same return type, and the same Variadic flag.
  • Two struct types are equal iff their Name fields agree. This is nominal. Two structurally identical anonymous structs declared separately are not equal because their generated names differ.
  • Two union types are equal iff their Name fields agree.
  • AnyType is equal to everything. This is the unsoundness hatch.

Unification is the same predicate but propagates substitutions for TypeVar. See types/check.go:148-387.

Numeric tower​

Listed from narrowest to widest, but the relations are not a clean total order:

int  ⊂  int64  ⊂  bigint
int          ⊂   float
int          ⊂   bigrat
bigint       ⊂   bigrat
float        ⊄   bigrat   (mixed becomes bigrat in practice today)

The actual rules used by inferBinaryType:

  • Integer divide (/ between two ints) returns int.
  • Either side bigrat widens to bigrat.
  • Either side int64 and the other side int or int64 returns int64.
  • Either side float and both sides numeric returns float.
  • Either side bigint returns bigint.
  • Two ints return int.
  • String plus string returns string.
  • List plus list returns the same list type if elements agree, or [any] otherwise.
  • Otherwise any.

The + rule on lists is silently widening, which is a soundness concern when one side is mutated.

Rationale​

Keeping String() as the only required method on Type makes the kind table easy to extend. Equality and unification are external because they need to be customisable for variance and substitution.

AnyType exists because the alternative is making every builtin generic, which we cannot do until parametric polymorphism (MEP 12) lands. AnyType is a debt; it is not a design choice.

The numeric tower is conservative on purpose. We prefer to widen to bigrat when in doubt rather than silently lose precision.

Backwards Compatibility​

Informational. No backward compatibility implications.

Reference Implementation​

  • types/check.go:12-14 — Type interface.
  • types/check.go:16-148 — kind definitions.
  • types/check.go:148-387 — unify.
  • types/infer.go — equalTypes and operator typing.
  • types/env.go — environment API.

Pinned decisions​

Reading a missing map key​

For m: map<K, V> and a key k that is not present in m, the expression m[k] will infer to OptionType{V}. Callers must unwrap the option before using the value at type V. The runtime will produce the absent variant instead of the zero value.

We considered three options before pinning this:

  1. Type m[k] as V?. Picked.
  2. Require an explicit default at the call site, for example m[k] ?? default, with a checker error otherwise.
  3. Raise a typed runtime panic.

Option 1 wins on consistency. MEP 10 A2 already commits OptionType as the destination for null and MEP 10 C1 adds the T? shorthand. Once that work lands, missing-key access slots into the same shape without introducing a second mechanism (no new ?? operator, no new panic class). Option 2 would require a new operator and option 3 would force defensive in m checks at every call site.

This is a deferred change. Today the runtime returns the zero value of V, which for non-zero-bearing types is a progress violation. The current behaviour is pinned by tests/types/valid/missing_map_key.mochi so the future tightening is a deliberate breaking change. The implementation work is tracked alongside MEP 10 A2.

Open Questions​

  • Tuple kind. A heterogeneous fixed-length sequence has no surface today. We will need it once query result tuples are generalised.
  • Option kind. OptionType exists but is not produced by inference. MEP 10 ties this to the null soundness gap and to the missing-map-key decision above.
  • Numeric ordering. float and bigrat mix awkwardly. We have not decided whether to widen to bigrat or to refuse the mix.

References​

  • See MEP 5 for how these kinds are produced by inference.
  • See MEP 10 for the soundness gaps these kinds expose.

This document is placed in the public domain.