MLTT Problem Ladder

This page is a source-tagged problem ladder for the experimental mltt.coremltt.core checker. It is a collection of implementation exercises and fixture candidates, not a normative Cosmo language specification. Each entry uses one of these statuses:

• supported-nowsupported-now: the current mltt.coremltt.core checker should have an executable fixture or Scala mirror test.
• source-backed-futuresource-backed-future: the problem is backed by external dependent-type implementation material, but the current checker deliberately does not support it yet.
• paper-exercisepaper-exercise: the problem is useful as a derivation or design exercise, but it is not yet a compiler fixture.

• elaboration-zooelaboration-zoo: Andras Kovacs, elaboration-zoo. This is a sequence of small dependent type checking and elaboration implementations. It is the main source for evaluation representations, bidirectional checking, holes, implicit arguments, pruning, and first-class polymorphism.
• nbe-tutorialnbe-tutorial: David Christiansen, Checking Dependent Types with Normalization by Evaluation. This is the main source for conversion, normalization, equality checking, holes, and project-style extensions such as vectors.
• cmu-dependency-notescmu-dependency-notes: CMU ATPL dependency notes. These notes are the source for Pi, Sigma, identity type rules, and eta-style exercises.
• agda-implicit-argsagda-implicit-args: Agda reference manual, Finding the Values of Implicit Arguments. This is a practical source for implicit argument metavariables and restricted pattern unification.
• lean-elaborationlean-elaboration: Lean 4 Metaprogramming Book, elaboration overview. This is a practical source for surface holes becoming metavariables during elaboration.
• practical-unificationpractical-unification: Practical Unification for Dependent Type Checking. This is the source for the boundary around higher-order unification and practical restrictions.
• pi-forallpi-forall: pi-forall paper and pi-forall repository. These are sources for small dependently typed language implementation exercises beyond the current checker.
• radboud-exercisesradboud-exercises: Radboud Type Theory Exercises 6. This is a source for proof-term and derivation exercises.

problem: mltt-core-displaymltt-core-display status: supported-nowsupported-now sources: elaboration-zooelaboration-zoo, nbe-tutorialnbe-tutorial

Exercise: build the same small core term set using explicit constructors and prove that display is deterministic for universes, Pi, Sigma, equality, Nat, and Vec. This is the smallest check that the implementation has a stable core syntax before type checking is involved.

problem: mltt-universe-variablemltt-universe-variable status: supported-nowsupported-now sources: elaboration-zooelaboration-zoo, cmu-dependency-notescmu-dependency-notes

Exercise: infer Type0 : Type1Type0 : Type1 and infer a variable from the local context. The context lookup case must report the mltt.coremltt.core profile on unknown variables.

problem: mltt-pi-lambda-applicationmltt-pi-lambda-application status: supported-nowsupported-now sources: elaboration-zooelaboration-zoo, cmu-dependency-notescmu-dependency-notes

Exercise: check an identity lambda against a Pi type and infer an application through the Pi codomain substitution. Lambdas should use check mode when an expected Pi is available; applications should infer the function type and then check the argument.

problem: mltt-sigma-reflmltt-sigma-refl status: supported-nowsupported-now sources: cmu-dependency-notescmu-dependency-notes, nbe-tutorialnbe-tutorial

Exercise: check a pair against a Sigma type and check Refl(x)Refl(x) against Eq(A, x, x)Eq(A, x, x). The equality case should use conversion, not raw syntax, for the two endpoints.

problem: mltt-projection-whnfmltt-projection-whnf status: supported-nowsupported-now sources: nbe-tutorialnbe-tutorial, cmu-dependency-notescmu-dependency-notes

Exercise: reduce fst((x, y))fst((x, y)) to xx and snd((x, y))snd((x, y)) to yy during WHNF conversion. This keeps dependent pair projections in the conversion relation without requiring a full normalizer.

problem: mltt-conversion-beta-let-defmltt-conversion-beta-let-def status: supported-nowsupported-now sources: nbe-tutorialnbe-tutorial, elaboration-zooelaboration-zoo

Exercise: accept beta conversion, transparent let conversion, and transparent pure definition unfolding, such as an add(Z, n)add(Z, n)-style fixture reducing to nn.

problem: mltt-conversion-effect-boundarymltt-conversion-effect-boundary status: supported-nowsupported-now sources: nbe-tutorialnbe-tutorial

