# 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:TM', 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[] ⊢ T1 <: T2, denoting that a module type T1 is a subtype of a module type T2.

• E[] ⊢ Spec1 <: Spec2, denoting that a specification Spec1 is more precise that a specification Spec2.
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:TT')
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:TM : Funsig(X:TT'
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 Spec1;...;Specn  End then T/p= Sig Spec1/p;...;Specn/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  =  Indp()[ΓP]( ΓC:=ΓI  )
• Indp'()[ΓP]( ΓC:=ΓI  )
/p  =  Indp'()[Γ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 Indp()[ΓP](
 ΓC:=ΓI  )
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 Indp()[ΓP](
 ΓC:=ΓI  )
. We give the formation rule for Indp()[ΓP](
 ΓC:=ΓI  )
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:T1T2 <: 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'        EP] ⊢ ΓC =βδιζ ΓC'        EPC] ⊢ ΓI =βδιζ ΓI'
E[] ⊢ Ind()[ΓP](ΓC:=ΓI ) <: Ind()[ΓP'](ΓC':=ΓI' )
INDP-IND
E[] ⊢ ΓP =βδιζ ΓP'        EP] ⊢ ΓC =βδιζ ΓC'        EPC] ⊢ ΓI =βδιζ ΓI'
E[] ⊢ Indp()[ΓP](
 ΓC:=ΓI  )
<: Ind()[ΓP'](ΓC':=ΓI' )
INDP-INDP
E[] ⊢ ΓP =βδιζ ΓP'      EP] ⊢ ΓC =βδιζ ΓC'      EPC] ⊢ Γ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}llabels(Spec1;...;Speci)

E[Γ] ⊢ p : Sig Spec1;...;Speci;Def()(c:=t:U);...  End
E[Γ] ⊢ p.c : U{p.l/l}llabels(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}llabels(Spec1;...;Speci)

In the rules below we assume ΓP is [p1:P1;…;pr:Pr], ΓI is [I1:A1;…;Ik:Ak], and ΓC is [c1:C1;…;cn:Cn]
ACC-IND
E[Γ] ⊢ p : Sig Spec1;...;Speci;Ind()[ΓP](ΓC:=ΓI );...  End
E[Γ] ⊢ p.Ij : (p1:P1)…(pr:Pr)Aj{p.l/l}llabels(Spec1;...;Speci)
E[Γ] ⊢ p : Sig Spec1;...;Speci;Ind()[ΓP](ΓC:=ΓI );...  End
E[Γ] ⊢ p.cm : (p1:P1)…(pr:Pr)Cm{Ij/(Ij p1pr)}j=1… k{p.l/l}llabels(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}llabels(Spec1;...;Speci)

E[Γ] ⊢ p : Sig Spec1;...;Speci; ModSEq(m:T==p');...  End
E[Γ] ⊢ p.m : T{p.l/l}llabels(Spec1;...;Speci)
ACC-MODEQ
E[Γ] ⊢ p : Sig Spec1;...;Speci; ModSEq(m:T==p');...  End
E[Γ] ⊢ p.mδ p'{p.l/l}llabels(Spec1;...;Speci)
ACC-MODTYPE
E[Γ] ⊢ p : Sig Spec1;...;Speci; ModType(S:=T);...  End
E[Γ] ⊢ p.Sδ T{p.l/l}llabels(Spec1;...;Speci)
The function labels() is used to calculate the set of label of the set of specifications. It is defined by labels(Spec1;...;Specn)=labels(Spec1)∪...;∪labels(Specn) where labels(Spec) is defined as follows:
• labels(Assum(Γ)(c:U))={c},
• labels(Def(Γ)(c:=t:U))={c},
• labels(Ind(Γ)[ΓP](ΓC:=ΓI ))=domC)∪domI),
• 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