MLTT Type Checking Guidance

This document is guidance for the experimental MLTT checker. It is not yet a normative language specification. Its purpose is to give implementers and reviewers a shared vocabulary before Cosmo grows dependent pattern matching, trait-aware checking, effect-aware checking, and object-safety checks.

The first implementation slice lives under packages/cosmoc/src/types/mltt/packages/cosmoc/src/types/mltt/, with a Scala-side mirror under packages/cosmo0/src/main/scala/cosmo0/tyck/mltt/TypeChecker.scalapackages/cosmo0/src/main/scala/cosmo0/tyck/mltt/TypeChecker.scala. It provides explicit MLTT core data, profile-aware diagnostics, bidirectional check/infer entry points, conservative metavariable records, Nat/Vec metadata fixtures, and the first declared conversion strategy mltt.whnf-conversionmltt.whnf-conversion. Selecting mltt.coremltt.core or mltt.dependent-patternsmltt.dependent-patterns in cosmo0 routes directly to the Scala MLTT checker for assertion fixtures; the dependent-pattern profile is an MLTT extension that invokes dependent-pattern elaboration. Ordinary Cosmo source still needs a surface elaborator before it can produce MLTT core artifacts.

The key design rule is:

MLTT is one checker profile, not the whole language.

MLTT is one checker profile, not the whole language.

Cosmo can host multiple checker profiles. A small MLTT checker is useful even when it rejects traits, effects, async, object dispatch, C++ imports, macros, and dependent pattern matching in its first version.

Martin-Lof type theory gives a compact dependent core:

• TypeType universes classify types.
• PiPi types classify dependent functions.
• SigmaSigma types classify dependent pairs.
• Inductive families classify indexed data such as Vec[A, n]Vec[A, n].
• Equality types classify proofs that two terms are propositionally equal.
• Conversion checks definitional equality by reducing pure transparent terms.

This is a good experimental core for Cosmo because it can support future dependent pattern matching without requiring every checker to become a proof assistant.

Keep two layers separate:

surface Cosmo:
  friendly syntax, traits, effects, async, objects, imports, pattern clauses
MLTT core:
  explicit binders, explicit terms, explicit conversion, explicit diagnostics

surface Cosmo:
  friendly syntax, traits, effects, async, objects, imports, pattern clauses
MLTT core:
  explicit binders, explicit terms, explicit conversion, explicit diagnostics

The checker should trust the core, not the surface syntax. Surface constructs are elaborated into core artifacts before or during checking.

The initial checker should be bidirectional:

Γ |- t <= A        check term t against expected type A
Γ |- t => A        infer type A for term t
Γ |- A == B        definitional equality / conversion
Γ |- E1 <= E2      effect-row inclusion, when effect profiles are added
Γ |- O solved      trait or capability obligation, when trait profiles are added

Γ |- t <= A        check term t against expected type A
Γ |- t => A        infer type A for term t
Γ |- A == B        definitional equality / conversion
Γ |- E1 <= E2      effect-row inclusion, when effect profiles are added
Γ |- O solved      trait or capability obligation, when trait profiles are added

The first MLTT profile only needs the first three judgments. Effect and trait judgments are listed because later profiles should layer them around the core instead of hiding them inside conversion.

A useful first core has these shapes:

Var(name or index)
Universe(level)
Pi(name, domain, body)
Sigma(name, first, second)
Lambda(name, annotation, body)
Apply(function, argument)
Pair(first, second)
Fst(pair)
Snd(pair)
Let(name, value, body)
Inductive(name, params, indices)
Constructor(name, args)
Eq(type, left, right)
Refl(value)
Neutral(head, spine)
Error

Var(name or index)
Universe(level)
Pi(name, domain, body)
Sigma(name, first, second)
Lambda(name, annotation, body)
Apply(function, argument)
Pair(first, second)
Fst(pair)
Snd(pair)
Let(name, value, body)
Inductive(name, params, indices)
Constructor(name, args)
Eq(type, left, right)
Refl(value)
Neutral(head, spine)
Error

Implementers can choose de Bruijn indices, de Bruijn levels, or stable local IDs. For Cosmo compiler code, stable IDs plus explicit context entries are easier to debug. For conversion and substitution, de Bruijn levels often make alpha-equivalence and reification back to core syntax cleaner.

Pi type:

(A: Type0) -> (x: A) -> A

(A: Type0) -> (x: A) -> A

Sigma type:

Sigma(x: A). B(x)

Sigma(x: A). B(x)

Equality type:

Eq(A, x, x)
Refl(x)

Eq(A, x, x)
Refl(x)

Nat metadata:

Nat : Type0
Z   : Nat
S   : Nat -> Nat

Nat : Type0
Z   : Nat
S   : Nat -> Nat

Vec metadata:

Vec(A: Type0, n: Nat) : Type0
Nil  : Vec(A, Z)
Cons : (k: Nat) -> A -> Vec(A, k) -> Vec(A, S(k))

Vec(A: Type0, n: Nat) : Type0
Nil  : Vec(A, Z)
Cons : (k: Nat) -> A -> Vec(A, k) -> Vec(A, S(k))

Conversion:

(fun x: A => x)(y) == y
let z = y; z == y

(fun x: A => x)(y) == y
let z = y; z == y

Use check mode when the expected type is known:

check(lambda, Pi)
check(pair, Sigma)
check(constructor, expected inductive family)

check(lambda, Pi)
check(pair, Sigma)
check(constructor, expected inductive family)

Use infer mode when the term naturally exposes its type:

infer(variable)
infer(application)
infer(projection)
infer(annotated term)

infer(variable)
infer(application)
infer(projection)
infer(annotated term)

