Annotated typing under annotation rewriting, and its bridge to HasType

Key theorems: LExpr.HasTypeA_replaceUserProvidedType_map (rewriting annotations by φ maps an annotated typing by φ), OpsConsistentR.of_opAnnots with its _body and _resolveTy forms (operator annotations that instantiate their signatures give OpsConsistentR), and HasType_of_HasTypeA_of_annots (annotated typing whose free-variable annotations the context holds gives HasType).

theorem Lambda.LExpr.HasTypeA_replaceUserProvidedType_map {T : LExprParams} (φ : LMonoTy → LMonoTy) (hφ_arrow : ∀ (a b : LMonoTy), φ (a.arrow b) = (φ a).arrow (φ b)) (hφ_bool : φ LMonoTy.bool = LMonoTy.bool) (hφ_const : ∀ (c : LConst), φ c.ty = c.ty) (Δ : List LMonoTy) (e : LExpr T.mono) (τ : LMonoTy) (h : HasTypeA Δ e τ) : HasTypeA (List.map φ Δ) (e.replaceUserProvidedType φ) (φ τ)

Rewriting annotations by φ maps an annotated typing's context and type by φ, when φ preserves arrows, bool, and literal types.

OpsConsistentR from operator annotations

theorem Lambda.OpsConsistentR.of_opAnnots {T : LExprParams} {F : Factory T} {e : LExpr T.mono} (hann : e.fullyAnnotated = true) (h : ∀ (o : Identifier T.mono.base.IDMeta) (ty : T.mono.TypeType), (o, ty) ∈ e.opAnnots → ∃ (fn : LFunc T), ∃ (τ : Subst), F[o.name]? = some fn ∧ ty = LMonoTy.subst τ (fn.output.mkArrow' (List.map Prod.snd fn.inputs))) : OpsConsistentR F e

A fully annotated expression satisfies OpsConsistentR F when every operator annotation is an instance of the signature of the function that F stores under the operator's name.

theorem Lambda.OpsConsistentR.of_opAnnots_body {T : LExprParams} [DecidableEq T.IDMeta] {ks : KnownTypes} {F : Factory T} {e : LExpr T.mono} (hsig : FactorySigsKnown ks F) (hann : e.fullyAnnotated = true) (h : ∀ (o : Identifier T.mono.base.IDMeta) (ty : T.mono.TypeType), (o, ty) ∈ e.opAnnots → ∃ (f : LFunc T), ∃ (xs : List TyIdentifier), ∃ (body : LMonoTy), F[o.name]? = some f ∧ f.type = Except.ok (LTy.forAll xs body) ∧ ∃ (τ : Subst), ty = LMonoTy.subst τ body) : OpsConsistentR F e

A fully annotated expression satisfies OpsConsistentR F when every operator annotation is an instance of the body of its function's type scheme and every signature type is registered.

theorem Lambda.OpsConsistentR.of_opAnnots_resolveTy {T : LExprParams} [DecidableEq T.IDMeta] [Hashable T.IDMeta] [Std.ToFormat T.IDMeta] {ks : KnownTypes} {F : Factory T} {Γ : TContext T.IDMeta} {e : LExpr T.mono} (hsig : FactorySigsKnown ks F) (hfresh : ∀ (al : TypeAlias), al ∈ Γ.aliases → ks.containsName al.name = false) (hann : e.fullyAnnotated = true) (h : ∀ (o : Identifier T.mono.base.IDMeta) (ty : T.mono.TypeType), (o, ty) ∈ e.opAnnots → ∃ (f : LFunc T), ∃ (xs : List TyIdentifier), ∃ (body : LMonoTy), F[o.name]? = some f ∧ f.type = Except.ok (LTy.forAll xs body) ∧ ∃ (τ : Subst), ty = LMonoTy.subst τ (Γ.resolveTy body)) : OpsConsistentR F e

A fully annotated expression satisfies OpsConsistentR F when every operator annotation is an instance of its function's type-scheme body with Γ's aliases resolved, and no alias of Γ is named in ks.

From annotated typing to polymorphic typing

HasTypeA checks annotations internally, while HasType also consults the ambient context and factory. The bridge below derives the second from the first when the free-variable and operator annotations agree with those environments.

Typing an operator occurrence

The bridge's conditions on subexpressions

The bridge theorem

theorem Lambda.HasType_of_HasTypeA_of_annots {T : LExprParams} [DecidableEq T.IDMeta] [Hashable T.IDMeta] [Inhabited T.IDMeta] {C : LContext T} {Γ : TContext T.IDMeta} {e : LExpr T.mono} {τ : LMonoTy} (hA : LExpr.HasTypeA [] e τ) (hctx : ∀ (y : Identifier T.IDMeta) (ann : LMonoTy), (y, some ann) ∈ e.freeVars → Γ.types.find? y = some (LTy.forAll [] ann)) (hop : OpsConsistentR C.functions e) (hdecl : ∀ (o : Identifier T.mono.base.IDMeta), o ∈ e.getOps → ∃ (f : LFunc T), ∃ (ty : LTy), C.functions[o.name]? = some f ∧ f.type = Except.ok ty) (hconst : ∀ (c : LConst), c ∈ e.getConsts → C.knownTypes.containsName c.tyName = true) (hsigwf : FactorySigWF C.functions) (hsig : FactorySigsKnown C.knownTypes C.functions) (hbind : ∀ (t : T.mono.TypeType), t ∈ e.binderAnnotations → LMonoTy.knownInstance t C.knownTypes = true) (hfresh : ∀ (al : TypeAlias), al ∈ Γ.aliases → C.knownTypes.containsName al.name = false) : LExpr.HasType C Γ e (LTy.forAll [] τ)

Annotated typing gives polymorphic typing. If e has annotated typing τ, its operator annotations instantiate the factory signatures, and Γ holds every annotated free variable of e at its annotation as a monotype, then e has the monotype τ in Γ. The other hypotheses say that every operator names a factory function that reports a type, that the factory's signatures are well formed and registered, that every constant's type and binder annotation is registered, and that no alias of Γ is named like a registered type.