\documentclass{article}
\usepackage{fullpage,amsmath,amssymb,proof}

\newcommand{\cd}[1]{\texttt{#1}}
\newcommand{\mt}[1]{\mathsf{#1}}

\newcommand{\rc}{+ \hspace{-.075in} + \;}
\newcommand{\rcut}{\; \texttt{--} \;}
\newcommand{\rcutM}{\; \texttt{---} \;}

\begin{document}

\title{The Ur/Web Manual}
\author{Adam Chlipala}

\maketitle

\section{Syntax}

\subsection{Lexical Conventions}

We give the Ur language definition in \LaTeX $\;$ math mode, since that is prettier than monospaced ASCII.  The corresponding ASCII syntax can be read off directly.  Here is the key for mapping math symbols to ASCII character sequences.

\begin{center}
  \begin{tabular}{rl}
    \textbf{\LaTeX} & \textbf{ASCII} \\
    $\to$ & \cd{->} \\
    $\times$ & \cd{*} \\
    $\lambda$ & \cd{fn} \\
    $\Rightarrow$ & \cd{=>} \\
    & \cd{---} \\
    \\
    $x$ & Normal textual identifier, not beginning with an uppercase letter \\
    $X$ & Normal textual identifier, beginning with an uppercase letter \\
  \end{tabular}
\end{center}

We often write syntax like $e^*$ to indicate zero or more copies of $e$, $e^+$ to indicate one or more copies, and $e,^*$ and $e,^+$ to indicate multiple copies separated by commas.  Another separator may be used in place of a comma.  The $e$ term may be surrounded by parentheses to indicate grouping; those parentheses should not be included in the actual ASCII.

We write $\ell$ for literals of the primitive types, for the most part following C conventions.  There are $\mt{int}$, $\mt{float}$, and $\mt{string}$ literals.

This version of the manual doesn't include operator precedences; see \texttt{src/urweb.grm} for that.

\subsection{Core Syntax}

\emph{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 &::=& \mt{Type} & \textrm{proper types} \\
  &&& \mt{Unit} & \textrm{the trivial constructor} \\
  &&& \mt{Name} & \textrm{field names} \\
  &&& \kappa \to \kappa & \textrm{type-level functions} \\
  &&& \{\kappa\} & \textrm{type-level records} \\
  &&& (\kappa\times^+) & \textrm{type-level tuples} \\
  &&& \_ & \textrm{wildcard} \\
  &&& (\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}$$

\emph{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 &::=& (c) :: \kappa & \textrm{kind annotation} \\
  &&& x & \textrm{constructor variable} \\
  \\
  &&& \tau \to \tau & \textrm{function type} \\
  &&& x \; ? \; \kappa \to \tau & \textrm{polymorphic function type} \\
  &&& \$ c & \textrm{record type} \\
  \\
  &&& c \; c & \textrm{type-level function application} \\
  &&& \lambda x \; ? \; \kappa \Rightarrow c & \textrm{type-level function abstraction} \\
  \\
  &&& () & \textrm{type-level unit} \\
  &&& \#X & \textrm{field name} \\
  \\
  &&& [(c = c)^*] & \textrm{known-length type-level record} \\
  &&& c \rc c & \textrm{type-level record concatenation} \\
  &&& \mt{fold} & \textrm{type-level record fold} \\
  \\
  &&& (c^+) & \textrm{type-level tuple} \\
  &&& c.n & \textrm{type-level tuple projection ($n \in \mathbb N^+$)} \\
  \\
  &&& \lambda [c \sim c] \Rightarrow c & \textrm{guarded constructor} \\
  \\
  &&& \_ & \textrm{wildcard} \\
  &&& (c) & \textrm{explicit precedence} \\
\end{array}$$

Modules of the module system are described by \emph{signatures}.
$$\begin{array}{rrcll}
  \textrm{Signatures} & S &::=& \mt{sig} \; s^* \; \mt{end} & \textrm{constant} \\
  &&& X & \textrm{variable} \\
  &&& \mt{functor}(X : S) : S & \textrm{functor} \\
  &&& S \; \mt{where} \; x = c & \textrm{concretizing an abstract constructor} \\
  &&& M.X & \textrm{projection from a module} \\
  \\
  \textrm{Signature items} & s &::=& \mt{con} \; x :: \kappa & \textrm{abstract constructor} \\
  &&& \mt{con} \; x :: \kappa = c & \textrm{concrete constructor} \\
  &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
  &&& \mt{datatype} \; x = M.x & \textrm{algebraic datatype import} \\
  &&& \mt{val} \; x : \tau & \textrm{value} \\
  &&& \mt{structure} \; X : S & \textrm{sub-module} \\
  &&& \mt{signature} \; X = S & \textrm{sub-signature} \\
  &&& \mt{include} \; S & \textrm{signature inclusion} \\
  &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
  &&& \mt{class} \; x & \textrm{abstract type class} \\
  &&& \mt{class} \; x = c & \textrm{concrete type class} \\
  \\
  \textrm{Datatype constructors} & dc &::=& X & \textrm{nullary constructor} \\
  &&& X \; \mt{of} \; \tau & \textrm{unary constructor} \\
\end{array}$$

\emph{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 &::=& \_ & \textrm{wildcard} \\
  &&& x & \textrm{variable} \\
  &&& \ell & \textrm{constant} \\
  &&& \hat{X} & \textrm{nullary constructor} \\
  &&& \hat{X} \; p & \textrm{unary constructor} \\
  &&& \{(x = p,)^*\} & \textrm{rigid record pattern} \\
  &&& \{(x = p,)^+, \ldots\} & \textrm{flexible record pattern} \\
  &&& (p) & \textrm{explicit precedence} \\
  \\
  \textrm{Qualified capitalized variable} & \hat{X} &::=& X & \textrm{not from a module} \\
  &&& M.X & \textrm{projection from a module} \\
\end{array}$$

\emph{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 & \textrm{type annotation} \\
  &&& x & \textrm{variable} \\
  &&& \ell & \textrm{constant} \\
  \\
  &&& e \; e & \textrm{function application} \\
  &&& \lambda x : \tau \Rightarrow e & \textrm{function abstraction} \\
  &&& e [c] & \textrm{polymorphic function application} \\
  &&& \lambda x \; ? \; \kappa \Rightarrow e & \textrm{polymorphic function abstraction} \\
  \\
  &&& \{(c = e,)^*\} & \textrm{known-length record} \\
  &&& e.c & \textrm{record field projection} \\
  &&& e \rc e & \textrm{record concatenation} \\
  &&& e \rcut c & \textrm{removal of a single record field} \\
  &&& e \rcutM c & \textrm{removal of multiple record fields} \\
  &&& \mt{fold} & \textrm{fold over fields of a type-level record} \\
  \\
  &&& \mt{let} \; ed^* \; \mt{in} \; e \; \mt{end} & \textrm{local definitions} \\
  \\
  &&& \mt{case} \; e \; \mt{of} \; (p \Rightarrow e|)^+ & \textrm{pattern matching} \\
  \\
  &&& \lambda [c \sim c] \Rightarrow e & \textrm{guarded expression} \\
  \\
  &&& \_ & \textrm{wildcard} \\
  &&& (e) & \textrm{explicit precedence} \\
  \\
  \textrm{Local declarations} & ed &::=& \cd{val} \; x : \tau = e & \textrm{non-recursive value} \\
  &&& \cd{val} \; \cd{rec} \; (x : \tau = e \; \cd{and})^+ & \textrm{mutually-recursive values} \\
\end{array}$$

\emph{Declarations} primarily bring new symbols into context.
$$\begin{array}{rrcll}
  \textrm{Declarations} & d &::=& \mt{con} \; x :: \kappa = c & \textrm{constructor synonym} \\
  &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
  &&& \mt{datatype} \; x = M.x & \textrm{algebraic datatype import} \\
  &&& \mt{val} \; x : \tau = e & \textrm{value} \\
  &&& \mt{val} \; \cd{rec} \; (x : \tau = e \; \mt{and})^+ & \textrm{mutually-recursive values} \\
  &&& \mt{structure} \; X : S = M & \textrm{module definition} \\
  &&& \mt{signature} \; X = S & \textrm{signature definition} \\
  &&& \mt{open} \; M & \textrm{module inclusion} \\
  &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
  &&& \mt{open} \; \mt{constraints} \; M & \textrm{inclusion of just the constraints from a module} \\
  &&& \mt{table} \; x : c & \textrm{SQL table} \\
  &&& \mt{sequence} \; x & \textrm{SQL sequence} \\
  &&& \mt{class} \; x = c & \textrm{concrete type class} \\
  &&& \mt{cookie} \; x : c & \textrm{HTTP cookie} \\
  \\
  \textrm{Modules} & M &::=& \mt{struct} \; d^* \; \mt{end} & \mt{constant} \\
  &&& X & \mt{variable} \\
  &&& M.X & \mt{projection} \\
  &&& M(M) & \mt{functor application} \\
  &&& \mt{functor}(X : S) : S = M & \mt{functor abstraction} \\
\end{array}$$

There are two kinds of Ur files.  A file named $M\texttt{.ur}$ is an \emph{implementation file}, and it should contain a sequence of declarations $d^*$.  A file named $M\texttt{.urs}$ is an \emph{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 $\mt{structure} \; M : \mt{sig} \; s^* \; \mt{end} = \mt{struct} \; d^* \; \mt{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.

\end{document}