Abstract
Features
Art & Science
Frank combines the simplicity of Henk and the power of General Inductive Schemes. It constitutes the core of the Christine (Coq) type checker but in Miranda-like syntax.
Correct and Canonical
Unlike Haskell, PureScript and other strongly typed non-consistent languages Frank remains Sound, Complete, Canonical, Total, Consistent, Decidable, and Conservative.
Runtime Extraction
Ready for production code extraction for Erlang/OTP and AtomVM (GRiSP).
Intro
Syntax
type term = | Var of name | Universe of level | Pi of name * term * term | Lam of name * term * term | App of term * term | Inductive of inductive | Constr of int * inductive * term list | Elim of inductive * term * term list * term
Semantics
Syntactic Equality
The function equal implements judgmental equality with substitution to handle bound variables, avoiding explicit α-conversion by assuming fresh names (a simplification over full de Bruijn indices [3]). The recursive descent ensures congruence, but lacks normalization, making it weaker than CIC’s definitional equality, which includes β-reduction.
Terminal Cases: Variables Var x are equal if names match; universes Universe i if levels are identical. Resursive Cases: App (f, arg) requires equality of function and argument. Pi (x, a, b) compares domains and codomains, adjusting for variable renaming via substitution. Inductive d checks name, level, and parameters. Constr and Elim compare indices, definitions, and arguments/cases. Default: Returns false for mismatched constructors.
Theorem 1. Equality is reflexive, symmetric, and transitive modulo α-equivalence (cf. [1], Section 2). For Pi (x, a, b) and Pi (y, a', b'), equality holds if a = a' and b[x := Var x] = b'[y := Var x], ensuring capture-avoiding substitution preserves meaning. ∎
Context Variables Lookup
The function lookup_var retrieves a variable’s type from the context. Context are the objects in the Substitutions categories. Searches ctx for (x, ty) using List.assoc. Returns Some ty if found, None otherwise.
Theorem 2: Context lookup is well-defined under uniqueness of names (cf. [1], Section 3). If ctx = Γ, x : A, Δ, then lookup_var ctx x = Some A. ∎
Substitution Calculus
The function subst substitutes a term s for variable x in term t. Substitutions are morphisms in Substitution categorties.
The capture-avoiding check if x = y prevents variable capture but assumes distinct bound names, a simplification over full renaming or de Bruijn indices. For Elim, substituting in the motive and cases ensures recursive definitions remain sound, aligning with CIC’s eliminator semantics.
Theorem 3 Substition case analysis: 1) Var: Replaces x with s, leaves others unchanged. 2) Pi/Lam: Skips substitution if bound variable shadows x, else recurses on domain and body. 3) App/Constr/Elim: Recurses on subterms. 4) Inductive: No substitution (assumes no free variables). ∎
Inductive Instantiation
The function apply_inductive instantiates an inductive type’s constructors with parameters, used only in infer_Ind.
This function ensures type-level parametricity, critical for polymorphic inductives like List A. The fold-based substitution avoids explicit recursion, leveraging OCaml’s functional style, but assumes args are well-typed, deferring validation to infer. 1) Validates argument count against d.params. 2) Substitutes each parameter into constructor types using subst_param.
Theorem 4: Parameter application preserves inductiveness (cf. [4], Section 4). If D is an inductive type with parameters P, then D[P] is well-formed with substituted constructors. ∎
Context Variables Lookup
The function infer_ctor validates constructor arguments against its type.
This function implements the dependent application rule for constructors, ensuring each argument satisfies the constructor’s domain type in sequence. The recursive descent mirrors the structure of Pi types, where ty is peeled layer by the layer, and subst x arg b updates the type for the next argument. 1) Recursively matches ty (a Pi chain) with args, checking each argument and substituting. 2) Returns the final type when all arguments are consumed.
Theorem 5. Constructor typing is preserved (cf. [1], Section 4, Application Rule; [1], Section 4.3). If ctx ⊢ c : Π (x:A), B and ctx ⊢ a : A, then ctx ⊢ c a : B[x := a]. ∎
Infer General Induction
The function infer_Ind type-checks an dependent elimination (induction principle) over inductive type d.
This function implements the dependent elimination rule of CIC, generalizing both computation (e.g., plus : Nat → Nat → Nat) and proof (e.g., nat_elim : Πx:Nat.Type0). The check equal env ctx t_ty a ensures the motive’s domain aligns with the target, while compute_case_type constructs the induction principle by injecting App (p, var) as the hypothesis type for recursive occurrences, mirroring the fixpoint-style eliminators of CIC [1]. The flexibility in result_ty avoids hardcoding it to D, supporting higher-type motives (e.g., Type0).
Theorem 6. Elimination preserves typing (cf. [1], Section 4.5; Elimination Rule for Inductive Types). For an inductive type D with constructors c_j, if ctx ⊢ t : D and ctx ⊢ P : D → Type_i, and each case case_j has type Πx:A_j.P(c_j x) where A_j are the argument types of c_j (including recursive hypotheses), then ctx ⊢ Ind(D, P, cases, t) : P t. ∎
Type Inference
The function infer infers the type of term t in context ctx and environment env.
For Pi and Lam, universe levels ensure consistency (e.g., Type i : Type (i + 1)), while Elim handles induction, critical for dependent elimination. Note that lambda agrument should be typed for easier type synthesis [13].
Theorem 7. Type inference is sound. ∎
Check Universes
The function check_universe ensures t is a universe, returning its level. Infers type of t, expects Universe i.
This auxiliary enforces universe hierarchy, preventing paradoxes (e.g., Type : Type). It relies on infer, assuming its correctness, and throws errors for non-universe types, aligning with ITT’s stratification.
Theorem 8: Universe checking is decidable (cf. [13]). If ctx ⊢ t : Universe i, then check_universe env ctx t = i. ∎
Check
The function check checks that t has type ty: 1) Lam: Ensures the domain is a type, extends the context, and checks the body against the codomain. 2) Constr: Infers the constructor’s type and matches it to the expected inductive type. 3) Elim: Computes the elimination type via check_elim and verifies it equals ty. 4) Default: Infers t’s type, normalizes ty, and checks equality.
The function leverages bidirectional typing: specific cases (e.g., Lam) check directly, while the default case synthesizes via infer and compares with a normalized ty, ensuring definitional equality (β-reduction). Completeness hinges on normalize terminating (ITT’s strong normalization) and equal capturing judgmental equality.
Theorem 9. Type checking is complete (cf. [1], Normalization). If ctx ⊢ t : T in the type theory, then check env ctx t T succeeds, assuming normalization and sound inference. ∎
Branch Evaluation
The function apply_case applies a case branch to constructor arguments, used only in reduce.
This function realizes CIC’s ι-reduction for inductive eliminators [1], where a case branch is applied to constructor arguments, including recursive hypotheses. For Nat’s succ in plus, ty = Πn:Nat.Nat, case = λk.λih.succ ih, and args = [n]. The recursive check a = Inductive d triggers for n : Nat, computing ih = Elim(Nat, Π_:Nat.Nat, [m; λk.λih.succ ih], n), ensuring succ ih : Nat. The nested apply_term handles multi-argument lambdas (e.g., k and ih), avoiding explicit uncurrying, while substitution preserves typing per CIC’s rules.
Theorem 10. Case application is sound (cf. [1] Elimination Typing). If case : Πx:A.P(c x) and args match A, then apply_case env ctx d p cases case ty args yields a term of type P(c args). ∎
One-step β-reductor
The function reduce performs one-step β-reduction or inductive elimination.
The function implements a one-step reduction strategy combining ITT’s β-reduction with CIC’s ι-reduction for inductives. The App (Lam, arg) case directly applies substitution, while Elim (Constr) uses apply_case to handle induction, ensuring recursive calls preserve typing via the motive p. The Pi case, though unconventional, supports type-level computation, consistent with CIC’s flexibility: 1) App (Lam, arg): Substitutes arg into the lambda body (β-reduction). 2) App (Pi, arg): Substitutes arg into the codomain (type-level β-reduction). 3) App (f, arg): Reduces f, then arg if f is unchanged. 4) Elim (d, p, cases, Constr): Applies the appropriate case to constructor arguments, computing recursive calls (ι-reduction). 5) Elim (d, p, cases, t'): Reduces the target t'. 6) Constr: Reduces arguments. 7) Default: Returns unchanged.
Theorem 11. Reduction preserves typing (cf. [8], Normalization Lemma, Subject Reduction). If ctx ⊢ t : T and t → t' via β-reduction or inductive elimination, then ctx ⊢ t' : T. ∎
Normalization
The function normalize reduces a term t to its normal form by iteratively applying one-step reductions via reduce until no further changes occur, ensuring termination for well-typed terms.
This function implements strong normalization, a cornerstone of MLTT [9] and CIC [1], where all reduction sequences terminate. The fixpoint iteration relies on reduce’s one-step reductions (β for lambdas, ι for inductives), with equal acting as the termination oracle. For plus 2 2, it steps to succ succ succ succ zero, terminating at a constructor form.
Theorem 12. Normalization terminates (cf. [1]. Strong Normalization via CIC). Every well-typed term in the system has a ormal form under β- and ι-reductions. ∎
