|
adamc@524
|
1 \documentclass{article}
|
|
adamc@524
|
2 \usepackage{fullpage,amsmath,amssymb,proof}
|
|
adamc@524
|
3
|
|
adamc@524
|
4 \newcommand{\cd}[1]{\texttt{#1}}
|
|
adamc@524
|
5 \newcommand{\mt}[1]{\mathsf{#1}}
|
|
adamc@524
|
6
|
|
adamc@524
|
7 \newcommand{\rc}{+ \hspace{-.075in} + \;}
|
|
adamc@524
|
8
|
|
adamc@524
|
9 \begin{document}
|
|
adamc@524
|
10
|
|
adamc@524
|
11 \title{The Ur/Web Manual}
|
|
adamc@524
|
12 \author{Adam Chlipala}
|
|
adamc@524
|
13
|
|
adamc@524
|
14 \maketitle
|
|
adamc@524
|
15
|
|
adamc@524
|
16 \section{Syntax}
|
|
adamc@524
|
17
|
|
adamc@524
|
18 \subsection{Lexical Conventions}
|
|
adamc@524
|
19
|
|
adamc@524
|
20 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.
|
|
adamc@524
|
21
|
|
adamc@524
|
22 \begin{center}
|
|
adamc@524
|
23 \begin{tabular}{rl}
|
|
adamc@524
|
24 \textbf{\LaTeX} & \textbf{ASCII} \\
|
|
adamc@524
|
25 $\to$ & \cd{->} \\
|
|
adamc@524
|
26 $\times$ & \cd{*} \\
|
|
adamc@524
|
27 $\lambda$ & \cd{fn} \\
|
|
adamc@524
|
28 $\Rightarrow$ & \cd{=>} \\
|
|
adamc@524
|
29 $\rc$ & \cd{++} \\
|
|
adamc@524
|
30 \\
|
|
adamc@524
|
31 $x$ & Normal textual identifier, not beginning with an uppercase letter \\
|
|
adamc@524
|
32 $\alpha$ & Normal textual identifier, not beginning with an uppercase letter \\
|
|
adamc@524
|
33 $f$ & Normal textual identifier, beginning with an uppercase letter \\
|
|
adamc@524
|
34 \end{tabular}
|
|
adamc@524
|
35 \end{center}
|
|
adamc@524
|
36
|
|
adamc@524
|
37 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.
|
|
adamc@524
|
38
|
|
adamc@524
|
39 \subsection{Core Syntax}
|
|
adamc@524
|
40
|
|
adamc@524
|
41 \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.
|
|
adamc@524
|
42 $$\begin{array}{rrcll}
|
|
adamc@524
|
43 \textrm{Kinds} & \kappa &::=& \mt{Type} & \textrm{proper types} \\
|
|
adamc@524
|
44 &&& \mid \mt{Unit} & \textrm{the trivial constructor} \\
|
|
adamc@524
|
45 &&& \mid \mt{Name} & \textrm{field names} \\
|
|
adamc@524
|
46 &&& \mid \kappa \to \kappa & \textrm{type-level functions} \\
|
|
adamc@524
|
47 &&& \mid \{\kappa\} & \textrm{type-level records} \\
|
|
adamc@524
|
48 &&& \mid (\kappa \times \cdots \times \kappa) & \textrm{type-level tuples} \\
|
|
adamc@524
|
49 &&& \mid (\kappa) & \textrm{explicit precedence} \\
|
|
adamc@524
|
50 \end{array}$$
|
|
adamc@524
|
51
|
|
adamc@524
|
52 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.
|
|
adamc@524
|
53 $$\begin{array}{rrcll}
|
|
adamc@524
|
54 \textrm{Explicitness} & ? &::=& :: & \textrm{explicit} \\
|
|
adamc@524
|
55 &&& \mid \; ::: & \textrm{implicit}
|
|
adamc@524
|
56 \end{array}$$
|
|
adamc@524
|
57
|
|
adamc@524
|
58 \emph{Constructors} are the main class of compile-time-only data. They include proper types and are classified by kinds.
|
|
adamc@524
|
59 $$\begin{array}{rrcll}
|
|
adamc@524
|
60 \textrm{Constructors} & c, \tau &::=& (c) :: \kappa & \textrm{kind annotation} \\
|
|
adamc@524
|
61 &&& \mid \alpha & \textrm{constructor variable} \\
|
|
adamc@524
|
62 \\
|
|
adamc@524
|
63 &&& \mid \tau \to \tau & \textrm{function type} \\
|
|
adamc@524
|
64 &&& \mid \alpha \; ? \; \kappa \to \tau & \textrm{polymorphic function type} \\
|
|
adamc@524
|
65 &&& \mid \$ c & \textrm{record type} \\
|
|
adamc@524
|
66 \\
|
|
adamc@524
|
67 &&& \mid c \; c & \textrm{type-level function application} \\
|
|
adamc@524
|
68 &&& \mid \lambda \alpha \; ? \; \kappa \Rightarrow c & \textrm{type-level function abstraction} \\
|
|
adamc@524
|
69 \\
|
|
adamc@524
|
70 &&& \mid () & \textrm{type-level unit} \\
|
|
adamc@524
|
71 &&& \mid \#f & \textrm{field name} \\
|
|
adamc@524
|
72 \\
|
|
adamc@524
|
73 &&& \mid [c = c, \cdots, c = c] & \textrm{known-length type-level record} \\
|
|
adamc@524
|
74 &&& \mid c \rc c & \textrm{type-level record concatenation} \\
|
|
adamc@524
|
75 &&& \mid \mt{fold} & \textrm{type-level record fold} \\
|
|
adamc@524
|
76 \\
|
|
adamc@524
|
77 &&& \mid (c, \cdots, c) & \textrm{type-level tuple} \\
|
|
adamc@524
|
78 &&& \mid c.n & \textrm{type-level tuple projection ($n \in \mathbb N^+$)} \\
|
|
adamc@524
|
79 \\
|
|
adamc@524
|
80 &&& \mid \lambda [c \sim c] \Rightarrow c & \textrm{guarded constructor} \\
|
|
adamc@524
|
81 \\
|
|
adamc@524
|
82 &&& \mid (c) & \textrm{explicit precedence} \\
|
|
adamc@524
|
83 \end{array}$$
|
|
adamc@524
|
84
|
|
adamc@524
|
85 \end{document} |
