Core Syntax

Kinds classify types and other compile-time-only entities. Each kind in the grammar is listed with a description of the sort of data it classifies.

$$\begin{array}{rrcll} \textrm{Kinds} & \kappa &::=& \mathsf{T... ...\ &&& (\kappa) & \textrm{explicit precedence} \\ \end{array}$$

Ur supports several different notions of functions that take types as arguments. These arguments can be either implicit, causing them to be inferred at use sites; or explicit, forcing them to be specified manually at use sites. There is a common explicitness annotation convention applied at the definitions of and in the types of such functions.

$$\begin{array}{rrcll} \textrm{Explicitness} & ? &::=& :: & \textrm{explicit} \\ &&& ::: & \textrm{implicit} \end{array}$$

Constructors are the main class of compile-time-only data. They include proper types and are classified by kinds.

$$\begin{array}{rrcll} \textrm{Constructors} & c, \tau &::=& (... ...\ &&& M.x & \textrm{projection from a module} \\ \end{array}$$

We include both abstraction and application for kind polymorphism, but applications are only inferred internally; they may not be written explicitly in source programs. Also, in the ``known-length type-level record'' form, in $c_1 = c_2$ terms, the parser currently only allows $c_1$ to be of the forms $X$ (as a shorthand for $\char93 X$ ) or $x$ , or a natural number to stand for the corresponding field name (e.g., for tuples).

Modules of the module system are described by signatures.

$$\begin{array}{rrcll} \textrm{Signatures} & S &::=& \mathsf{s... ...mathsf{of} \; \tau & \textrm{unary constructor} \\ \end{array}$$

Patterns are used to describe structural conditions on expressions, such that expressions may be tested against patterns, generating assignments to pattern variables if successful.

$$\begin{array}{rrcll} \textrm{Patterns} & p &::=& \_ & \textr... ...\ &&& M.X & \textrm{projection from a module} \\ \end{array}$$

Expressions are the main run-time entities, corresponding to both ``expressions'' and ``statements'' in mainstream imperative languages.

$$\begin{array}{rrcll} \textrm{Expressions} & e &::=& e : \tau... ...tt{and})^+ & \textrm{mutually recursive values} \\ \end{array}$$

As with constructors, we include both abstraction and application for kind polymorphism, but applications are only inferred internally.

Declarations primarily bring new symbols into context.

$$\begin{array}{rrcll} \textrm{Declarations} & d &::=& \mathsf... ...}(X : S) : S = M & \textrm{functor abstraction} \\ \end{array}$$

There are two kinds of Ur files. A file named $M\texttt{.ur}$ is an implementation file, and it should contain a sequence of declarations $d^*$ . A file named $M\texttt{.urs}$ is an interface file; it must always have a matching $M\texttt{.ur}$ and should contain a sequence of signature items $s^*$ . When both files are present, the overall effect is the same as a monolithic declaration $\mathsf{structure} \; M : \mathsf{sig} \; s^* \; \mathsf{end} = \mathsf{struct} \; d^* \; \mathsf{end}$ . When no interface file is included, the overall effect is similar, with a signature for module $M$ being inferred rather than just checked against an interface.

We omit some extra possibilities in $\mathsf{table}$ syntax, deferring them to Section 9.1.1. The concrete syntax of $\mathsf{view}$ declarations is also more complex than shown in the table above, with details deferred to Section 9.1.1.