Exercise: reject conversion through opaque or effectful definitions, and reject unknown normalization strategy names. This preserves the design rule that definitional equality is pure, deterministic type-level computation.

problem: mltt-nat-vec-constructorsmltt-nat-vec-constructors status: supported-nowsupported-now sources: nbe-tutorialnbe-tutorial, agda-implicit-argsagda-implicit-args

Exercise: record Nat and Vec declaration metadata, check ZZ and S(Z)S(Z) against Nat, check NilNil against Vec(A, Z)Vec(A, Z), and check Cons(k, head, tail)Cons(k, head, tail) against Vec(A, S(k))Vec(A, S(k)). This is constructor-signature checking only; impossible branch analysis belongs to dependent pattern elaboration.

problem: mltt-meta-exact-higher-order-rejectmltt-meta-exact-higher-order-reject status: supported-nowsupported-now sources: elaboration-zooelaboration-zoo, agda-implicit-argsagda-implicit-args, practical-unificationpractical-unification

Exercise: create a local metavariable with a context snapshot, solve it exactly when a known term is supplied, and reject arbitrary higher-order unification with a deterministic diagnostic.

problem: mltt-surface-holesmltt-surface-holes status: source-backed-futuresource-backed-future sources: elaboration-zooelaboration-zoo, lean-elaborationlean-elaboration, nbe-tutorialnbe-tutorial

Exercise: elaborate a surface __ hole into a metavariable that records the current context and expected type. The current checker has core metavariable records, but no surface elaborator that creates them from syntax.

problem: mltt-implicit-argumentsmltt-implicit-arguments status: source-backed-futuresource-backed-future sources: elaboration-zooelaboration-zoo, agda-implicit-argsagda-implicit-args, lean-elaborationlean-elaboration

Exercise: insert implicit argument metavariables while elaborating a function call, then solve them from explicit arguments or the expected result type. The current core has no explicit/implicit Pi distinction.

problem: mltt-pruning-pattern-unificationmltt-pruning-pattern-unification status: source-backed-futuresource-backed-future sources: elaboration-zooelaboration-zoo, agda-implicit-argsagda-implicit-args, practical-unificationpractical-unification

Exercise: solve only restricted pattern constraints, prune unused metavariable dependencies, and postpone or reject non-pattern constraints. The current checker only exposes conservative exact solving and a higher-order rejection diagnostic.

problem: mltt-first-class-polymorphismmltt-first-class-polymorphism status: source-backed-futuresource-backed-future sources: elaboration-zooelaboration-zoo, pi-forallpi-forall

Exercise: pass polymorphic values through the core while preserving explicit and implicit function boundaries. This is outside the current mltt.coremltt.core term language.

problem: mltt-dependent-pattern-impossible-branchmltt-dependent-pattern-impossible-branch status: source-backed-futuresource-backed-future sources: nbe-tutorialnbe-tutorial, agda-implicit-argsagda-implicit-args

Exercise: elaborate a match on xs : Vec(A, S(n))xs : Vec(A, S(n)) and mark the NilNil branch as impossible by unifying Vec(A, S(n))Vec(A, S(n)) with the constructor result Vec(A, Z)Vec(A, Z). This belongs to the dependent-pattern checker profile, not the first core checker.

problem: mltt-identity-eliminator-jmltt-identity-eliminator-j status: source-backed-futuresource-backed-future sources: cmu-dependency-notescmu-dependency-notes

Exercise: add the identity eliminator J and its beta rule while keeping the theory intensional unless a later proposal explicitly accepts additional equality principles.

problem: mltt-eta-cumulativitymltt-eta-cumulativity status: source-backed-futuresource-backed-future sources: cmu-dependency-notescmu-dependency-notes, nbe-tutorialnbe-tutorial

Exercise: evaluate whether Pi/Sigma eta rules or universe cumulativity should be part of a later profile. The current checker keeps strict universe levels and does not add eta conversion.

problem: mltt-logic-proof-term-derivationsmltt-logic-proof-term-derivations status: paper-exercisepaper-exercise sources: radboud-exercisesradboud-exercises, cmu-dependency-notescmu-dependency-notes

Exercise: derive a proof term and context typing derivation for a small predicate-logic encoding. This is useful reviewer training for dependent judgments, but it should not become a compiler fixture until Cosmo has a surface syntax for those proof terms.