summaryrefslogtreecommitdiff
path: root/doc/manual.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/manual.tex')
-rw-r--r--doc/manual.tex85
1 files changed, 85 insertions, 0 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
new file mode 100644
index 00000000..8517206a
--- /dev/null
+++ b/doc/manual.tex
@@ -0,0 +1,85 @@
+\documentclass{article}
+\usepackage{fullpage,amsmath,amssymb,proof}
+
+\newcommand{\cd}[1]{\texttt{#1}}
+\newcommand{\mt}[1]{\mathsf{#1}}
+
+\newcommand{\rc}{+ \hspace{-.075in} + \;}
+
+\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{=>} \\
+ $\rc$ & \cd{++} \\
+ \\
+ $x$ & Normal textual identifier, not beginning with an uppercase letter \\
+ $\alpha$ & Normal textual identifier, not beginning with an uppercase letter \\
+ $f$ & Normal textual identifier, beginning with an uppercase letter \\
+ \end{tabular}
+\end{center}
+
+We often write syntax like $N, \cdots, N$ to stand for the non-terminal $N$ repeated 0 or more times. That is, the $\cdots$ symbol is not translated literally to ASCII.
+
+\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} \\
+ &&& \mid \mt{Unit} & \textrm{the trivial constructor} \\
+ &&& \mid \mt{Name} & \textrm{field names} \\
+ &&& \mid \kappa \to \kappa & \textrm{type-level functions} \\
+ &&& \mid \{\kappa\} & \textrm{type-level records} \\
+ &&& \mid (\kappa \times \cdots \times \kappa) & \textrm{type-level tuples} \\
+ &&& \mid (\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} \\
+ &&& \mid \; ::: & \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} \\
+ &&& \mid \alpha & \textrm{constructor variable} \\
+ \\
+ &&& \mid \tau \to \tau & \textrm{function type} \\
+ &&& \mid \alpha \; ? \; \kappa \to \tau & \textrm{polymorphic function type} \\
+ &&& \mid \$ c & \textrm{record type} \\
+ \\
+ &&& \mid c \; c & \textrm{type-level function application} \\
+ &&& \mid \lambda \alpha \; ? \; \kappa \Rightarrow c & \textrm{type-level function abstraction} \\
+ \\
+ &&& \mid () & \textrm{type-level unit} \\
+ &&& \mid \#f & \textrm{field name} \\
+ \\
+ &&& \mid [c = c, \cdots, c = c] & \textrm{known-length type-level record} \\
+ &&& \mid c \rc c & \textrm{type-level record concatenation} \\
+ &&& \mid \mt{fold} & \textrm{type-level record fold} \\
+ \\
+ &&& \mid (c, \cdots, c) & \textrm{type-level tuple} \\
+ &&& \mid c.n & \textrm{type-level tuple projection ($n \in \mathbb N^+$)} \\
+ \\
+ &&& \mid \lambda [c \sim c] \Rightarrow c & \textrm{guarded constructor} \\
+ \\
+ &&& \mid (c) & \textrm{explicit precedence} \\
+\end{array}$$
+
+\end{document} \ No newline at end of file