MEP 4. Type System

Field	Value
MEP	4
Title	Type System
Author	Mochi core
Status	Informational
Type	Informational
Created	2026-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. Misunderstandings about whether int and int64 are equal, or whether any is a top type or a bottom type, produce soundness gaps that are hard to track down later. This MEP documents the kinds and their relationships so future changes are 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:150-387. The fallthrough case in equalTypes is reflect.DeepEqual, with explicit carve-outs for Int/Int64 interop, union/struct member matching, and option types. unify uses a different rule for AnyType: see below.

Kinds present today

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

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 (tracked in #21188). 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

The exact rules in equalTypes (types/infer.go):

• IntType and Int64Type are equal to each other. The code has explicit carve-outs so int64 result types (for example from now()) unify cleanly with int variables.
• 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 arity, parameter types, return type, and Variadic flag all match.
• Two struct types are equal by reflect.DeepEqual; in practice names are unique so this reduces to name equality.
• Two union types are equal by name.
• A StructType is equal to a UnionType when the struct is one of the union's variants. This is what allows match arms typed as variant structs to satisfy a union binding.
• AnyType is equal only to another AnyType in equalTypes. It is unify that accepts AnyType on either side as a match; that is the unsoundness escape hatch.

Unification propagates substitutions for TypeVar on top of the equality rules. See types/check.go:150-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 silently widens to [any] on element type mismatch. This is a soundness gap tracked in #21187.

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-140: kind definitions.
• types/check.go:150-387: unify.
• types/infer.go: equalTypes and operator typing.
• types/env.go: environment API.

Pinned decisions

Reading a missing map key

Once MEP 10 A2 lands, m[k] for an absent key will infer to OptionType{V}. Callers must unwrap the option before using the value at type V.

Three options were considered:

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

Option 1 wins because it reuses the same OptionType shape that MEP 10 A2 gives null and MEP 10 C1 gives the T? shorthand. Option 2 needs a new operator; option 3 forces in m guards at every call site.

Today the runtime returns the zero value of V. For non-zero-bearing types this is a progress violation. The current behaviour is pinned by tests/types/valid/missing_map_key.mochi; the future tightening is a deliberate breaking change tracked in #21186 alongside MEP 10 A2.

Open Questions

• Tuple kind. No surface type for heterogeneous fixed-length sequences. Needed once query result tuples are generalised.
• Option kind. OptionType exists but is not produced by inference today. Tied to the null soundness gap in MEP 10.
• Numeric ordering. float and bigrat mix awkwardly. No decision yet on whether to widen to bigrat or reject the mix.

References

• MEP 5: how these kinds are produced by inference.
• MEP 10: soundness gaps these kinds expose.

Copyright

This document is placed in the public domain.