next up previous contents
Next: Shorthands Up: Ur Syntax Previous: Lexical Conventions   Contents


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{displaymath}\begin{array}{rrcll}
\textrm{Kinds} & \kappa &::=& \mathsf{T...
...\
&&& (\kappa) & \textrm{explicit precedence} \\
\end{array}\end{displaymath}

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{displaymath}\begin{array}{rrcll}
\textrm{Explicitness} & ? &::=& :: & \textrm{explicit} \\
&&& ::: & \textrm{implicit}
\end{array}\end{displaymath}

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

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

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{displaymath}\begin{array}{rrcll}
\textrm{Signatures} & S &::=& \mathsf{s...
...mathsf{of} \; \tau & \textrm{unary constructor} \\
\end{array}\end{displaymath}

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{displaymath}\begin{array}{rrcll}
\textrm{Patterns} & p &::=& \_ & \textr...
...\
&&& M.X & \textrm{projection from a module} \\
\end{array}\end{displaymath}

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

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

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{displaymath}\begin{array}{rrcll}
\textrm{Declarations} & d &::=& \mathsf...
...}(X : S) : S = M & \textrm{functor abstraction} \\
\end{array}\end{displaymath}

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.


next up previous contents
Next: Shorthands Up: Ur Syntax Previous: Lexical Conventions   Contents
2014-07-14