# 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 means 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 e and is either a definition of a constant, an assumption, a definition of an inductive, a definition of a module, an alias of module or a module type abbreviation.

##### Structure expression.

It is denoted by S and can be:

• an access path p
• a plain structure Struct e ;; e  End
• a functor Functor(X:SS′, where X is a module variable, S and S′ are structure expression
• an application S p, where S is a structure expression and p an access path
• a refined structure S  with p := p′ or S  with p := t:T where S is a structure expression, p and p′ are access paths, t is a term and T is the type of t.
##### Module definition,

is written Mod(X:S [:=S]) and consists of a module variable X, a module type S which can be any structure expression and optionally a module implementation S′ which can be any structure expression except a refined structure.

##### Module alias,

is written ModA(X==p) and consists of a module variable X and a module path p.

##### Module type abbreviation,

is written ModType(Y:=S), where Y is an identifier and S is any structure expression .

## 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 structure elements. Terms, apart from variables, constants and complex terms, include also access paths.

We also need additional typing judgments:

• E[] ⊢ WF(S), denoting that a structure S is well-formed,
• E[] ⊢ p : S, denoting that the module pointed by p has type S in environment E.
• E[] ⊢ S —→ S, denoting that a structure S is evaluated to a structure S in weak head normal form.
• E[] ⊢ S1 <: S2, denoting that a structure S1 is a subtype of a structure S2.
• E[] ⊢ e1 <: e2, denoting that a structure element e1 is more precise that a structure element e2.

The rules for forming structures are the following:

WF-STR
 WF(E;E′)[] E[] ⊢  WF( Struct E′  End)
WF-FUN
E; Mod(X:S)[] ⊢  WF(
 S′
)
E[] ⊢  WF( Functor(X:SS′)

Evaluation of structures to weak head normal form:

WEVAL-APP
E[] ⊢ S —→ Functor(X:S1S2     E[] ⊢ S1 —→ S1
E[] ⊢ p : S3     E[] ⊢ S3 <:
 S1
E[] ⊢ S p —→ S2{p/X,t1/p1.c1,…,tn/pn.cn}

In the last rule, {t1/p1.c1,…,tn/pn.cn} is the resulting substitution from the inlining mechanism. We substitute in S the inlined fields pi.ci form Mod(X:S1) by the corresponding delta-reduced term ti in p.

WEVAL-WITH-MOD
E[] ⊢ S —→ Struct e1;…;ei; Mod(X:S1);ei+2;… ;en  End     E;e1;…;ei[] ⊢ S1 —→ S1
E[] ⊢ p : S2     E;e1;…;ei[] ⊢ S2 <:
 S1
 E[] ⊢ S  with x := p —→ Struct e1;…;ei; ModA(X==p);ei+2{p/X} ;…;en{p/X}  End
WEVAL-WITH-MOD-REC
 E[] ⊢ S —→ Struct e1;…;ei; Mod(X1:S1);ei+2;… ;en  End E;e1;…;ei[] ⊢ S1  with p := p1 —→ S2
 E[] ⊢ S  with X1.p := p1 —→ Struct e1;…;ei; Mod(X:S2);ei+2{p1/X1.p} ;…;en{p1/X1.p}  End
WEVAL-WITH-DEF
 E[] ⊢ S —→ Struct e1;…;ei;Assum()(c:T1);ei+2;… ;en  End E;e1;…;ei[] ⊢ Def()(c:=t:T) <: Assum()(c:T1)
 E[] ⊢ S  with c := t:T —→ Struct e1;…;ei;Def()(c:=t:T);ei+2;… ;en  End
WEVAL-WITH-DEF-REC
 E[] ⊢ S —→ Struct e1;…;ei; Mod(X1:S1);ei+2;… ;en  End E;e1;…;ei[] ⊢ S1  with p := p1 —→ S2
 E[] ⊢ S  with X1.p := t:T —→ Struct e1;…;ei; Mod(X:S2);ei+2;… ;en  End
WEVAL-PATH-MOD
 E[] ⊢ p —→ Struct e1;…;ei; Mod(X:S [:=S1]);ei+2;… ;en  End E;e1;…;ei[] ⊢ S —→ S
E[] ⊢ p.X —→ S
 WF(E)[]       Mod(X:S [:=S1])∈ E E[] ⊢ S —→ S
E[] ⊢ X —→ S
WEVAL-PATH-ALIAS
 E[] ⊢ p —→ Struct e1;…;ei; ModA(X==p1);ei+2;… ;en  End E;e1;…;ei[] ⊢ p1 —→ S
E[] ⊢ p.X —→ S
 WF(E)[]        ModA(X==p1)∈ E E[] ⊢ p1 —→ S
E[] ⊢ X —→ S
WEVAL-PATH-TYPE
 E[] ⊢ p —→ Struct e1;…;ei; ModType(Y:=S);ei+2;… ;en  End E;e1;…;ei[] ⊢ S —→ S
E[] ⊢ p.Y —→ S
WEVAL-PATH-TYPE
 WF(E)[]        ModType(Y:=S)∈ E E[] ⊢ S —→ S
E[] ⊢ Y —→ S

Rules for typing module:

MT-EVAL
E[] ⊢ p —→ S
E[] ⊢ p :
 S
MT-STR
 E[] ⊢ p : S E[] ⊢ p : S/p

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

• if S—→ Struct e1;…;en  End then S/p= Struct e1/p;…;en/p  End where e/p is defined as follows:
• Def()(c:=t:T)/p1  =  Def()(c:=t:T)
• Assum()(c:U)/p  =  Def()(c:=p.c:U)
• Mod(X:S)/p  =  ModA(X==p.X)
• ModA(X==p′)/p  =  ModA(X==p′)
• IndP](ΓC := ΓI)/p  =  Indp()[ΓP]( ΓC:=ΓI  )
• Indp()[ΓP]( ΓC:=ΓI  )/p
=  Indp()[ΓP]( ΓC:=ΓI  )
• if S—→ Functor(X:S′) S″ then S/p=S

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 IndP](Γ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-STR
 E;e1;…;en[] ⊢ eσ(i) <: e′i for  i=1..m σ : {1… m} → {1… n}  injective
E[] ⊢  Struct e1;…;en  End <:  Struct e1;…;em  End
MSUB-FUN
E[] ⊢
 S1′
<:
 S1
E; Mod(X:S1′)[] ⊢
 S2
<:
 S2′
E[] ⊢  Functor(X:S1S2 <:  Functor(X:S1′) S2

Structure element subtyping rules:

ASSUM-ASSUM
 E[] ⊢ T1 ≤βδιζη T2 E[] ⊢ Assum()(c:T1) <: Assum()(c:T2)
DEF-ASSUM
 E[] ⊢ T1 ≤βδιζη T2 E[] ⊢ Def()(c:=t:T1) <: Assum()(c:T2)
ASSUM-DEF
 E[] ⊢ T1 ≤βδιζη T2        E[] ⊢ c =βδιζη t2 E[] ⊢ Assum()(c:T1) <: Def()(c:=t2:T2)
DEF-DEF
 E[] ⊢ T1 ≤βδιζη T2        E[] ⊢ t1 =βδιζη t2 E[] ⊢ Def()(c:=t1:T1) <: Def()(c:=t2:T2)
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′        EP] ⊢ ΓC =βδιζη ΓC′        EPC] ⊢ ΓI =βδιζη ΓI
E[] ⊢ Indp()[ΓP](
 ΓC:=ΓI  )
<: IndP′](Γ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′  )
MOD-MOD
 E[] ⊢ S1 <: S2 E[] ⊢  Mod(X:S1) <:  Mod(X:S2)
