Chapter 5  The Module System

• 5.1  Modules and module types
• 5.2  Typing Modules

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:S) S′, 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[] ⊢ S₁ <: S₂, denoting that a structure S₁ is a subtype of a structure S₂.
• E[] ⊢ e₁ <: e₂, denoting that a structure element e₁ is more precise that a structure element e₂.

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:S) S′)

Evaluation of structures to weak head normal form:

WEVAL-APP

E[] ⊢ S —→ Functor(X:S1) S2     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, {t₁/p₁.c₁,…,t_n/p_n.c_n} is the resulting substitution from the inlining mechanism. We substitute in S the inlined fields p_i.c_i form Mod(X:S₁) by the corresponding delta-reduced term t_i 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 e₁;…;e_n  End then S/p= Struct e₁/p;…;e_n/p  End where e/p is defined as follows:
  • Def()(c:=t:T)/p¹  =  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′)
  • Ind[Γ_P](Γ_C := Γ_I)/p  =  Ind_p()[Γ_P](

    ΓC:=ΓI  )

  • Ind_p′()[Γ_P](

    ΓC:=ΓI  )/p

     =  Ind_p′()[Γ_P](

    ΓC:=ΓI  )

• if S—→ Functor(X:S′) S″ then S/p=S

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-STR

E;e1;…;en[] ⊢ eσ(i) <: e′i for  i=1..m        σ : {1… m} → {1… n}  injective E[] ⊢  Struct e1;…;en  End <:  Struct e′1;…;e′m  End

MSUB-FUN

E[] ⊢  S1′  <:  S1           E; Mod(X:S1′)[] ⊢  S2  <:  S2′ E[] ⊢  Functor(X:S1) S2 <:  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′        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′  )

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 [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 :  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.