Higher-kinded relational interpretation of Fω types

9 fully proved

Relational interpretation of Fω

DefinitionKind algebra of beta-invariant relations#✓fully proved

The generic kind algebra instantiated with the banked relation substrate.

def relationalAlgebra : KindAlgebra SystemF.Rel where
  arr := SystemF.Rel.arrow
  all := fun {_} => SystemF.Rel.universal

Uses 6 · Used by 7

Statement usesKinds of pure Fω · Semantic interpretation of kinds · Kind algebra of arrow and universal type constructors · Beta-invariant binary relations on the term model · Function-space relation of beta-invariant relations · Universal quantification over a family of relations

Used byRelational interpretation of Fω types · Type-beta conversion preserves the relational interpretation · Relational interpretation of an instantiated Fω type · Relational interpretation of a renamed Fω type · Relational interpretation of a substituted Fω type · Fundamental theorem of higher-kinded parametricity for Fω · Closed inhabitants of the higher-kinded identity type are identities

DefinitionRelational interpretation of Fω types#✓fully proved

A kinded type denotes a relation or an appropriately kinded function.

def Ty.interpret {Δ : List Kind} {κ : Kind} (t : Ty Δ κ)
    (ρ : KEnv SystemF.Rel Δ) : Kind.Sem SystemF.Rel κ :=
  t.eval relationalAlgebra ρ

Uses 7 · Used by 12

Statement usesKinded semantic environment · Kinds of pure Fω · Semantic interpretation of kinds · Intrinsically kinded Fω type operators · Semantic evaluation of kinded type operators · Kind algebra of beta-invariant relations · Beta-invariant binary relations on the term model

Used byType-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 · 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 · Relational interpretation of canonically embedded types · Type translation preserves the relational interpretation

Substitution and type-beta conversion

TheoremRelational interpretation of a substituted Fω type#✓fully proved

Relational substitution at every kind, with arbitrary higher-kind values.

theorem interpret_subst (t : Ty Δ κ) (σ : Ty.Sub Δ Ε)
    (ρ : KEnv SystemF.Rel Ε) :
    (t.subst σ).interpret ρ =
      t.interpret (fun {_} x => (σ x).interpret ρ)

Uses 11

Statement usesKinded semantic environment · Kinded type variables of Fω · Kinds of pure Fω · Semantic interpretation of kinds · Intrinsically kinded Fω type operators · Kind-preserving simultaneous type substitutions · Relational interpretation of Fω types · Simultaneous substitution of Fω type operators · Beta-invariant binary relations on the term model

Proof usesEvaluation of a substituted type operator · Kind algebra of beta-invariant relations

TheoremType-beta conversion preserves the relational interpretation#✓fully proved

Proved type-beta conversion is sound for the higher-kinded relations.

theorem Conv.interpret {a b : Ty Δ κ} (h : Conv a b)
    (ρ : KEnv SystemF.Rel Δ) : a.interpret ρ = b.interpret ρ

Uses 9 · Used by 1

Statement usesKinded semantic environment · Kinds of pure Fω · Semantic interpretation of kinds · Intrinsically kinded Fω type operators · Type-beta conversion in Fω · Relational interpretation of Fω types · Beta-invariant binary relations on the term model

Proof usesSoundness of type-beta conversion in kind algebras · Kind algebra of beta-invariant relations

Used byFundamental theorem of higher-kinded parametricity for Fω

TheoremRelational interpretation of a renamed Fω type#✓fully proved

Type renaming transports an arbitrary higher-kinded relation environment.

theorem interpret_rename (t : Ty Δ κ) (η : KRen Δ Ε)
    (ρ : KEnv SystemF.Rel Ε) :
    (t.rename η).interpret ρ = t.interpret (fun {_} x => ρ (η x))

Uses 11 · Used by 1

Statement usesKinded semantic environment · Kind-preserving renamings of type variables · Kinded type variables of Fω · Kinds of pure Fω · Semantic interpretation of kinds · Intrinsically kinded Fω type operators · Relational interpretation of Fω types · Renaming of Fω type operators · Beta-invariant binary relations on the term model

Proof usesEvaluation of a renamed type operator · Kind algebra of beta-invariant relations

Used byRelational interpretation of a weakened Fω type

TheoremRelational interpretation of an instantiated Fω type#✓fully proved

A kinded type argument is interpreted before its universal is discharged.

theorem interpret_instantiate (b : Ty (μ :: Δ) κ) (a : Ty Δ μ)
    (ρ : KEnv SystemF.Rel Δ) :
    (b.instantiate a).interpret ρ =
      b.interpret (KEnv.extend ρ (a.interpret ρ))

Uses 10 · Used by 1

Statement usesKinded semantic environment · Extension of a kinded semantic environment · Kinds of pure Fω · Semantic interpretation of kinds · Intrinsically kinded Fω type operators · Instantiation of an Fω type binder · Relational interpretation of Fω types · Beta-invariant binary relations on the term model

Proof usesEvaluation of an instantiated type operator · Kind algebra of beta-invariant relations

Used byFundamental theorem of higher-kinded parametricity for Fω

TheoremRelational interpretation of an Fω universal type#✓fully proved

A universal quantifies every semantic value of its bound kind.

@[simp] theorem interpret_all {b : Ty (κ :: Δ) .star}
    (ρ : KEnv SystemF.Rel Δ) (f g : SystemF.Model) :
    ((Ty.all b).interpret ρ).holds f g ↔
      ∀ R : Kind.Sem SystemF.Rel κ,
        (b.interpret (KEnv.extend ρ R)).holds f g

Uses 8

Statement usesKinded semantic environment · Extension of a kinded semantic environment · Kinds of pure Fω · Semantic interpretation of kinds · Intrinsically kinded Fω type operators · Relational interpretation of Fω types · Untyped locally closed term model · Beta-invariant binary relations on the term model

TheoremRelational interpretation of an Fω function type#✓fully proved

An arrow relates every related pair of inputs at its codomain.

@[simp] theorem interpret_arr (a b : Ty Δ .star)
    (ρ : KEnv SystemF.Rel Δ) (f g : SystemF.Model) :
    ((Ty.arr a b).interpret ρ).holds f g ↔
      ∀ x y, (a.interpret ρ).holds x y →
        (b.interpret ρ).holds (SystemF.Model.app f x) (SystemF.Model.app g y)

Uses 7

Statement usesKinded semantic environment · Kinds of pure Fω · Intrinsically kinded Fω type operators · Relational interpretation of Fω types · Untyped locally closed term model · Application in the untyped term model · Beta-invariant binary relations on the term model

TheoremRelational interpretation of a weakened Fω type#✓fully proved

Weakening ignores the arbitrary new semantic value, at every binder kind.

@[simp] theorem interpret_weaken (t : Ty Δ κ) (ρ : KEnv SystemF.Rel Δ)
    (R : Kind.Sem SystemF.Rel μ) :
    (t.rename KVar.succ).interpret (KEnv.extend ρ R) = t.interpret ρ

Uses 10 · Used by 2

Statement usesKinded semantic environment · Extension of a kinded semantic environment · Kinded type variables of Fω · Kinds of pure Fω · Semantic interpretation of kinds · Intrinsically kinded Fω type operators · Relational interpretation of Fω types · Renaming of Fω type operators · Beta-invariant binary relations on the term model

Proof usesRelational interpretation of a renamed Fω type

Used byFundamental theorem of higher-kinded parametricity for Fω · Type translation preserves the relational interpretation

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.