Skip to content

Semantic kind interpretation and substitution

9 fully proved

Semantic interpretation of kinds

DefinitionSemantic interpretation of kinds#✓fully proved

Interpret kinds over a carrier for term types.

def Kind.Sem (α : Type u) : Kind → Type u
  | .star => α
  | .arrow κ μ => Kind.Sem α κ → Kind.Sem α μ
Uses 1 · Used by 25
Statement usesKinds of pure Fω
Used byRelational interpretation of Fω types · Type-beta conversion preserves the relational interpretation · Relational interpretation of an Fω universal type · Relational interpretation of an instantiated Fω type · Relational interpretation of a renamed Fω type · Relational interpretation of a substituted Fω type · Relational interpretation of a weakened Fω type · Kind algebra of beta-invariant relations · No closed Fω term inhabits \(\forall X, X\) · Fundamental theorem of higher-kinded parametricity for Fω · Closed inhabitants of the higher-kinded identity type are identities · Higher-kinded identity inhabitants preserve admissible relations · No closed Fω term inhabits \(\forall F, \forall X, F\,X\) · Function types are not convertible to quantified types · Soundness of type-beta conversion in kind algebras · Semantic evaluation of kinded type operators · Evaluation depends only on the environment pointwise · Evaluation of an instantiated type operator · Evaluation of a renamed type operator · Evaluation of a substituted type operator · Extension of a kinded semantic environment · Kinded semantic environment · Kind algebra of arrow and universal type constructors · Relational interpretation of canonically embedded types · Type translation preserves the relational interpretation

AbbreviationKinded semantic environment#✓fully proved

An environment supplies a value of the declared kind for every variable.

abbrev KEnv (α : Type u) (Δ : List Kind) :=
  ∀ {κ}, KVar Δ κ → Kind.Sem α κ
Uses 3 · Used by 23
Statement usesKinded type variables of Fω · Kinds of pure Fω · Semantic interpretation of kinds
Used byRelational interpretation of Fω types · Type-beta conversion preserves the relational interpretation · Relational interpretation of an Fω universal type · Relational interpretation of an Fω function type · Relational interpretation of an instantiated Fω type · Relational interpretation of a renamed Fω type · Relational interpretation of a substituted Fω type · Relational interpretation of a weakened Fω type · No closed Fω term inhabits \(\forall X, X\) · Fundamental theorem of higher-kinded parametricity for Fω · Closed typed Fω terms are related to themselves · Closed inhabitants of the higher-kinded identity type are identities · Higher-kinded identity inhabitants preserve admissible relations · No closed Fω term inhabits \(\forall F, \forall X, F\,X\) · Soundness of type-beta conversion in kind algebras · Semantic evaluation of kinded type operators · Evaluation depends only on the environment pointwise · Evaluation of an instantiated type operator · Evaluation of a renamed type operator · Evaluation of a substituted type operator · Extension of a kinded semantic environment · Relational interpretation of canonically embedded types · Type translation preserves the relational interpretation

DefinitionExtension of a kinded semantic environment#✓fully proved

Extend a semantic environment at its newest kinded variable.

def KEnv.extend {α : Type u} {Δ : List Kind} {κ : Kind}
    (ρ : KEnv α Δ) (a : Kind.Sem α κ) : KEnv α (κ :: Δ)
  | _, .zero => a
  | _, .succ x => ρ x
Uses 4 · Used by 11
Statement usesKinded semantic environment · Kinded type variables of Fω · Kinds of pure Fω · Semantic interpretation of kinds
Used byRelational interpretation of an Fω universal type · Relational interpretation of an instantiated Fω type · Relational interpretation of a weakened Fω type · Fundamental theorem of higher-kinded parametricity for Fω · Closed inhabitants of the higher-kinded identity type are identities · Soundness of type-beta conversion in kind algebras · Semantic evaluation of kinded type operators · Evaluation of an instantiated type operator · Evaluation of a renamed type operator · Evaluation of a substituted type operator · Type translation preserves the relational interpretation

StructureKind algebra of arrow and universal type constructors#✓fully proved

The two type constructors at star; higher kinds need no extra laws.

structure KindAlgebra (α : Type u) where
  arr : α → α → α
  all : {κ : Kind} → (Kind.Sem α κ → α) → α
Uses 2 · Used by 8
Statement usesKinds of pure Fω · Semantic interpretation of kinds
Used byKind algebra of beta-invariant relations · Function types are not convertible to quantified types · Soundness of type-beta conversion in kind algebras · Semantic evaluation of kinded type operators · Evaluation depends only on the environment pointwise · Evaluation of an instantiated type operator · Evaluation of a renamed type operator · Evaluation of a substituted type operator

Evaluation of type operators

DefinitionSemantic evaluation of kinded type operators#✓fully proved

Interpret a kinded operator by ordinary function abstraction/application.

