Skip to content

Modules, namespaces and name resolution

Jump to bottom Edit New page
Tahina Ramananandro (professional account) edited this page Mar 3, 2017 · 13 revisions

F* has had modules and namespaces since its inception. Pull request 772 introduces a number of related improvements, which this article explains in extenso.

Modules

Similarly to OCaml, a F* module is a collection of top-level definitions of types, terms (and also effects), introduced by a module name:

module ModuleA
 
let term = 18
 
type typ = | Datacon1 | Datacon2

Similarly to OCaml, the name of a module must start with an uppercase letter.

A module must be stored in a file such that the basename (without the .fst file name extension) converted in lowercase must match the module name converted in lowercase. In this example, any one of modulea.fst, ModuleA.fst, MODULEA.FST will work.

Now, another module, say ModuleB, can access the definitions of ModuleA by qualifying each definition with the name of the module:

module ModuleB
 
let b : bool = true

let example : ModuleA.typ =
  if b
  then ModuleA.Datacon1
  else if ModuleA.term = 42
       then ModuleA.Datacon1
       else ModuleA.Datacon2

IMPORTANT: Contrary to OCaml, F* has no nested modules. In other words, a module cannot contain other modules. Thus, a F* source file always contains exactly one module.

open

However, it is not always necessary to manually qualify every access to ModuleA in ModuleB. Similarly to OCaml, F* allows users to access definitions of ModuleA without qualifying them, using the open keyword. Thus ModuleB can be equivalently rewritten as ModuleC below:

module ModuleC
 
let b : bool = true
 
open ModuleA
 
let example : typ =
  if b
  then Datacon1
  else if term = 42
       then Datacon1
       else Datacon2

In this example, open ModuleA makes the definitions of ModuleA reachable from within ModuleC without being qualified.

NOTE: open only applies within the module it is declared. For instance, accessing ModuleC from outside will not have ModuleA automatically reachable through ModuleC. :

let example2 = ModuleC.example
let term2 = ModuleC.term (* <-- this will fail. *)
let term3 = ModuleA.term (* <-- this will succeed. *)

Shadowing and local open

Consider the following example:

module K
let z = 18

module L
open K
let z = 42
let example = z

In this example, z is defined after open K, so z shadows K.z and example has value 42.

However, consider the following example:

module U
let left = 1
let middle = 2
let right = 3

module V
let left = 4
open U
let example = left + (middle + right)

Here, in fact, example will have value 1+2+3 instead of 4+2+3, because open U brings all definitions of U into the current scope, thus making U.left shadow V.left.

It is however possible to open a module only in the middle of a term rather than globally:

module W
let left = 4
let example = left + let open U in (middle + right)

Equivalently, let open Module in term has an alternative syntax Module.(term) also borrowed from OCaml, so that module W is syntactically equivalent to the following:

module W
let left = 4
let example = left + U.(middle + right)

