Mercurial > urweb

comparison doc/manual.tex @ 1891:779c390382b9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Manual: add a pointer to background reading on inference rule notation
author Adam Chlipala <adam@chlipala.net>
date Sun, 17 Nov 2013 07:54:59 -0500
parents a5b08bdfa450
children afdc823563de 44f607a7f4cd
comparison
equal deleted inserted replaced
1890:abb0e95dcaa1 1891:779c390382b9
616 616
617 617
618 \section{Static Semantics} 618 \section{Static Semantics}
619 619
620 In this section, we give a declarative presentation of Ur's typing rules and related judgments. Inference is the subject of the next section; here, we assume that an oracle has filled in all wildcards with concrete values. 620 In this section, we give a declarative presentation of Ur's typing rules and related judgments. Inference is the subject of the next section; here, we assume that an oracle has filled in all wildcards with concrete values.
621
622 The notations used here are the standard ones of programming language semantics. They are probably the most effective way to convey this information. At the same time, most Ur/Web users can probably get by \emph{without} knowing the contents of this section! If you're interested in diving into the details of Ur typing but are unfamiliar with ``inference rule notation,'' I recommend the following book:
623 \begin{quote}
624 Benjamin C. Pierce, \emph{Types and Programming Languages}, MIT Press, 2002.
625 \end{quote}
621 626
622 Since there is significant mutual recursion among the judgments, we introduce them all before beginning to give rules. We use the same variety of contexts throughout this section, implicitly introducing new sorts of context entries as needed. 627 Since there is significant mutual recursion among the judgments, we introduce them all before beginning to give rules. We use the same variety of contexts throughout this section, implicitly introducing new sorts of context entries as needed.
623 \begin{itemize} 628 \begin{itemize}
624 \item $\Gamma \vdash \kappa$ expresses kind well-formedness. 629 \item $\Gamma \vdash \kappa$ expresses kind well-formedness.
625 \item $\Gamma \vdash c :: \kappa$ assigns a kind to a constructor in a context. 630 \item $\Gamma \vdash c :: \kappa$ assigns a kind to a constructor in a context.