Mercurial > urweb

annotate doc/manual.tex @ 526:f87fd1549c33

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Patterns
author Adam Chlipala <adamc@hcoop.net>
date Thu, 27 Nov 2008 15:06:29 -0500
parents 602f7536cae3
children 74dd4dca9e32
rev   line source
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@526 38 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.
adamc@526 39
adamc@524 40 \subsection{Core Syntax}
adamc@524 41
adamc@524 42 \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 43 $$\begin{array}{rrcll}
adamc@524 44 \textrm{Kinds} & \kappa &::=& \mt{Type} & \textrm{proper types} \\
adamc@525 45 &&& \mt{Unit} & \textrm{the trivial constructor} \\
adamc@525 46 &&& \mt{Name} & \textrm{field names} \\
adamc@525 47 &&& \kappa \to \kappa & \textrm{type-level functions} \\
adamc@525 48 &&& \{\kappa\} & \textrm{type-level records} \\
adamc@525 49 &&& (\kappa\times^+) & \textrm{type-level tuples} \\
adamc@525 50 &&& (\kappa) & \textrm{explicit precedence} \\
adamc@524 51 \end{array}$$
adamc@524 52
adamc@524 53 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 54 $$\begin{array}{rrcll}
adamc@524 55 \textrm{Explicitness} & ? &::=& :: & \textrm{explicit} \\
adamc@525 56 &&& \; ::: & \textrm{implicit}
adamc@524 57 \end{array}$$
adamc@524 58
adamc@524 59 \emph{Constructors} are the main class of compile-time-only data. They include proper types and are classified by kinds.
adamc@524 60 $$\begin{array}{rrcll}
adamc@524 61 \textrm{Constructors} & c, \tau &::=& (c) :: \kappa & \textrm{kind annotation} \\
adamc@525 62 &&& x & \textrm{constructor variable} \\
adamc@524 63 \\
adamc@525 64 &&& \tau \to \tau & \textrm{function type} \\
adamc@525 65 &&& x \; ? \; \kappa \to \tau & \textrm{polymorphic function type} \\
adamc@525 66 &&& \$ c & \textrm{record type} \\
adamc@524 67 \\
adamc@525 68 &&& c \; c & \textrm{type-level function application} \\
adamc@525 69 &&& \lambda x \; ? \; \kappa \Rightarrow c & \textrm{type-level function abstraction} \\
adamc@524 70 \\
adamc@525 71 &&& () & \textrm{type-level unit} \\
adamc@525 72 &&& \#X & \textrm{field name} \\
adamc@524 73 \\
adamc@525 74 &&& [(c = c)^*] & \textrm{known-length type-level record} \\
adamc@525 75 &&& c \rc c & \textrm{type-level record concatenation} \\
adamc@525 76 &&& \mt{fold} & \textrm{type-level record fold} \\
adamc@524 77 \\
adamc@525 78 &&& (c^+) & \textrm{type-level tuple} \\
adamc@525 79 &&& c.n & \textrm{type-level tuple projection ($n \in \mathbb N^+$)} \\
adamc@524 80 \\
adamc@525 81 &&& \lambda [c \sim c] \Rightarrow c & \textrm{guarded constructor} \\
adamc@524 82 \\
adamc@525 83 &&& (c) & \textrm{explicit precedence} \\
adamc@525 84 \end{array}$$
adamc@525 85
adamc@525 86 Modules of the module system are described by \emph{signatures}.
adamc@525 87 $$\begin{array}{rrcll}
adamc@525 88 \textrm{Signatures} & S &::=& \mt{sig} \; s^* \; \mt{end} & \textrm{constant} \\
adamc@525 89 &&& X & \textrm{variable} \\
adamc@525 90 &&& \mt{functor}(X : S) : S & \textrm{functor} \\
adamc@525 91 &&& S \; \mt{where} \; x = c & \textrm{concretizing an abstract constructor} \\
adamc@525 92 &&& M.X & \textrm{projection from a module} \\
adamc@525 93 \\
adamc@525 94 \textrm{Signature items} & s &::=& \mt{con} \; x :: \kappa & \textrm{abstract constructor} \\
adamc@525 95 &&& \mt{con} \; x :: \kappa = c & \textrm{concrete constructor} \\
adamc@525 96 &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype declaration} \\
adamc@525 97 &&& \mt{datatype} \; x = M.x & \textrm{algebraic datatype import} \\
adamc@525 98 &&& \mt{val} \; x : \tau & \textrm{value} \\
adamc@525 99 &&& \mt{structure} \; X : S & \textrm{sub-module} \\
adamc@525 100 &&& \mt{signature} \; X = S & \textrm{sub-signature} \\
adamc@525 101 &&& \mt{include} \; S & \textrm{signature inclusion} \\
adamc@525 102 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
adamc@525 103 &&& \mt{class} \; x & \textrm{abstract type class} \\
adamc@525 104 &&& \mt{class} \; x = c & \textrm{concrete type class} \\
adamc@525 105 \\
adamc@525 106 \textrm{Datatype constructors} & dc &::=& X & \textrm{nullary constructor} \\
adamc@525 107 &&& X \; \mt{of} \; \tau & \textrm{unary constructor} \\
adamc@524 108 \end{array}$$
adamc@524 109
adamc@526 110 \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.
adamc@526 111 $$\begin{array}{rrcll}
adamc@526 112 \textrm{Patterns} & p &::=& \_ & \textrm{wildcard} \\
adamc@526 113 &&& x & \textrm{variable} \\
adamc@526 114 &&& \ell & \textrm{constant} \\
adamc@526 115 &&& \hat{X} & \textrm{nullary constructor} \\
adamc@526 116 &&& \hat{X} \; p & \textrm{unary constructor} \\
adamc@526 117 &&& \{(x = p,)^*\} & \textrm{rigid record pattern} \\
adamc@526 118 &&& \{(x = p,)^+, \ldots\} & \textrm{flexible record pattern} \\
adamc@526 119 \\
adamc@526 120 \textrm{Qualified capitalized variable} & \hat{X} &::=& X & \textrm{not from a module} \\
adamc@526 121 &&& M.X & \textrm{projection from a module} \\
adamc@526 122 \end{array}$$
adamc@526 123
adamc@524 124 \end{document}