XXX: Make parameter P : S just declare P which can then be open-ed (at least for the core calculus)

XXX: It may be useful to allow type constraints at the top-level of a module---this would allow constraining type parameters from different parameters

Modules

A module is for managing names, and may:

• bring things into scope via imports (or open, see later)
• define new entities via definitions
• a module may export some of the entities that are in scope in it

Nested Modules

Modules may be nested.

• An entity that's in scope in a module, is also in scope in all its nested modules (i.e., the parent module is implicit imported)
• Names in nested module may shadow names in outer modules.
• A nested module declaration brings a new module entity in scope
• import always refers to a top-level module (found in the usual way)
• We use open, which is similar to import but is used to bring names from nested modules in scope.

Examples

Example 1: Basic use

module A where   // A top level (ordinary) module

  module B where // A nested module declaration
    x = 0x2

  open B        // This is OK because `B` is in scope

  y = x         // `x` got in scope via the import above

Example 2: Nested modules may refer to each other

module A where

  module B where
    x = 0x2

  module C where
    open B       // This is OK because `B` is in scope
    z = x

  open C

  y = z
  // y = x            // Error: `x` is not in scope

Example 3: Importing a nested module

module A where

  module B where
    x = 0x2

module C where

  import qualified A    // Brings `A::B` into scope
  open A::B             // This is the `B` imported above

Syntactic sugar

• Define and open a nested module (see Example 1)

open module A where // Also a variant where the name can be omitted
  ...

means

module A where
  ...

open A

• Open a nested module (see Example 3)

import open A::B    -- XXX: hm

means

import A as Anon
open Anon::B

Signatures

A signature is a named set of module parameters, which may be:

• type parameters of a specific kind
• constraints on the type parameters
• value parameters, of a specific (possibly polymorphic) type

Example:

signature A where
  type n : #                  // type parameter
  type constraint (n <= 64)   // constraint on type parameter
  len : [n]                   // value parameter

A declaration like the above defines a new signature entity called A.

• Signature declarations reside within other modules.
• The parameter names in a signature shadow names from the outer module scope.

Parameterized Modules

A module may be parameterized by a signature, with a parameter declaration:

parameter P : S   // `P` is the parameter name
                  // `S` is the name of a signature that is in scope

A parameter declaration is similar to an import, in that it brings the parameters from the specified signature in scope---the parameters may be used like ordinary values or types.

Similar to imports, parameters may be brought into scope with a qualifier:

parameter P : S as Q

A declaration like this would bring the parameters from S in scope qualified by the prefix Q

Syntactic sugar

• unnamed parameters

parameter S

means

parameter S : S

• combined parameter and signature declaration:

parameter
  v : [64]

means

signature Anon
  v : [64]

parameter Anon : Anon

Multiple anonymous parameter blocks are combined into a single anonymous signature and parameter.

Instantiating Modules

New modules may be defined with a module instantiation declaraiont:

module A = M with { P = N1; Q = N2 }

• This declaration defines a new module entity A, that may be used like any other module.
• M, N1, and N2 are module entities
  • M must contain a parameter declarations P : S1 and Q : S2
  • N1 should match S1 and N2 S2.

Syntactic sugar:

• omit parameter name if M has only a single parameter:

module A = M with N

• inline module declarations:

module A = M with
  module P where
    ...
  module Q where
    ...

means:

module Anon1 where
  ...
module Anon2 where
   ...
module A = M with { P = Anon1, Q = Anon2 }

• inline declarations when only a single signature parameter:

module A = M where
  x = 64

means:

module Anon where
  x = 64
module A = M with { P = Anon }  // P is the only parameter of `M`

• combined import and instantiation

open (M where x = 64)

Generative and Applicative

Instantiating a module with the same parameters gives rise to the same module. For example, consider:

module A = M with { P = N }
module B = M with { P = N }

A and B are two distinct module entities that refer to the same module. This can be observed when resolving names, or with newtypes.

Anonymous modules generate new modules distinct from everything else. Consider, for example:

module C = M where x = 64
module D = M where x = 64

C and D are two distinct module entities that refer to different modules, because the desugared version is:

module Anon1 where
  x = 64
module Anon2 where
  x = 62
module C = M with { P = Anon1 }
module D = M with { P = Anon2 }

Core Abstract Syntax

ModuleExpr =
   Module [Decl]                                   -- define a new module
 | ModulInst ModuleExpr (Map Name ModuleExpr)      -- define by instantiation
 | ModuleName Name                                 -- reference to a module that's in scope
 | ModuleSig ModuleExpr Name                       -- Annotate a module with a signature

Decl =
 ...
 | Signature Name [ SigParam ]         -- Declare a signature
 | Parameter Name Name                 -- param name, signature name
 | Module Name ModuleExpr              -- declare a new module
 | Open ModuleExpr (Maybe Name)        -- bring names from a nested module module in scope