The Wyn Language Specification

Modules

Grammar

mod_bind      ::= "module" name mod_param* "=" [":" mod_type_exp] "=" mod_exp
mod_param     ::= "(" name ":" mod_type_exp ")"
mod_type_bind ::= "module" "type" name "=" mod_type_exp

Wyn supports an ML-style higher-order module system. Modules can contain types, functions, and other modules and module types. Module types are used to classify the contents of modules, and parametric modules are used to abstract over modules (essentially module-level functions). In Standard ML, modules, module types and parametric modules are called structs, signatures, and functors, respectively. Module names exist in the same name space as values, but module types are their own name space.

Module Bindings

module m = mod_exp

Binds m to the module produced by the module expression mod_exp. Any name x in the module produced by mod_exp can then be accessed with m.x.

module m : mod_type_exp = mod_exp

Shorthand for module m = mod_exp : mod_type_exp.

module m mod_params… = mod_exp

Shorthand for module m = \mod_params... -> mod_exp. This produces a parametric module.

module type mt = mod_type_exp

Binds mt to the module type produced by the module type expression mod_type_exp.

Module Expressions

mod_exp ::= qualname
            | mod_exp ":" mod_type_exp
            | "\" "(" mod_param* ")" [":" mod_type_exp] "->" mod_exp
            | mod_exp mod_exp
            | "(" mod_exp ")"
            | "{" dec* "}"
            | "import" stringlit

A module expression produces a module. Modules are collections of bindings produced by declarations (dec). In particular, a module may contain other modules or module types.

qualname

Evaluates to the module of the given name.

(mod_exp)

Evaluates to mod_exp.

mod_exp : mod_type_exp

Module ascription evaluates the module expression and the module type expression, verifies that the module implements the module type, then returns a module that exposes only the functionality described by the module type. This is how internal details of a module can be hidden.

As a slightly ad-hoc limitation, ascription is forbidden when a type substitution of size-lifted types occurs in a size appearing at the top level.

(p: mt1): mt2 -> e

Constructs a parametric module (a function at the module level) that accepts a parameter of module type mt1 and returns a module of type mt2. The latter is optional, but the parameter type is not.

e1 e2

Apply the parametric module m1 to the module m2.

Returns a module that contains the given definitions. The resulting module defines any name defined by any declaration that is not local, in particular including names made available via open.

import “foo”

Returns a module that contains the definitions of the file “foo” relative to the current file.

Module Type Expressions

mod_type_exp ::= qualname
                 | "{" spec* "}"
                 | mod_type_exp "with" qualname type_param* "=" type
                 | "(" mod_type_exp ")"
                 | "(" name ":" mod_type_exp ")" "->" mod_type_exp
                 | mod_type_exp "->" mod_type_exp

spec ::= "val" name type_param* ":" type
         | "val" "(" symbol ")" ":" type
         | "val" symbol type_param* ":" type
         | ("type" | "type^" | "type~") name type_param* "=" type
         | ("type" | "type^" | "type~") name type_param*
         | "module" name ":" mod_type_exp
         | "include" mod_type_exp
         | "#[" attr "]" spec

Module types classify modules, with the only (unimportant) difference in expressivity being that modules can contain module types, but module types cannot specify that a module must contain a specific module type. They can specify of course that a module contains a submodule of a specific module type.

A module type expression can be the name of another module type, or a sequence of specifications, or specs, enclosed in curly braces. A spec can be a value spec, indicating the presence of a function or value, an abstract type spec, or a type abbreviation spec.

In a value spec, sizes in types on the left-hand side of a function arrow must not be anonymous. For example, this is forbidden:

sig sum: []t -> t

Instead write:

sig sum [n]: [n]t -> t

But this is allowed, because the empty size is not to the left of a function arrow:

sig evens [n]: [n]i32 -> []i32

Referencing Other Files

You can refer to external files in a Wyn file like this:

import "file"

The above will include all non-local top-level definitions from file.fut is and make them available in the current file (but will not export them). The .fut extension is implied.

You can also include files from subdirectories:

import "path/to/a/file"

The above will include the file path/to/a/file.fut relative to the including file.

Qualified imports are also possible, where a module is created for the file:

module M = import "file"

In fact, a plain import "file" is equivalent to:

local open import "file"

To re-export names from another file in the current module, use:

open import "file"