Mercurial > urweb

comparison doc/manual.tex @ 536:e32d0f6a1e15

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Signature compatibility
author Adam Chlipala <adamc@hcoop.net>
date Sat, 29 Nov 2008 12:58:58 -0500
parents b742bf4e377b
children a4a7cd341a1b
comparison
equal deleted inserted replaced
535:b742bf4e377b 536:e32d0f6a1e15
243 \item $\Gamma \vdash c \hookrightarrow C$ proves that record constructor $c$ decomposes into set $C$ of field names and record constructors. 243 \item $\Gamma \vdash c \hookrightarrow C$ proves that record constructor $c$ decomposes into set $C$ of field names and record constructors.
244 \item $\Gamma \vdash c \equiv c$ proves the computational equivalence of two constructors. This is often called a \emph{definitional equality} in the world of type theory. 244 \item $\Gamma \vdash c \equiv c$ proves the computational equivalence of two constructors. This is often called a \emph{definitional equality} in the world of type theory.
245 \item $\Gamma \vdash e : \tau$ is a standard typing judgment. 245 \item $\Gamma \vdash e : \tau$ is a standard typing judgment.
246 \item $\Gamma \vdash p \leadsto \Gamma; \tau$ combines typing of patterns with calculation of which new variables they bind. 246 \item $\Gamma \vdash p \leadsto \Gamma; \tau$ combines typing of patterns with calculation of which new variables they bind.
247 \item $\Gamma \vdash d \leadsto \Gamma$ expresses how a declaration modifies a context. We overload this judgment to apply to sequences of declarations. 247 \item $\Gamma \vdash d \leadsto \Gamma$ expresses how a declaration modifies a context. We overload this judgment to apply to sequences of declarations.
248 \item $\Gamma \vdash S$ is the signature validity judgment. 248 \item $\Gamma \vdash S \leq S$ is the signature compatibility judgment. We write $\Gamma \vdash S$ as shorthand for $\Gamma \vdash S \leq S$.
249 \item $\Gamma \vdash S \leq S$ is the signature compatibility judgment.
250 \item $\Gamma \vdash M : S$ is the module signature checking judgment. 249 \item $\Gamma \vdash M : S$ is the module signature checking judgment.
251 \item $\mt{proj}(M, S, V)$ is a partial function for projecting a signature item from a signature $S$, given the module $M$ that we project from. $V$ may be $\mt{con} \; x$, $\mt{datatype} \; x$, $\mt{val} \; x$, $\mt{signature} \; X$, or $\mt{structure} \; X$. The parameter $M$ is needed because the projected signature item may refer to other items of $S$. 250 \item $\mt{proj}(M, S, V)$ is a partial function for projecting a signature item from a signature $S$, given the module $M$ that we project from. $V$ may be $\mt{con} \; x$, $\mt{datatype} \; x$, $\mt{val} \; x$, $\mt{signature} \; X$, or $\mt{structure} \; X$. The parameter $M$ is needed because the projected signature item may refer to other items of $S$.
252 \end{itemize} 251 \end{itemize}
253 252
254 \subsection{Kinding} 253 \subsection{Kinding}
598 } 597 }
599 \quad \infer{\overline{y}; x; \Gamma \vdash X \; \mt{of} \; \tau \mid \overline{dc} \leadsto \Gamma', X : \overline{y ::: \mt{Type}} \to \tau \to x \; \overline{y}}{ 598 \quad \infer{\overline{y}; x; \Gamma \vdash X \; \mt{of} \; \tau \mid \overline{dc} \leadsto \Gamma', X : \overline{y ::: \mt{Type}} \to \tau \to x \; \overline{y}}{
600 \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma' 599 \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'
601 }$$ 600 }$$
602 601
602 \subsection{Signature Compatibility}
603
604 $$\infer{\Gamma \vdash S \equiv S}{}
605 \quad \infer{\Gamma \vdash S_1 \equiv S_2}{
606 \Gamma \vdash S_2 \equiv S_1
607 }
608 \quad \infer{\Gamma \vdash X \equiv S}{
609 X = S \in \Gamma
610 }
611 \quad \infer{\Gamma \vdash M.X \equiv S}{
612 \Gamma \vdash M : S'
613 & \mt{proj}(M, S', \mt{signature} \; X) = S
614 }$$
615
616 $$\infer{\Gamma \vdash S \; \mt{where} \; \mt{con} \; x = c \equiv \mt{sig} \; \overline{s^1} \; \mt{con} \; x :: \kappa = c \; \overline{s_2} \; \mt{end}}{
617 \Gamma \vdash S \equiv \mt{sig} \; \overline{s^1} \; \mt{con} \; x :: \kappa \; \overline{s_2} \; \mt{end}
618 & \Gamma \vdash c :: \kappa
619 }$$
620
621 $$\infer{\Gamma \vdash S_1 \leq S_2}{
622 \Gamma \vdash S_1 \equiv S_2
623 }
624 \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \mt{end}}{}
625 \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s^1} \; s \; \overline{s^2} \; \mt{end} \leq \mt{sig} \; s' \; \overline{s} \; \mt{end}}{
626 \Gamma \vdash s \leq s'; \Gamma'
627 & \Gamma' \vdash \mt{sig} \; \overline{s^1} \; s \; \overline{s^2} \; \mt{end} \leq \mt{sig} \; \overline{s} \; \mt{end}
628 }$$
629
630 $$\infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 \leq \mt{functor} (X : S'_1) : S'_2}{
631 \Gamma \vdash S'_1 \leq S_1
632 & \Gamma, X : S'_1 \vdash S_2 \leq S'_2
633 }$$
634
603 \end{document} 635 \end{document}