Mercurial > urweb
comparison doc/manual.tex @ 536:e32d0f6a1e15
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} |