|
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@525
|
32 $X$ & Normal textual identifier, beginning with an uppercase letter \\
|
|
adamc@524
|
33 \end{tabular}
|
|
adamc@524
|
34 \end{center}
|
|
adamc@524
|
35
|
|
adamc@525
|
36 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.
|
|
adamc@524
|
37
|
|
adamc@524
|
38 \subsection{Core Syntax}
|
|
adamc@524
|
39
|
|
adamc@524
|
40 \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
|
41 $$\begin{array}{rrcll}
|
|
adamc@524
|
42 \textrm{Kinds} & \kappa &::=& \mt{Type} & \textrm{proper types} \\
|
|
adamc@525
|
43 &&& \mt{Unit} & \textrm{the trivial constructor} \\
|
|
adamc@525
|
44 &&& \mt{Name} & \textrm{field names} \\
|
|
adamc@525
|
45 &&& \kappa \to \kappa & \textrm{type-level functions} \\
|
|
adamc@525
|
46 &&& \{\kappa\} & \textrm{type-level records} \\
|
|
adamc@525
|
47 &&& (\kappa\times^+) & \textrm{type-level tuples} \\
|
|
adamc@525
|
48 &&& (\kappa) & \textrm{explicit precedence} \\
|
|
adamc@524
|
49 \end{array}$$
|
|
adamc@524
|
50
|
|
adamc@524
|
51 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
|
52 $$\begin{array}{rrcll}
|
|
adamc@524
|
53 \textrm{Explicitness} & ? &::=& :: & \textrm{explicit} \\
|
|
adamc@525
|
54 &&& \; ::: & \textrm{implicit}
|
|
adamc@524
|
55 \end{array}$$
|
|
adamc@524
|
56
|
|
adamc@524
|
57 \emph{Constructors} are the main class of compile-time-only data. They include proper types and are classified by kinds.
|
|
adamc@524
|
58 $$\begin{array}{rrcll}
|
|
adamc@524
|
59 \textrm{Constructors} & c, \tau &::=& (c) :: \kappa & \textrm{kind annotation} \\
|
|
adamc@525
|
60 &&& x & \textrm{constructor variable} \\
|
|
adamc@524
|
61 \\
|
|
adamc@525
|
62 &&& \tau \to \tau & \textrm{function type} \\
|
|
adamc@525
|
63 &&& x \; ? \; \kappa \to \tau & \textrm{polymorphic function type} \\
|
|
adamc@525
|
64 &&& \$ c & \textrm{record type} \\
|
|
adamc@524
|
65 \\
|
|
adamc@525
|
66 &&& c \; c & \textrm{type-level function application} \\
|
|
adamc@525
|
67 &&& \lambda x \; ? \; \kappa \Rightarrow c & \textrm{type-level function abstraction} \\
|
|
adamc@524
|
68 \\
|
|
adamc@525
|
69 &&& () & \textrm{type-level unit} \\
|
|
adamc@525
|
70 &&& \#X & \textrm{field name} \\
|
|
adamc@524
|
71 \\
|
|
adamc@525
|
72 &&& [(c = c)^*] & \textrm{known-length type-level record} \\
|
|
adamc@525
|
73 &&& c \rc c & \textrm{type-level record concatenation} \\
|
|
adamc@525
|
74 &&& \mt{fold} & \textrm{type-level record fold} \\
|
|
adamc@524
|
75 \\
|
|
adamc@525
|
76 &&& (c^+) & \textrm{type-level tuple} \\
|
|
adamc@525
|
77 &&& c.n & \textrm{type-level tuple projection ($n \in \mathbb N^+$)} \\
|
|
adamc@524
|
78 \\
|
|
adamc@525
|
79 &&& \lambda [c \sim c] \Rightarrow c & \textrm{guarded constructor} \\
|
|
adamc@524
|
80 \\
|
|
adamc@525
|
81 &&& (c) & \textrm{explicit precedence} \\
|
|
adamc@525
|
82 \end{array}$$
|
|
adamc@525
|
83
|
|
adamc@525
|
84 Modules of the module system are described by \emph{signatures}.
|
|
adamc@525
|
85 $$\begin{array}{rrcll}
|
|
adamc@525
|
86 \textrm{Signatures} & S &::=& \mt{sig} \; s^* \; \mt{end} & \textrm{constant} \\
|
|
adamc@525
|
87 &&& X & \textrm{variable} \\
|
|
adamc@525
|
88 &&& \mt{functor}(X : S) : S & \textrm{functor} \\
|
|
adamc@525
|
89 &&& S \; \mt{where} \; x = c & \textrm{concretizing an abstract constructor} \\
|
|
adamc@525
|
90 &&& M.X & \textrm{projection from a module} \\
|
|
adamc@525
|
91 \\
|
|
adamc@525
|
92 \textrm{Signature items} & s &::=& \mt{con} \; x :: \kappa & \textrm{abstract constructor} \\
|
|
adamc@525
|
93 &&& \mt{con} \; x :: \kappa = c & \textrm{concrete constructor} \\
|
|
adamc@525
|
94 &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype declaration} \\
|
|
adamc@525
|
95 &&& \mt{datatype} \; x = M.x & \textrm{algebraic datatype import} \\
|
|
adamc@525
|
96 &&& \mt{val} \; x : \tau & \textrm{value} \\
|
|
adamc@525
|
97 &&& \mt{structure} \; X : S & \textrm{sub-module} \\
|
|
adamc@525
|
98 &&& \mt{signature} \; X = S & \textrm{sub-signature} \\
|
|
adamc@525
|
99 &&& \mt{include} \; S & \textrm{signature inclusion} \\
|
|
adamc@525
|
100 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
|
|
adamc@525
|
101 &&& \mt{class} \; x & \textrm{abstract type class} \\
|
|
adamc@525
|
102 &&& \mt{class} \; x = c & \textrm{concrete type class} \\
|
|
adamc@525
|
103 \\
|
|
adamc@525
|
104 \textrm{Datatype constructors} & dc &::=& X & \textrm{nullary constructor} \\
|
|
adamc@525
|
105 &&& X \; \mt{of} \; \tau & \textrm{unary constructor} \\
|
|
adamc@524
|
106 \end{array}$$
|
|
adamc@524
|
107
|
|
adamc@524
|
108 \end{document} |