This avoids pretending that a dependent language has complete inference. It also gives better diagnostics because the checker knows whether it was trying to check against a specific type or synthesize one.

Conversion answers:

Are these two core terms definitionally equal?

Are these two core terms definitionally equal?

The first implementation should only reduce:

• beta-redexes from applying lambdas;
• transparent pure lets;
• transparent total definitions admitted by the MLTT profile;
• eliminator or case reductions only after those features are introduced.

It must not run:

• async computations;
• generator/yield computations;
• throwing computations;
• IO;
• mutation;
• arbitrary compile-time reflection;
• general recursive definitions.

This boundary keeps type checking deterministic and prevents effectful programs from deciding type equality.

Normalization is a service used by conversion. It is not the whole checker.

The first MLTT implementation should expose a stable conversion API and use a small first-stage strategy:

WHNF + structural comparison:
  simpler to implement incrementally
  enough for many early tests
  can need repeated normalization in nested comparisons

WHNF + structural comparison:
  simpler to implement incrementally
  enough for many early tests
  can need repeated normalization in nested comparisons

This first profile can be named:

mltt.whnf-conversion

mltt.whnf-conversion

Other normalization strategies need separate research before they become design commitments. This guidance intentionally does not evaluate or recommend a specific advanced strategy. Any later proposal should bring its own references, formal model, host-language assumptions, performance expectations, and conformance tests.

Use predicative universe levels first:

Type0 : Type1
Type1 : Type2
...

Type0 : Type1
Type1 : Type2
...

Do not add cumulativity unless it is a deliberate proposal:

Type0 <= Type1

Type0 <= Type1

Cumulativity improves ergonomics but adds constraints and diagnostic complexity. Strict universe equality is easier for the first implementation.

Represent inductive families as declarations:

Inductive Vec(A: Type0, n: Nat): Type0
  Nil  : Vec(A, Z)
  Cons : (k: Nat) -> A -> Vec(A, k) -> Vec(A, S(k))

Inductive Vec(A: Type0, n: Nat): Type0
  Nil  : Vec(A, Z)
  Cons : (k: Nat) -> A -> Vec(A, k) -> Vec(A, S(k))

Constructor checking compares the expected family with the constructor result. For dependent pattern matching, matching a constructor will later refine indices by unifying the scrutinee family with the constructor result.

The first equality type can be intensional:

Eq(A, x, y)

Eq(A, x, y)

Refl(x)Refl(x) checks against Eq(A, x, x)Eq(A, x, x) when both sides are definitionally equal.

Do not silently assume advanced equality principles such as K, UIP, univalence, or quotient equality. If Cosmo later accepts one of those principles, it should be an explicit proposal because it changes the theory and dependent pattern matching rules.

Metavariables are useful for elaboration:

?m : A in context Γ

?m : A in context Γ

The first checker should solve only conservative cases:

• exact known term;
• first-order constructor-shaped constraints;
• simple pattern variables.

Arbitrary higher-order unification should remain unsupported. When a metavariable cannot be solved, report a deterministic postponed or unsolved constraint instead of guessing.

Effects and traits are not part of the first MLTT conversion relation.

Later profiles can add:

Γ |- effects(body) <= declared effects
Γ |- T implements Trait
Γ |- object-safe(Trait, ABI)

Γ |- effects(body) <= declared effects
Γ |- T implements Trait
Γ |- object-safe(Trait, ABI)

Those checks should produce obligations around the core checker. They should not turn definitional equality into trait search or effect execution.

Dependent pattern matching should elaborate into core case trees or eliminators. When matching:

xs : Vec(A, S(n))

xs : Vec(A, S(n))

against NilNil, the checker tries to unify:

Vec(A, S(n)) == Vec(A, Z)

Vec(A, S(n)) == Vec(A, Z)

which fails because S(n)S(n) and ZZ do not unify. The branch is impossible.

When matching against ConsCons, the branch learns:

xs = Cons(k, head, tail)
tail : Vec(A, k)
S(k) == S(n)

xs = Cons(k, head, tail)
tail : Vec(A, k)
S(k) == S(n)

and the expected result type is specialized under those refinements.

This is why dependent pattern matching should be implemented as an elaborator over MLTT core metadata, not as ad hoc expression typing.

Suggested modules:

types/mltt/core.cos          term, type, binder, declaration data
types/mltt/context.cos       local context and lookup
types/mltt/diagnostic.cos    profile-aware diagnostics
types/mltt/normalize.cos     first-stage normalization strategy
types/mltt/convert.cos       definitional equality
types/mltt/check.cos         bidirectional check/infer
types/mltt/fixture.cos       small Nat/Vec examples

types/mltt/core.cos          term, type, binder, declaration data
types/mltt/context.cos       local context and lookup
types/mltt/diagnostic.cos    profile-aware diagnostics
types/mltt/normalize.cos     first-stage normalization strategy
types/mltt/convert.cos       definitional equality
types/mltt/check.cos         bidirectional check/infer
types/mltt/fixture.cos       small Nat/Vec examples

Keep functions small and explicit. Prefer helper functions for repeated diagnostic and context-extension logic. The checker should read top to bottom: infer a shape, validate it, emit obligations, return a typed artifact.

Start with:

• Type0 : Type1Type0 : Type1;
• identity function checks against (A: Type0) -> A -> A(A: Type0) -> A -> A;
• application of identity infers the argument type;
• pair checks against a Sigma type;
• Refl(x)Refl(x) checks against Eq(A, x, x)Eq(A, x, x);
• mismatch between Type0Type0 and a non-universe reports a diagnostic;
• effectful source is rejected by mltt.coremltt.core;
• trait source is rejected by mltt.coremltt.core.

After that, add Nat and Vec fixtures before dependent pattern matching.