inductive CurryType : Type

• phi : Char → CurryType
• arrow : CurryType → CurryType → CurryType

def instReprCurryType.repr : CurryType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance instReprCurryType : Repr CurryType

Equations

• instReprCurryType = { reprPrec := instReprCurryType.repr }

instance instBEqCurryType : BEq CurryType

Equations

• instBEqCurryType = { beq := instBEqCurryType.beq }

def instBEqCurryType.beq : CurryType → CurryType → Bool

Equations

• instBEqCurryType.beq (CurryType.phi a) (CurryType.phi b) = (a == b)
• instBEqCurryType.beq (a.arrow a_1) (b.arrow b_1) = (instBEqCurryType.beq a b && instBEqCurryType.beq a_1 b_1)
• instBEqCurryType.beq x✝¹ x✝ = false

instance instDecidableEqCurryType : DecidableEq CurryType

Equations

• instDecidableEqCurryType = instDecidableEqCurryType.decEq

def instDecidableEqCurryType.decEq (x✝ x✝¹ : CurryType) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• instDecidableEqCurryType.decEq (CurryType.phi a) (CurryType.phi b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqCurryType.decEq (CurryType.phi a) (a_1.arrow a_2) = isFalse ⋯
• instDecidableEqCurryType.decEq (a.arrow a_1) (CurryType.phi a_2) = isFalse ⋯

instance instReflBEqCurryType : ReflBEq CurryType

instance instLawfulBEqCurryType : LawfulBEq CurryType

inductive Term : Type

• var : Char → Term
• abs : Char → Term → Term
• app : Term → Term → Term

instance instReprTerm : Repr Term

Equations

• instReprTerm = { reprPrec := instReprTerm.repr }

def instReprTerm.repr : Term → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprTerm.repr (Term.var a) prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Term.var" ++ Std.Format.line ++ reprArg a)).group prec✝

structure TypeCtx : Type

• env : List (Char × CurryType)
• label : Char

instance instReprTypeCtx : Repr TypeCtx

Equations

• instReprTypeCtx = { reprPrec := instReprTypeCtx.repr }

def instReprTypeCtx.repr : TypeCtx → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def emptyEnv : TypeCtx

Equations

• emptyEnv = { env := [], label := 'A' }

def union (ctx1 ctx2 : TypeCtx) : TypeCtx

Equations

• union ctx1 ctx2 = { env := ctx1.env ++ ctx2.env, label := if ctx1.label > ctx2.label then ctx1.label else ctx2.label }

def next (ctx : TypeCtx) : CurryType × TypeCtx

Equations

• next ctx = (CurryType.phi (Char.ofNat (ctx.label.toNat + 1)), { env := ctx.env, label := Char.ofNat (ctx.label.toNat + 1) })

def add (c : Char) (ty : CurryType) (ctx : TypeCtx) : TypeCtx

Equations

• add c ty ctx = { env := (c, ty) :: ctx.env, label := ctx.label }

def applySubst (f : CurryType → CurryType) (ctx : TypeCtx) : TypeCtx

Equations

• applySubst f ctx = { env := List.map (fun (x : Char × CurryType) => match x with | (c, ty) => (c, f ty)) ctx.env, label := ctx.label }

structure PrincipalPair : Type

• ctx : TypeCtx
• ty : CurryType

def instReprPrincipalPair.repr : PrincipalPair → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance instReprPrincipalPair : Repr PrincipalPair

Equations

• instReprPrincipalPair = { reprPrec := instReprPrincipalPair.repr }

partial def curryTypeToString : CurryType → String

instance instToStringCurryType : ToString CurryType

Equations

• instToStringCurryType = { toString := curryTypeToString }

partial def termToString : Term → String

instance instToStringTerm : ToString Term

Equations

• instToStringTerm = { toString := termToString }

instance instToStringPrincipalPair : ToString PrincipalPair

Equations

• One or more equations did not get rendered due to their size.

instance instToStringOption_sTLCLean {α : Type u_1} [ToString α] : ToString (Option α)

Equations

• instToStringOption_sTLCLean = { toString := fun (x : Option α) => match x with | some x => toString x | none => "Type Error" }

def occursIn (p : Char) : CurryType → Bool

Check whether type variable p occurs (free) in type τ. Used in the occurs-check of unify to prevent circular substitutions.

Equations

• occursIn p (CurryType.phi a) = (p == a)
• occursIn p (a.arrow a_1) = (occursIn p a || occursIn p a_1)

def replaceVar (x : Char) (ty : CurryType) : CurryType → CurryType

Substitute type variable x with type ty throughout the given type. The caller must ensure the occurs-check holds (i.e., ¬occursIn x ty) to prevent introducing a cyclic type.

Equations

• replaceVar x ty (CurryType.phi a) = if (a == x) = true then ty else CurryType.phi a
• replaceVar x ty (a.arrow a_1) = (replaceVar x ty a).arrow (replaceVar x ty a_1)

def vars : CurryType → Finset Char

Compute the set of free type variables in a CurryType. Used as the primary component of the lexicographic termination measure for unify: cardinality of vars left ∪ vars right must decrease (or stay equal with size decreasing) across recursive calls.

Equations

• vars (CurryType.phi a) = {a}
• vars (a.arrow a_1) = vars a ∪ vars a_1

def size : CurryType → ℕ

Compute the structural size (number of syntax-tree nodes) of a CurryType. Used as the secondary component of the termination measure for unify: when the variable-cardinality component stays equal, size must strictly decrease.

Equations

• size (CurryType.phi a) = 1
• size (a.arrow a_1) = 1 + size a + size a_1

theorem SizeGtZ (ty : CurryType) : size ty > 0

Every CurryType has strictly positive size. Used as a termination witness for unify.

theorem VarsArrow (ty ty' : CurryType) : vars ty ⊆ vars (ty.arrow ty')

The free type variables of any type are a subset of the free variables of any arrow type built from it. Used as a termination witness for unify.

structure Subst (left right : CurryType) : Type

A type substitution witnessing that left and right can be unified. Carries apply : CurryType → CurryType together with three invariants used to prove termination of unify:

• vars_decreased: the free variables of any image are bounded by those of left, right, and the input type's own variables.
• vars_eq_then_id: if the variable-cardinality does not decrease, apply is the identity.
• subst_rec: apply distributes over arrow types.

• apply : CurryType → CurryType
• vars_decreased (ty : CurryType) : vars (self.apply ty) ⊆ vars left ∪ vars right ∪ vars ty
• vars_eq_then_id (ty : CurryType) : (vars (self.apply ty)).card = (vars left ∪ vars right ∪ vars ty).card → self.apply = _root_.id
• subst_rec (a b : CurryType) : self.apply (a.arrow b) = (self.apply a).arrow (self.apply b)
• uleft : CurryType
• uright : CurryType

def Subst.id (left right : CurryType) : Subst left right

The identity substitution. apply is id, so all invariants hold trivially.

Equations

• Subst.id left right = { apply := id, vars_decreased := ⋯, vars_eq_then_id := ⋯, subst_rec := Subst.id._proof_3, uleft := left, uright := right }

theorem ReplaceVarScope (a : Char) (ty ty1 : CurryType) : vars (replaceVar a ty ty1) ⊆ vars (CurryType.phi a) ∪ vars ty ∪ vars ty1

Substituting ty for a in any type ty1 can only introduce variables already present in ty (where a was replaced). All free variables of the result lie within vars (.phi a) ∪ vars ty ∪ vars ty1.

theorem OccursInIffInVars {c : Char} {τ : CurryType} : c ∈ vars τ → occursIn c τ = true

Membership in vars implies occursIn: if c ∈ vars τ then occursIn c τ = true. Connects the Finset-based and Bool-based representations of free-variable occurrence.

theorem ReplaceElim (a : Char) (ty : CurryType) (ho : ¬occursIn a ty = true) (t : CurryType) : a ∉ vars (replaceVar a ty t)

After substituting ty for a, the variable a no longer appears in the result. The occurs-check condition ¬occursIn a ty prevents a from being reintroduced via ty.

theorem ReplaceAddsNewVars (a : Char) (ty : CurryType) (ho : ¬occursIn a ty = true) (ty' : CurryType) : ¬(vars (replaceVar a ty ty')).card = (vars (CurryType.phi a) ∪ vars ty ∪ vars ty').card

The variable count can never stay equal after a replaceVar substitution. Formally, (vars (replaceVar a ty ty')).card ≠ (vars (.phi a) ∪ vars ty ∪ vars ty').card. This is used to show that Subst.replace satisfies vars_eq_then_id by contradiction: if cardinalities were equal, subset equality would follow (by ReplaceVarScope), but a is in the RHS (vars (.phi a)) and absent from the LHS (ReplaceElim).

def Subst.replace (a : Char) (ty : CurryType) (ho : ¬occursIn a ty = true) : Subst (CurryType.phi a) ty

Substitution that replaces type variable a with ty everywhere, given the occurs-check ¬occursIn a ty.

Equations

• Subst.replace a ty ho = { apply := replaceVar a ty, vars_decreased := ⋯, vars_eq_then_id := ⋯, subst_rec := ⋯, uleft := CurryType.phi a, uright := ty }

def Subst.replacer (a : Char) (ty : CurryType) (ho : ¬occursIn a ty = true) : Subst ty (CurryType.phi a)

Like Subst.replace but with the Subst type indices swapped (Subst ty (.phi a) instead of Subst (.phi a) ty). The underlying function is the same (replaceVar a ty); invariants delegate to ReplaceVarScope and ReplaceAddsNewVars.

Equations

• Subst.replacer a ty ho = { apply := replaceVar a ty, vars_decreased := ⋯, vars_eq_then_id := ⋯, subst_rec := ⋯, uleft := CurryType.phi a, uright := ty }

def Subst.comp {a c b d : CurryType} (s1 : Subst a c) (s2 : Subst (s1.apply b) (s1.apply d)) : Subst (a.arrow b) (c.arrow d)

Composition of two substitutions. Given s1 : Subst a c and s2 : Subst (s1.apply b) (s1.apply d), their composition s2 ∘ s1 is a Subst (.arrow a b) (.arrow c d).

• vars_decreased: chain the two subset inclusions via calc.
• vars_eq_then_id: if the composition is variable-count-preserving, derive that s2 = id (by cardinality squeeze on s2's image), then that s1 = id similarly.
• subst_rec: each factor distributes over arrows; compose the two equations.

Equations

• s1.comp s2 = { apply := s2.apply ∘ s1.apply, vars_decreased := ⋯, vars_eq_then_id := ⋯, subst_rec := ⋯, uleft := a.arrow b, uright := c.arrow d }

@[irreducible]

def unify (left right : CurryType) : Option (Subst left right)

Unification of two CurryTypes. Returns a Subst left right whose apply unifies the two types, or none if no unifier exists (fails occurs check). Termination measure: ((vars left ∪ vars right).card, size left + size right) lexicographically

• φp = φq: identity if equal, otherwise replace p (φq).
• φp, non-variable: occurs check; if clear, replace p ty.
• arrow cases: unify heads with s1, then unify s1-images of tails with s2; compose.
• non-variable, φp: symmetric to the φp case.

Equations

• unify (CurryType.phi p) (CurryType.phi q) = if ho : p = q then some (Subst.id (CurryType.phi p) (CurryType.phi q)) else some (Subst.replace p (CurryType.phi q) ⋯)
• unify (CurryType.phi p) right = if ho : occursIn p right = true then none else some (Subst.replace p right ⋯)
• unify (a.arrow b) (c.arrow d) = match unify a c with | none => none | some s1 => match unify (s1.apply b) (s1.apply d) with | none => none | some s2 => some (s1.comp s2)
• unify left (CurryType.phi p) = if ho : occursIn p left = true then none else some (Subst.replacer p left ⋯)

structure CtxSubst (ctx1 ctx2 : TypeCtx) : Type

A substitution that simultaneously unifies all common variable bindings of two typing contexts. Unlike Subst, it does not carry termination invariants; it stores the apply function, the list of unified type pairs, and a subst_rec distribution proof.

• apply : CurryType → CurryType
• vars : List (CurryType × CurryType)
• subst_rec (a b : CurryType) : self.apply (a.arrow b) = (self.apply a).arrow (self.apply b)
• uctx1 : TypeCtx
• uctx2 : TypeCtx

def CtxSubst.from (cvars : List (Char × CurryType × CurryType)) (f : CurryType → CurryType) (subst_rec : ∀ (a b : CurryType), f (a.arrow b) = (f a).arrow (f b)) (ctx1 ctx2 : TypeCtx) : CtxSubst ctx1 ctx2

Construct a CtxSubst ctx1 ctx2 from a list of (variable, type1, type2) triples, a substitution function f, a proof that f distributes over arrows, and the two contexts.

Equations

• One or more equations did not get rendered due to their size.

inductive ExSubst : Type

Wrapper that erases the dependent type params of a Subst, allowing substitutions for different type pairs to be stored in a homogeneous list.

• from {a b : CurryType} : Subst a b → ExSubst

def ExSubst.cast (ex : ExSubst) : CurryType → CurryType

Extract the underlying substitution function from an ExSubst.

Equations

• (ExSubst.from s).cast = s.apply

@[irreducible]

def unifyCtx' (commonVars : List (Char × CurryType × CurryType)) : Option (List ExSubst)

Helper function to recursively unify a list of common variables. Crucially, it applies the substitution from unifying the first pair to the rest of the list before continuing the recursion.

Equations

• One or more equations did not get rendered due to their size.
• unifyCtx' [] = some []

def unifyCtx (ctx1 ctx2 : TypeCtx) : Option (CtxSubst ctx1 ctx2)

Unify two typing contexts by unifying the types assigned to their common variables. Collects all variables present in both environments, runs unifyCtx' to recursively unify and accumulate substitutions, and composes the resulting substitutions left-to-right via foldl. Returns none if any individual unification fails.

Equations

• One or more equations did not get rendered due to their size.

def TypeCtx.lookup (ctx : TypeCtx) (c : Char) : Option CurryType

Look up the type assigned to variable c in the typing context.

Equations

• ctx.lookup c = List.lookup c ctx.env

def pp' (ctx : TypeCtx) : Term → Option PrincipalPair

Principal-type algorithm helper. Infers a PrincipalPair for term t given initial context ctx. Fresh type variables are allocated with next; type and context unification use unify / unifyCtx. Returns none only if unification fails (term is untypeable).

• .var c: return the existing type if c is in ctx, else allocate a fresh variable.
• .abs x m: recursively infer for m; if x was assigned a type, wrap as x.ty → m.ty; otherwise allocate a fresh type for x.
• .app m n: infer for m and n sequentially; unify p1 with p2 → a (fresh a); then unify the two resulting contexts and apply the composed substitution.

Equations

• One or more equations did not get rendered due to their size.
• pp' ctx (Term.var a) = match ctx.lookup a with | some ty => some { ctx := ctx, ty := ty } | none => match next ctx with | (a_1, ctx') => some { ctx := add a a_1 ctx', ty := a_1 }

def pp (t : Term) : Option PrincipalPair

Principal-type algorithm. Infers the principal type of t starting from an empty context. Returns some pair where pair.ctx is the minimal typing context and pair.ty the principal type, or none if t is not typeable in the simply-typed lambda calculus.

Equations

• pp t = pp' emptyEnv t

def runTest (name : String) (t : Term) : String

Equations

• runTest name t = toString "[" ++ toString name ++ toString "] " ++ toString t ++ toString ": " ++ toString (pp t)