def eval (M : KindAlgebra α) : {Δ : List Kind} → KEnv α Δ →
    {κ : Kind} → Ty Δ κ → Kind.Sem α κ
  | _, ρ, _, .var x => ρ x
  | _, ρ, _, .lam b => fun a => eval M (KEnv.extend ρ a) b
  | _, ρ, _, .app f a => eval M ρ f (eval M ρ a)
  | _, ρ, _, .arr a b => M.arr (eval M ρ a) (eval M ρ b)
  | _, ρ, _, .all b => M.all (fun a => eval M (KEnv.extend ρ a) b)
Uses 7 · Used by 9
Statement usesKinded semantic environment · Extension of a kinded semantic environment · Kinded type variables of Fω · Kinds of pure Fω · Semantic interpretation of kinds · Kind algebra of arrow and universal type constructors · Intrinsically kinded Fω type operators
Used byRelational interpretation of Fω types · Fundamental theorem of higher-kinded parametricity for Fω · Closed inhabitants of the higher-kinded identity type are identities · Function types are not convertible to quantified types · Soundness of type-beta conversion in kind algebras · Evaluation depends only on the environment pointwise · Evaluation of an instantiated type operator · Evaluation of a renamed type operator · Evaluation of a substituted type operator

TheoremEvaluation depends only on the environment pointwise#✓fully proved

Interpretation depends only on the pointwise kinded environment.

theorem eval_congr (M : KindAlgebra α) {ρ τ : KEnv α Δ}
    (h : ∀ {ν} (x : KVar Δ ν), ρ x = τ x) (t : Ty Δ κ) :
    eval M ρ t = eval M τ t
Uses 7 · Used by 3
Statement usesKinded semantic environment · Kinded type variables of Fω · Kinds of pure Fω · Semantic interpretation of kinds · Kind algebra of arrow and universal type constructors · Intrinsically kinded Fω type operators · Semantic evaluation of kinded type operators
Used byEvaluation of an instantiated type operator · Evaluation of a renamed type operator · Evaluation of a substituted type operator

TheoremEvaluation of a renamed type operator#✓fully proved

Semantic renaming is precomposition of the kinded environment.

theorem eval_rename (M : KindAlgebra α) (η : KEnv α Ε)
    (ρ : KRen Δ Ε) (t : Ty Δ κ) :
    eval M η (rename ρ t) = eval M (fun {_} x => η (ρ x)) t
Uses 12 · Used by 2
Statement usesKinded semantic environment · Kind-preserving renamings of type variables · Kinded type variables of Fω · Kinds of pure Fω · Semantic interpretation of kinds · Kind algebra of arrow and universal type constructors · Intrinsically kinded Fω type operators · Semantic evaluation of kinded type operators · Renaming of Fω type operators
Proof usesExtension of a kinded semantic environment · Lifting a renaming under a type binder · Evaluation depends only on the environment pointwise
Used byRelational interpretation of a renamed Fω type · Evaluation of a substituted type operator

TheoremEvaluation of a substituted type operator#✓fully proved

Semantic simultaneous substitution at every kind, including higher kinds.

theorem eval_subst (M : KindAlgebra α) (η : KEnv α Ε)
    (σ : Sub Δ Ε) (t : Ty Δ κ) :
    eval M η (subst σ t) =
      eval M (fun {_} x => eval M η (σ x)) t
Uses 13 · Used by 2
Statement usesKinded semantic environment · Kinded type variables of Fω · Kinds of pure Fω · Semantic interpretation of kinds · Kind algebra of arrow and universal type constructors · Intrinsically kinded Fω type operators · Kind-preserving simultaneous type substitutions · Semantic evaluation of kinded type operators · Simultaneous substitution of Fω type operators
Proof usesExtension of a kinded semantic environment · Evaluation depends only on the environment pointwise · Evaluation of a renamed type operator · Lifting a type substitution under a type binder
Used byRelational interpretation of a substituted Fω type · Evaluation of an instantiated type operator

TheoremEvaluation of an instantiated type operator#✓fully proved

Semantic instantiation is environment extension by the argument value.

theorem eval_instantiate (M : KindAlgebra α) (η : KEnv α Δ)
    (b : Ty (μ :: Δ) κ) (a : Ty Δ μ) :
    eval M η (instantiate b a) =
      eval M (KEnv.extend η (eval M η a)) b
Uses 13 · Used by 2
Statement usesKinded semantic environment · Extension of a kinded semantic environment · Kinds of pure Fω · Semantic interpretation of kinds · Kind algebra of arrow and universal type constructors · Intrinsically kinded Fω type operators · Semantic evaluation of kinded type operators · Instantiation of an Fω type binder
Proof usesKinded type variables of Fω · Evaluation depends only on the environment pointwise · Evaluation of a substituted type operator · Substitution for the newest type variable · Simultaneous substitution of Fω type operators
Used byRelational interpretation of an instantiated Fω type · Soundness of type-beta conversion in kind algebras

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.