Mercurial > urweb

comparison doc/manual.tex @ 525:602f7536cae3

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