ALIAS-MOD
 E[] ⊢ p : S1        E[] ⊢ S1 <: S2 E[] ⊢  ModA(X==p) <:  Mod(X:S2)
MOD-ALIAS
 E[] ⊢ p : S2         E[] ⊢ S1 <: S2        E[] ⊢ X =βδιζη p E[] ⊢  Mod(X:S1) <:  ModA(X==p)
ALIAS-ALIAS
 E[] ⊢ p1 =βδιζη p2 E[] ⊢  ModA(X==p1) <:  ModA(X==p2)
MODTYPE-MODTYPE
 E[] ⊢ S1 <: S2        E[] ⊢ S2 <: S1 E[] ⊢  ModType(Y:=S1) <:  ModType(Y:=S2)

New environment formation rules

WF-MOD
 WF(E)[]        E[] ⊢  WF(S) WF(E; Mod(X:S))[]
WF-MOD
 E[] ⊢ S2 <: S1 WF(E)[]     E[] ⊢  WF(S1)     E[] ⊢  WF(S2)
WF(E; Mod(X:S1 [:=S2]))[]
WF-ALIAS
 WF(E)[]           E[] ⊢ p : S WF(E, ModA(X==p))[]
WF-MODTYPE
 WF(E)[]           E[] ⊢  WF(S) WF(E, ModType(Y:=S))[]
WF-IND
 WF(E;Ind[ΓP](ΓC := ΓI))[] E[] ⊢ p: Struct e1;…;en;Ind[ΓP′](ΓC′ := ΓI′);…  End : E[] ⊢ Ind[ΓP′](ΓC′ := ΓI′) <: Ind[ΓP](ΓC := ΓI)
WF(E;Indp()[ΓP](
 ΓC:=ΓI  )
)[]

Component access rules

ACC-TYPE
 E[Γ] ⊢ p :  Struct e1;…;ei;Assum()(c:T);…  End E[Γ] ⊢ p.c : T

 E[Γ] ⊢ p :  Struct e1;…;ei;Def()(c:=t:T);…  End E[Γ] ⊢ p.c : T
ACC-DELTA
Notice that the following rule extends the delta rule defined in section 4.3
 E[Γ] ⊢ p :  Struct e1;…;ei;Def()(c:=t:U);…  End E[Γ] ⊢ p.c ▷δ t

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 :  Struct e1;…;ei;Ind[ΓP](ΓC := ΓI);…  End E[Γ] ⊢ p.Ij : (p1:P1)…(pr:Pr)Aj
 E[Γ] ⊢ p :  Struct e1;…;ei;Ind[ΓP](ΓC := ΓI);…  End E[Γ] ⊢ p.cm : (p1:P1)…(pr:Pr)CmIj(Ij p1… pr)j=1… k
ACC-INDP
E[] ⊢ p :  Struct e1;…;ei;Indp()[ΓP](
 ΓC:=ΓI  )
;…  End
E[] ⊢ p.Iiδ p′.Ii
E[] ⊢ p :  Struct e1;…;ei;Indp()[ΓP](
 ΓC:=ΓI  )
;…  End
E[] ⊢ p.ciδ p′.ci

1
Opaque definitions are processed as assumptions.