MEP 12. Parametric Polymorphism

Field	Value
MEP	12
Title	Parametric Polymorphism
Author	Mochi core
Status	Draft
Type	Standards Track
Created	2026-05-08

Abstract

Mochi has the syntax of generics but not the inference. TypeVar exists, the grammar accepts type parameter lists, but call sites do not unify variables across argument and result positions. This MEP proposes a small System F-lite algorithm that wires TypeVar through the call site, removes most of the any-typed builtins, and gives callers precise types.

Motivation

The looseness around generic call sites is the largest single source of any in Mochi today. Builtins like len, first, and push are declared with any parameters because authors found inference would not propagate the variable. Tightening them is gated on this MEP. Once it lands, the soundness gains compound: less any everywhere, sharper error messages, fewer escape hatches.

Specification

Today

TypeVar{Name string} exists in types/check.go:104. The grammar admits type parameter lists on functions and on inline lambdas. Calls do not unify type variables across positions in a meaningful way, so the language has the syntax of generics but not the inference.

Concretely:

• fun id<T>(x: T): T parses and checks. Inside the body, T is a fresh type variable.
• A call site id(7) is typed by looking up id and walking the declared signature. The result type comes back as T, which then appears as the type of the let binding because there is no substitution from x : T to T = int.
• Many builtins are declared with AnyType{} parameters and return types instead of using TypeVar, because authors found inference would not propagate the variable.

The result is a system that accepts more programs than a sound parametric system would, with the looseness leaking into call sites that should be precisely typed.

Target

Standard ML or System F-lite. The deliverable for v0.11.0:

• Each generic function declares a list of type parameters.
• Each call site allocates fresh type variables for the parameters.
• Argument unification produces a substitution.
• The result type is the declared result with the substitution applied.
• Conflicting unifications are an error with a new code.
• Type parameters do not escape unless they appear in the declared result type.

Higher-kinded polymorphism is out of scope.

Inference algorithm

Hindley-Milner is overkill for what Mochi needs. A small algorithm:

1. On call f(a1, ..., an) where f has signature <G1, ..., Gk>(P1, ..., Pn) : R:
   1. Allocate fresh TypeVar instances T1, ..., Tk for G1, ..., Gk.
   2. Substitute Gi -> Ti in the parameter and result types.
   3. For each argument ai, infer Ai and call unify(Pi[s], Ai), accumulating the substitution.
   4. Return R[s]. If any free Ti remains in R[s], it is an escaped variable: error.
2. unify(s, t):
   • If both are concrete and equal, success.
   • If one is a TypeVar not yet bound, bind to the other (with occurs check).
   • If both are constructors of the same shape (ListType, MapType, FuncType), recurse on components.
   • Otherwise, error.

This is a single pass per call site. No global generalisation, which matches the language's value semantics where every function has a declared type.

Surface effects

Once parametric inference works, builtins are tightened:

• len(any) : int becomes len<T>([T]) : int plus a string overload.
• first<T>([T]) : T plus an option to indicate emptiness.
• push<T>([T], T) : [T].
• append<T>([T], T) : [T] plus a variadic form concat<T>([T], ...) : [T].
• keys<K, V>({K: V}) : [K].
• values<K, V>({K: V}) : [V].
• range(int, ...) : [int] stays monomorphic.

User-defined generics:

• id<T>(x: T) : T flows through inferred types.
• pair<A, B>(a: A, b: B) : Pair<A, B> requires generic struct declarations. The grammar does not have those today; we mark this as a follow-up.

Parametricity

Once inference is sound, we get the standard parametricity guarantees:

• A function of type T -> T either returns its argument or does not return.
• A function of type [T] -> [T] produces a list whose elements are drawn from the input.
• map<A, B>(xs: [A], f: fun(A): B) : [B] commutes with composition.

We add fixtures that snapshot these properties as runtime equality assertions on small examples.

Fixtures to author

For v0.11.0:

• generic_id_int_string. A fun id<T>(x: T): T called with both types, asserting the inferred result types.
• generic_first_list_int. first<T>([T]): T on [1, 2, 3].
• generic_pair_arg_unify. A two-parameter generic that requires the two arguments to share a type variable. Error case is a conflicting use.
• generic_freshness_per_call. Two calls of the same function with different argument types do not produce a unification error.
• generic_escaping_variable. A function that does not bind a type parameter through arguments or result is rejected.
• generic_constraint_arity. Calling a generic with the wrong number of explicit type arguments is rejected.

Once user-defined generic structs land, add:

• generic_struct_pair.
• generic_struct_constructor_inference.

Migration plan

1. Wire subst Type -> Type and unify(s, t, subst) cleanly. Keep the existing entry points until the new ones are proven against the suite.
2. Move builtins one by one from AnyType parameters to TypeVar parameters. After each move, run the type valid suite.
3. Remove the loose builtin declarations.
4. Tighten the call site checker to use the new substitution path.
5. Author fixtures and update MEP 9.

Rationale

A small, deterministic algorithm beats Hindley-Milner for our use case. We do not want let-generalisation. Every function in Mochi has a declared signature, so we know exactly which type variables to introduce. The trade-off is that we cannot infer signatures for unannotated functions, and we are happy with that.

Bounded quantification (T extends Comparable) is out of scope. The need has not surfaced in idiomatic Mochi code. We may revisit when sorted query support is generalised beyond the built-in numeric and string ordering.

Subtype polymorphism on tagged unions stays as it is in MEP 11. The generic parameter mechanism is independent of variant subtyping.

Backwards Compatibility

Tightening builtins from any to TypeVar is a breaking change for any program that relied on the looseness. The migration plan moves builtins one at a time so we can audit the breakage at each step.

User-defined generic functions that used to compile because of the loose typing may fail under the new algorithm. We pin the current behaviour in fixtures and document the change.

Reference Implementation

• types/check.go:104 — current TypeVar.
• types/check.go:148-387 — current unify (to be split into substitution-aware form).
• types/check.go:393-562 — builtins that need tightening.

Open Questions

• Generic struct declarations. Required for Pair<A, B> and friends. Grammar change is non-trivial.
• Type argument inference at call sites. Whether to require explicit type arguments at the call (id<int>(7)) or always infer. We prefer always-infer with explicit arguments as an opt-in.
• Bounded quantification. TAPL chapter 26. Defer.

References

• Benjamin C. Pierce, Types and Programming Languages, chapters 22 and 23.
• Andrew K. Wright, "Polymorphism for Imperative Languages without Imperative Types", 1995.

Copyright

This document is placed in the public domain.