Chapter 5  The Module System

The module system extends the Calculus of Inductive Constructions providing a convenient way to structure large developments as well as a mean of massive abstraction.

5.1  Modules and module types

Access path.

It is denoted by p, it can be either a module variable X or, if p′ is an access path and id an identifier, then p′.id is an access path.

Structure element.

It is denoted by Impl and is either a definition of a constant, an assumption, a definition of an inductive or a definition of a module or a module type abbreviation.

Module expression.

It is denoted by M and can be:

• an access path p
• a structure Struct Impl ; … ; Impl  End
• a functor Functor(X:T) M′, where X is a module variable, T is a module type and M′ is a module expression
• an application of access paths p′ p″

Signature element.

It is denoted by Spec, it is a specification of a constant, an assumption, an inductive, a module or a module type abbreviation.

Module type,

denoted by T can be:

• a module type name
• an access path p
• a signature Sig Spec ; … ; Spec  End
• a functor type Funsig(X:T′) T″, where T′ and T″ are module types

Module definition,

written Mod(X:T:=M) can be a structure element. It consists of a module variable X, a module type T and a module expression M.

Module specification,

written ModS(X:T) or ModSEq(X:T==p) can be a signature element or a part of an environment. It consists of a module variable X, a module type T and, optionally, a module path p.

Module type abbreviation,

written ModType(S:=T), where S is a module type name and T is a module type.

5.2  Typing Modules

In order to introduce the typing system we first slightly extend the syntactic class of terms and environments given in section 4.1. The environments, apart from definitions of constants and inductive types now also hold any other signature elements. Terms, apart from variables, constants and complex terms, include also access paths.

We also need additional typing judgments:

• E[] ⊢ WF(T), denoting that a module type T is well-formed,
• E[] ⊢ M : T, denoting that a module expression M has type T in environment E.
• E[] ⊢ Impl : Spec, denoting that an implementation Impl verifies a specification Spec
• E[] ⊢ T₁ <: T₂, denoting that a module type T₁ is a subtype of a module type T₂.
• E[] ⊢ Spec₁ <: Spec₂, denoting that a specification Spec₁ is more precise that a specification Spec₂.

The rules for forming module types are the following:

WF-SIG

WF(E;E′)[] E[] ⊢  WF( Sig E′  End)

WF-FUN

E; ModS(X:T)[] ⊢  WF(T′) E[] ⊢  WF( Funsig(X:T) T′)

Rules for typing module expressions:

MT-STRUCT

E[] ⊢  WF( Sig Spec1;…;Specn  End)       E;Spec1;…;Speci−1[] ⊢ Impli : Speci for  i=1… n E[] ⊢  Struct Impl1;…;Impln  End :  Sig Spec1;…;Specn  End

MT-FUN

E; ModS(X:T)[] ⊢ M : T′ E[] ⊢  Functor(X:T) M :  Funsig(X:T) T′

MT-APP

E[] ⊢ p :  Funsig(X1:T1) … Funsig(Xn:Tn) T′       E[] ⊢ pi : Ti{X1/p1… Xi−1/pi−1} for  i=1… n E[] ⊢ p  p1 … pn : T′{X1/p1… Xn/pn}

MT-SUB

E[] ⊢ M : T            E[] ⊢ T <: T′ E[] ⊢ M : T′

MT-STR

E[] ⊢ p : T E[] ⊢ p : T/p

The last rule, called strengthening is used to make all module fields manifestly equal to themselves. The notation T/p has the following meaning:

• if T= Sig Spec₁;…;Spec_n  End then T/p= Sig Spec₁/p;…;Spec_n/p  End where Spec/p is defined as follows:
  • Def()(c:=U:t)/p  =  Def()(c:=U:t)
  • Assum()(c:U)/p  =  Def()(c:=p.c:U)
  • ModS(X:T)/p  =  ModSEq(X:T/p.X==p.X)
  • ModSEq(X:T==p′)/p  =  ModSEq(X:T/p==p′)
  • Ind()[Γ_P](Γ_C:=Γ_I )/p  =  Ind_p()[Γ_P](

    ΓC:=ΓI  )

  • Ind_p′()[Γ_P](

    ΓC:=ΓI  )

    /p  =  Ind_p′()[Γ_P](

    ΓC:=ΓI  )

• if T= Funsig(X:T′) T″ then T/p=T
• if T is an access path or a module type name, then we have to unfold its definition and proceed according to the rules above.

