Skip to main content

MEP 5. Type Inference

FieldValue
MEP5
TitleType Inference
AuthorMochi core
StatusInformational
TypeInformational
Created2026-05-08

Abstract​

Type inference in Mochi is local. Each expression form has a deterministic rule that maps operand types to a result type. There is no global solver and no constraint generation phase. This MEP documents the inference rules per construct so contributors can reason about a single expression without scanning the whole infer.go file.

Motivation​

Inference rules are easy to break by accident. A new operator added to the grammar has no result type until someone decides one. A new collection literal has to interact with empty-literal hinting. Without a single record of the rules, contributors guess, and the guesses drift.

Specification​

Entry points​

types/infer.go:17-69.

ExprType(e *parser.Expr, env *Env) Type
ExprTypeHint(e *parser.Expr, hint Type, env *Env) Type

ExprType is the basic inference call. ExprTypeHint accepts a hint and uses it to type empty list and map literals where context is the only signal. Both return AnyType{} when no better answer is found.

The expression entry point delegates to inferBinaryType, which flattens precedence, then inferUnaryType, inferPostfixType, and finally inferPrimaryType.

Operator precedence and inference​

types/infer.go:89-198. The order of resolution:

1. *  /  %
2. +  -
3. <  <=  >  >=
4. ==  !=  in
5. &&
6. ||
7. union  union all  except  intersect

Within a level the algorithm reduces left to right. The result type table per operator is in MEP 4 under "numeric tower" and the same logic in code at types/infer.go:114-191.

A subtle order dependency exists in numeric mixes. Because the algorithm folds left to right, bigint - float and float - bigint can produce different result types depending on rule firing order. Fixtures for each pair are required (see MEP 9).

Inference for declarations​

let x = e        ->  Γ' = Γ ∪ { x : ExprType(e) }, immutable
var x = e        ->  Γ' = Γ ∪ { x : ExprType(e) }, mutable
let x : T        ->  Γ' = Γ ∪ { x : T }, immutable
let x : T = e    ->  Γ' = Γ ∪ { x : T },
                     require unify(T, ExprType(e))
var x : T = e    ->  Γ' = Γ ∪ { x : T },
                     require unify(T, ExprType(e))

let with neither type nor value raises T000.

fun f<G1, G2>(p: T) : R { ... } introduces type variables in scope for the function body but does not generalise them across calls today. See MEP 12.

Inference for control flow​

  • if cond { ... } requires cond : bool (T040). The body inherits the parent environment.
  • while cond { ... } requires cond : bool.
  • for x in source { ... }:
    • if source : [T] then x : T in the body.
    • if source : {K: V} then x : K in the body.
    • if source : int (range form) then x : int.
    • any other shape raises T022.
  • for x in a..b { ... } requires both bounds : int and binds x : int.

Inference for collections​

  • [] with no hint has type [any].
  • [e1, ..., en] has type [T] where T is the equal type of all ei if they agree, else any.
  • [] hinted with [T] has type [T].
  • {} with no hint has type {any: any}.
  • {k1: v1, ..., kn: vn} has type {K: V} where K is the equal type of all ki (else any) and same for V.
  • xs[i] requires xs : [T] | string | {K: V} and i : int for list and string, or i : K for map. Returns T, string, or V. List index out of range is a runtime error.
  • xs[a:b] requires xs : [T] or string and bounds : int. Returns the same kind. Maps reject slicing (T017).

Inference for queries​

The query type is computed in types/check.go via the query plan builder. The shape:

from x in xs                where xs : [T]
let xprime : T              the iteration variable
{ from y in ys }*           additional sources stack as nested loops
{ join z in zs on c }*      join clauses
[ where p ]                 require p : bool
[ group by k into g ]       g : group<K, T>
[ sort by s ]
[ skip n ] [ take n ]       require n : int
select [ distinct ] r       result type list of ExprType(r)

The final result is ListType{Elem: ExprType(r)}. There is no narrower relation between sources and the projection result; the projection can produce any structurally typed value.

Aggregate functions inside select are special cased:

  • count(g) : int where g is a list or group.
  • sum(g) : int | float | bigint | bigrat matching the element type.
  • avg(g) : float | bigrat.
  • min(g), max(g) : T where g : [T] and T is comparable.

Anything else falls through to general expression inference. The fall-through is part of why MEP 10 flags loose verification of select results.

Inference for matches​

match e { p1 => r1, ..., pn => rn }.

  • The result type is the join of ExprType(ri). With the current join that almost always means the common type or any.
  • Pattern shapes:
    • Literal pattern: requires the literal type to be equal to ExprType(e). Pattern binds nothing.
    • Identifier pattern: binds the name to ExprType(e).
    • Underscore: binds nothing, never fails.
    • Variant call pattern: requires e to have a UnionType containing the named variant. Binds field positions to the variant fields.

Exhaustiveness is not enforced today. See MEP 13.

Inference for casts​

e as T. The result type is T. There is no compatibility check between the source and target type. This is a documented hole.

Inference for function calls​

f(a1, ..., an). Requires Γ(f) to be a FuncType. Then:

  • If f is variadic with m formal params, the first m - 1 args unify normally and the rest must each unify with the last param.
  • Otherwise n must equal m (else T006 or T039).
  • Each ai is checked against Γ(f).Params[i]. Mismatch yields T007.
  • The call's type is Γ(f).Return after substitution.

For pure functions, the Pure flag is set but the checker does not yet require pure call sites in any context. The flag is reserved for future enforcement.

Inference for tagged unions​

A union type U = A(x: int) | B(s: string) enters the environment as:

  • U bound to UnionType{Name: "U", Variants: {"A": ..., "B": ...}}.
  • A bound to a constructor function (int) -> U.
  • B bound to a constructor function (string) -> U.

So let u = A(7) gives u : U. Pattern matching is the only way to recover the variant in a checked way today.

Inference for I/O expressions​

  • load p as T with opts. Type is [T] if the format is "json" with an array file, T if format is "json" with a single object, and [T] for "csv". The default format is "csv".
  • save x to p with opts. Type is void.
  • fetch url with opts. Type is any (the body of the response is decoded based on options).

Inference for closures and lambda​

fun(p1, ..., pn) : R => body produces type FuncType{Params: [P1, ..., Pn], Return: R, Pure: false}. With a block body the return type is inferred from the trailing return statements. Free variables in the body are captured by reference, which has implications for mutation that MEP 15 documents.

Rationale​

Local inference is enough for a small language. Global constraint solving would buy us better generic inference but at the cost of harder-to-explain error messages. We prefer to keep error messages tied to concrete source positions.

The "join" we use for if branches and match arms is conservative: we widen to any when in doubt. That is part of why MEP 10 calls out any as the most common loss of information.

Backwards Compatibility​

Informational. No backward compatibility implications.

Reference Implementation​

  • types/infer.go:17-69 — entry points.
  • types/infer.go:89-198 — operator precedence and inference.
  • types/infer.go:114-191 — operator result types.
  • types/check.go — query plan builder and special-cased aggregates.

Open Questions​

  • Tighter join. Should the join of two arms produce the union of their types instead of any? That would tighten match results but requires anonymous union types.
  • Generic call inference. Currently call sites do not unify type variables across positions. MEP 12 proposes the change.
  • Aggregate fall-through. select falls through to general expression inference for non-aggregates. We should reject any projections in strict mode.

References​

  • See MEP 4 for the kinds inference produces.
  • See MEP 12 for the polymorphism upgrade.

This document is placed in the public domain.