NOTE: .( is a token, i.e. no whitespace is allowed in between . and (

Local open and interleaving

Consider the following example:

module M
let a = 1
let b = 2

module N
let example =
  let a = 3 in
  let open M in
  let b = 4 in
  a + b

Here, example will have value 1+4 because let open M makes M.a shadow the locally-defined a, but since b is defined after let open M, it thus shadows M.b.

Namespaces

A module name can itself be qualified by names (each starting with an upper-case letter), yielding a long module name. For instance:

module A.X
let u = 18

Module A.X can be defined regardless of whether module A is defined or not. As before, A.X must be stored in a file such that the basename converted in lowercase is the same as the whole module name converted in lowercase, such as a.x.fst, a.X.fst, A.x.fst, etc.

TODO: do we have path-defined namespaces à la Coq?

The purpose of modules with long names is to define namespaces that can also be opened, this time similary to F#. The following example is thus valid:

module A.X
let u = 18

module A.Y
let v = 42

module B
open A
let example = X.18 + Y.42

In this example, A is said to be a namespace that is opened to resolve module names.

IMPORTANT: There are several restrictions:

  • similarly to F#, this example no longer works if module A is defined. More precisely, if A is a module, then A is no longer a namespace and open A only opens the module, not the namespace. For example:

    module B
let u = 18

module B.X
let v = 42

module C
open B
let example1 = u (* <-- works, resolves to B.u *)
let example2 = X.v (* <-- resolves to X.v, not B.X.v, thus fails *)

  • In open A, name A is taken as is, and does not trigger namespace-based name resolution:

    module A.X.Y
let u = 18

module B
open A
open X  (* <-- opens module/namespace X, not A.X *)
let example = Y.u (* resolves to Y.u, not A.X.Y.u, thus fails *)

Module abbreviations

Long module names can be too long. So, it is possible to define module abbreviations:

module A.Very.Long.Name
let x = 18

module B
module AVLN = A.Very.Long.Name
let example = AVLN.x

There are several restrictions, however:

  • Module abbreviations are only reachable from within the module where they are defined.

    module A
let x = 18

module B
module C = A

module D
let example = B.C.x (* <-- resolves to B.C.x, not A.x, thus fails *)

    This is consistent with the principle that F* has no nested modules.

  • A module abbreviation itself cannot be qualified, so module A.B = C is forbidden.

  • When defining a module abbreviation, the module name must be fully qualified. In other words, open-based module name resolution is not honored on the right-hand-side of a module abbreviation:

    module A.B
let x = 18

module C
open A
module D = B (* <-- resolves to B, not A.B, so fails *)

  • A module abbreviation only rewrites a module name, not part of a namespace name:

    module A
let x = 18

module A.U
let y = 42

module B
module C = A
let example = C.U.y (* <-- resolves to C.U.y, not A.U.y, thus fails *)

As an extra feature, open M works if M is a module abbrev, such as in the following example:

module A
let x = 18

module B
module C = A
open C (* <-- module abbrev allowed, so actually opens module A *)
let example = x (* <-- works, resolves to A.x *)

include

It is sometimes desirable to split a library into several distinct modules A1, A2, etc. (for instance, when A1 contains abstract definitions and A2 should be based only on A1's definition types) and still have the end user access all definitions through a single module name A. To this end, we provide the include feature.

From within a module, include behaves like open except that it is restricted to modules (namespaces are not allowed.)

The main impact of include is outside of the module it is declared. Consider the following example:

module A
let x : int = 18

module B
include A
let y : bool = true
let k = x (* succeeds, resolves into A.x *)

module C
let z = B.y (* succeeds *)
let t = B.x (* succeeds, resolves into A.x *)

Within B, include A behaves like open A, so x resolves into A.x. What includes offers more is that this resolution exposes x as if it were defined in B, so that any occurrence of B.x resolves into A.x. (Internally however, the definition of x in A is not copied into B; instead, include is fully based on name resolution.)

  • include is sensitive to shadowing of definitions:

    module U
let x = 18
let y = 42

module V
include U
let y = 1 (* shadows U.y *)

module W
let z = V.x (* resolves into U.x *)
let t = V.y (* resolves into V.y *)

  • include is sensitive to shadowing by include itself:

    module R
let x = 18
let y = 42

module S
let x = 1729

module T
include R
include S (* shadows R.x *)

module U
let z = T.y (* succeeds, resolves into R.y *)
let t = T.x (* succeeds, resolves into S.x *)

  • include is transitive

    module K
let x = 18

module L
include K

module M
include L

module N
let y = M.x (* succeeds, resolves into K.x *)

  • include is compatible with open

    module D
let x = 18

module E
include D

module F
open E
let y = x (* succeeds, resolves into D.x *)

  • include B does not expose module abbreviations defined in B or its included ancestors:

    module A
let x = 18

module B
module Z = A

module C
include B

module D
let y = C.Z.x (* resolves into C.Z.x, not A.x, thus fails *)

include is now actively used in the standard library:

  • FStar.Seq is obtained by "merging" FStar.Seq.Base and FStar.Seq.Properties through include
  • similarly, FStar.List.Tot is obtained from FStar.List.Tot.Base and FStar.List.Tot.Properties

Summary: name resolution

open A

  • A must be a fully qualified namespace or module name, or a module abbrev. In other words, open is not honored to resolve A itself, but module A = ... is.
  • If module A is defined, then opens the module A only.
  • Otherwise, opens the whole namespace A.

module A = B

  • A must be a short name (not qualified)
  • B must be a fully qualified module name, so neither module B = ... nor open B are honored to resolve B itself.
  • Only rewrites module A, not namespace prefix A.

module A include B

  • B must be a fully qualified module name, or a module abbrev (not a namespace.)
  • From within A, behaves like open B
  • From outside of A, any term or type x (but not module abbrev) defined in B not subsequently shadowed in A can be referred to as A.x
  • include is transitive
Add a custom footer
Add a custom sidebar
Clone this wiki locally