The notation Ind_p()[Γ_P](

denotes an inductive definition that is definitionally equal to the inductive definition in the module denoted by the path p. All rules which have Ind()[Γ_P](Γ_C:=Γ_I ) as premises are also valid for Ind_p()[Γ_P](

. We give the formation rule for Ind_p()[Γ_P](

below as well as the equality rules on inductive types and constructors.

The module subtyping rules:

MSUB-SIG

E;Spec1;…;Specn[] ⊢ Specσ(i) <: Spec′i for  i=1..m        σ : {1… m} → {1… n}  injective E[] ⊢  Sig Spec1;…;Specn  End <:  Sig Spec′1;…;Spec′m  End

MSUB-FUN

E[] ⊢ T1′ <: T1          E; ModS(X:T1′)[] ⊢ T2 <: T2′ E[] ⊢  Funsig(X:T1) T2 <:  Funsig(X:T1′) T2′

Specification subtyping rules:

ASSUM-ASSUM

E[] ⊢ U1 ≤βδιζ U2 E[] ⊢ Assum()(c:U1) <: Assum()(c:U2)

DEF-ASSUM

E[] ⊢ U1 ≤βδιζ U2 E[] ⊢ Def()(c:=t:U1) <: Assum()(c:U2)

ASSUM-DEF

E[] ⊢ U1 ≤βδιζ U2        E[] ⊢ c =βδιζ t2 E[] ⊢ Assum()(c:U1) <: Def()(c:=t2:U2)

DEF-DEF

E[] ⊢ U1 ≤βδιζ U2        E[] ⊢ t1 =βδιζ t2 E[] ⊢ Def()(c:=t1:U1) <: Def()(c:=t2:U2)

IND-IND

E[] ⊢ ΓP =βδιζ ΓP′        E[ΓP] ⊢ ΓC =βδιζ ΓC′        E[ΓP;ΓC] ⊢ ΓI =βδιζ ΓI′ E[] ⊢ Ind()[ΓP](ΓC:=ΓI ) <: Ind()[ΓP′](ΓC′:=ΓI′ )

INDP-IND

E[] ⊢ ΓP =βδιζ ΓP′        E[ΓP] ⊢ ΓC =βδιζ ΓC′        E[ΓP;ΓC] ⊢ ΓI =βδιζ ΓI′ E[] ⊢  Indp()[ΓP]( ΓC:=ΓI  )  <: Ind()[ΓP′](ΓC′:=ΓI′ )

INDP-INDP

E[] ⊢ ΓP =βδιζ ΓP′      E[ΓP] ⊢ ΓC =βδιζ ΓC′      E[ΓP;ΓC] ⊢ ΓI =βδιζ ΓI′      E[] ⊢ p =βδιζ p′ E[] ⊢  Indp()[ΓP]( ΓC:=ΓI  )  <:  Indp′()[ΓP′]( ΓC′:=ΓI′  )

MODS-MODS

E[] ⊢ T1 <: T2 E[] ⊢  ModS(m:T1) <:  ModS(m:T2)

MODEQ-MODS

E[] ⊢ T1 <: T2 E[] ⊢  ModSEq(m:T1==p) <:  ModS(m:T2)

MODS-MODEQ

E[] ⊢ T1 <: T2        E[] ⊢ m =βδιζ p2 E[] ⊢  ModS(m:T1) <:  ModSEq(m:T2==p2)

MODEQ-MODEQ

E[] ⊢ T1 <: T2        E[] ⊢ p1 =βδιζ p2 E[] ⊢  ModSEq(m:T1==p1) <:  ModSEq(m:T2==p2)

MODTYPE-MODTYPE

E[] ⊢ T1 <: T2        E[] ⊢ T2 <: T1 E[] ⊢  ModType(S:=T1) <:  ModType(S:=T2)

Verification of the specification

IMPL-SPEC

WF(E;Spec)[]       Spec  is one of   Def, Assum, Ind, ModType E[] ⊢ Spec : Spec

MOD-MODS

WF(E; ModS(m:T))[]        E[] ⊢ M : T E[] ⊢  Mod(m:T:=M) :  ModS(m:T)

MOD-MODEQ

WF(E; ModSEq(m:T==p))[]           E[] ⊢ p =βδιζ p′ E[] ⊢  Mod(m:T:=p′) :  ModSEq(m:T==p′)

New environment formation rules

WF-MODS

WF(E)[]        E[] ⊢  WF(T)  WF(E; ModS(m:T))[]

WF-MODEQ

WF(E)[]           E[] ⊢ p : T  WF(E, ModSEq(m:T==p))[]

WF-MODTYPE

WF(E)[]           E[] ⊢  WF(T)  WF(E, ModType(S:=T))[]

WF-IND

WF(E;Ind()[ΓP](ΓC:=ΓI ))[]       E[] ⊢ p: Sig Spec1;…;Specn;Ind()[ΓP′](ΓC′:=ΓI′ );…  End :  E[] ⊢ Ind()[ΓP′](ΓC′:=ΓI′ ){p.l/l}l ∈ labels(Spec1;…;Specn) <: Ind()[ΓP](ΓC:=ΓI )  WF(E; Indp()[ΓP]( ΓC:=ΓI  ) )[]

Component access rules

ACC-TYPE

E[Γ] ⊢ p :  Sig Spec1;…;Speci;Assum()(c:U);…  End E[Γ] ⊢ p.c : U{p.l/l}l ∈ labels(Spec1;…;Speci)

E[Γ] ⊢ p :  Sig Spec1;…;Speci;Def()(c:=t:U);…  End E[Γ] ⊢ p.c : U{p.l/l}l ∈ labels(Spec1;…;Speci)

ACC-DELTA

Notice that the following rule extends the delta rule defined in section 4.3

E[Γ] ⊢ p :  Sig Spec1;…;Speci;Def()(c:=t:U);…  End E[Γ] ⊢ p.c ▷δ t{p.l/l}l ∈ labels(Spec1;…;Speci)

In the rules below we assume Γ_P is [p₁:P₁;…;p_r:P_r], Γ_I is [I₁:A₁;…;I_k:A_k], and Γ_C is [c₁:C₁;…;c_n:C_n]

ACC-IND

E[Γ] ⊢ p :  Sig Spec1;…;Speci;Ind()[ΓP](ΓC:=ΓI );…  End E[Γ] ⊢ p.Ij : (p1:P1)…(pr:Pr)Aj{p.l/l}l ∈ labels(Spec1;…;Speci)

E[Γ] ⊢ p :  Sig Spec1;…;Speci;Ind()[ΓP](ΓC:=ΓI );…  End E[Γ] ⊢ p.cm : (p1:P1)…(pr:Pr)Cm{Ij/(Ij p1… pr)}j=1… k{p.l/l}l ∈ labels(Spec1;…;Speci)

ACC-INDP

E[] ⊢ p :  Sig Spec1;…;Specn; Indp′()[ΓP]( ΓC:=ΓI  ) ;…  End E[] ⊢ p.Ii ▷δ p′.Ii

E[] ⊢ p :  Sig Spec1;…;Specn; Indp′()[ΓP]( ΓC:=ΓI  ) ;…  End E[] ⊢ p.ci ▷δ p′.ci

ACC-MOD

E[Γ] ⊢ p :  Sig Spec1;…;Speci; ModS(m:T);…  End E[Γ] ⊢ p.m : T{p.l/l}l ∈ labels(Spec1;…;Speci)

E[Γ] ⊢ p :  Sig Spec1;…;Speci; ModSEq(m:T==p′);…  End E[Γ] ⊢ p.m : T{p.l/l}l ∈ labels(Spec1;…;Speci)

ACC-MODEQ

E[Γ] ⊢ p :  Sig Spec1;…;Speci; ModSEq(m:T==p′);…  End E[Γ] ⊢ p.m ▷δ p′{p.l/l}l ∈ labels(Spec1;…;Speci)

ACC-MODTYPE

E[Γ] ⊢ p :  Sig Spec1;…;Speci; ModType(S:=T);…  End E[Γ] ⊢ p.S ▷δ T{p.l/l}l ∈ labels(Spec1;…;Speci)

The function labels() is used to calculate the set of label of the set of specifications. It is defined by labels(Spec₁;…;Spec_n)=labels(Spec₁)∪…;∪labels(Spec_n) where labels(Spec) is defined as follows:

• labels(Assum(Γ)(c:U))={c},
• labels(Def(Γ)(c:=t:U))={c},
• labels(Ind(Γ)[Γ_P](Γ_C:=Γ_I ))=dom(Γ_C)∪dom(Γ_I),
• labels( ModS(m:T))={m},
• labels( ModSEq(m:T==M))={m},
• labels( ModType(S:=T))={S}

Environment access for modules and module types

ENV-MOD

WF(E; ModS(m:T);E′)[Γ] E; ModS(m:T);E′[Γ] ⊢ m : T

WF(E; ModSEq(m:T==p);E′)[Γ] E; ModSEq(m:T==p);E′[Γ] ⊢ m : T

ENV-MODEQ

WF(E; ModSEq(m:T==p);E′)[Γ] E; ModSEq(m:T==p);E′[Γ] ⊢ m ▷δ p

ENV-MODTYPE

WF(E; ModType(S:=T);E′)[Γ] E; ModType(S:=T);E′[Γ] ⊢ S ▷δ T

ENV-INDP

WF(E; Indp()[ΓP]( ΓC:=ΓI  ) )[] E;Indp()[ΓP]( ΓC:=ΓI  ) [] ⊢ Ii ▷δ p.Ii

WF(E; Indp()[ΓP]( ΓC:=ΓI  ) )[] E;Indp()[ΓP]( ΓC:=ΓI  ) [] ⊢ ci ▷δ p.ci