# HG changeset patch # User Adam Chlipala # Date 1227984653 18000 # Node ID a4a7cd341a1b509b82a984a96006be85496e1b7a # Parent e32d0f6a1e153ad0c6014232ad09941babba34f8 Signature compatibility diff -r e32d0f6a1e15 -r a4a7cd341a1b doc/manual.tex --- a/doc/manual.tex Sat Nov 29 12:58:58 2008 -0500 +++ b/doc/manual.tex Sat Nov 29 13:50:53 2008 -0500 @@ -244,10 +244,11 @@ \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. \item $\Gamma \vdash e : \tau$ is a standard typing judgment. \item $\Gamma \vdash p \leadsto \Gamma; \tau$ combines typing of patterns with calculation of which new variables they bind. -\item $\Gamma \vdash d \leadsto \Gamma$ expresses how a declaration modifies a context. We overload this judgment to apply to sequences of declarations. +\item $\Gamma \vdash d \leadsto \Gamma$ expresses how a declaration modifies a context. We overload this judgment to apply to sequences of declarations, as well as to signature items and sequences of signature items. +\item $\Gamma \vdash S \equiv S$ is the signature equivalence judgment. \item $\Gamma \vdash S \leq S$ is the signature compatibility judgment. We write $\Gamma \vdash S$ as shorthand for $\Gamma \vdash S \leq S$. \item $\Gamma \vdash M : S$ is the module signature checking judgment. -\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$. +\item $\mt{proj}(M, \overline{s}, V)$ is a partial function for projecting a signature item from $\overline{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 from $\overline{s}$. \end{itemize} \subsection{Kinding} @@ -263,12 +264,12 @@ }$$ $$\infer{\Gamma \vdash M.x :: \kappa}{ - \Gamma \vdash M : S - & \mt{proj}(M, S, \mt{con} \; x) = \kappa + \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} + & \mt{proj}(M, \overline{s}, \mt{con} \; x) = \kappa } \quad \infer{\Gamma \vdash M.x :: \kappa}{ - \Gamma \vdash M : S - & \mt{proj}(M, S, \mt{con} \; x) = (\kappa, c) + \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} + & \mt{proj}(M, \overline{s}, \mt{con} \; x) = (\kappa, c) }$$ $$\infer{\Gamma \vdash \tau_1 \to \tau_2 :: \mt{Type}}{ @@ -374,8 +375,8 @@ x :: \kappa = c \in \Gamma } \quad \infer{\Gamma \vdash M.x \equiv c}{ - \Gamma \vdash M : S - & \mt{proj}(M, S, \mt{con} \; x) = (\kappa, c) + \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} + & \mt{proj}(M, \overline{s}, \mt{con} \; x) = (\kappa, c) } \quad \infer{\Gamma \vdash (\overline c).i \equiv c_i}{}$$ @@ -417,15 +418,15 @@ x : \tau \in \Gamma } \quad \infer{\Gamma \vdash M.x : \mathcal I(\tau)}{ - \Gamma \vdash M : S - & \mt{proj}(M, S, \mt{val} \; x) = \tau + \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} + & \mt{proj}(M, \overline{s}, \mt{val} \; x) = \tau } \quad \infer{\Gamma \vdash X : \mathcal I(\tau)}{ X : \tau \in \Gamma } \quad \infer{\Gamma \vdash M.X : \mathcal I(\tau)}{ - \Gamma \vdash M : S - & \mt{proj}(M, S, \mt{val} \; X) = \tau + \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} + & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \tau }$$ $$\infer{\Gamma \vdash e_1 \; e_2 : \tau_2}{ @@ -502,14 +503,14 @@ }$$ $$\infer{\Gamma \vdash M.X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{ - \Gamma \vdash M : S - & \mt{proj}(M, S, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau + \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} + & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau & \textrm{$\tau$ not a function type} }$$ $$\infer{\Gamma \vdash M.X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{ - \Gamma \vdash M : S - & \mt{proj}(M, S, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau'' \to \tau + \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} + & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau'' \to \tau & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau'' }$$ @@ -528,7 +529,9 @@ This is the first judgment where we deal with type classes, for the $\mt{class}$ declaration form. We will omit their special handling in this formal specification. In the compiler, a set of available type classes and their instances is maintained, and these instances are used to fill in expression wildcards. -We presuppose the existence of a function $\mathcal O$, where $\mathcal(M, S)$ implements the $\mt{open}$ declaration by producing a context with the appropriate entry for each available component of module $M$ with signature $S$. Where possible, $\mathcal O$ uses ``transparent'' entries (e.g., an abstract type $M.x$ is mapped to $x :: \mt{Type} = M.x$), so that the relationship with $M$ is maintained. A related function $\mathcal O_c$ builds a context containing the disjointness constraints found in $S$. +We presuppose the existence of a function $\mathcal O$, where $\mathcal(M, \overline{s})$ implements the $\mt{open}$ declaration by producing a context with the appropriate entry for each available component of module $M$ with signature items $\overline{s}$. Where possible, $\mathcal O$ uses ``transparent'' entries (e.g., an abstract type $M.x$ is mapped to $x :: \mt{Type} = M.x$), so that the relationship with $M$ is maintained. A related function $\mathcal O_c$ builds a context containing the disjointness constraints found in $S$. + +We write $\kappa_1^n \to \kappa$ as a shorthand, where $\kappa_1^0 \to \kappa = \kappa$ and $\kappa_1^{n+1} \to \kappa_2 = \kappa_1 \to (\kappa_1^n \to \kappa_2)$. We write $\mt{len}(\overline{y})$ for the length of vector $\overline{y}$ of variables. $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{} \quad \infer{\Gamma \vdash d, \overline{d} \leadsto \Gamma''}{ @@ -544,8 +547,8 @@ }$$ $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leadsto \Gamma'}{ - \Gamma \vdash M : S - & \mt{proj}(M, S, \mt{datatype} \; z) = (\overline{y}, \overline{dc}) + \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} + & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc}) & \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} = M.z \vdash \overline{dc} \leadsto \Gamma' }$$ @@ -561,12 +564,12 @@ $$\infer{\Gamma \vdash \mt{structure} \; X : S = M \leadsto \Gamma, X : S}{ \Gamma \vdash M : S } -\quad \infer{\Gamma \vdash \mt{siganture} \; X = S \leadsto \Gamma, X = S}{ +\quad \infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{ \Gamma \vdash S }$$ -$$\infer{\Gamma \vdash \mt{open} \; M \leadsto \Gamma, \mathcal O(M, S)}{ - \Gamma \vdash M : S +$$\infer{\Gamma \vdash \mt{open} \; M \leadsto \Gamma, \mathcal O(M, \overline{s})}{ + \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} }$$ $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma}{ @@ -574,8 +577,8 @@ & \Gamma \vdash c_2 :: \{\kappa\} & \Gamma \vdash c_1 \sim c_2 } -\quad \infer{\Gamma \vdash \mt{open} \; \mt{constraints} \; M \leadsto \Gamma, \mathcal O_c(M, S)}{ - \Gamma \vdash M : S +\quad \infer{\Gamma \vdash \mt{open} \; \mt{constraints} \; M \leadsto \Gamma, \mathcal O_c(M, \overline{s})}{ + \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} }$$ $$\infer{\Gamma \vdash \mt{table} \; x : c \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_table} \; c}{ @@ -599,8 +602,62 @@ \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma' }$$ +\subsection{Signature Item Typing} + +We appeal to a signature item analogue of the $\mathcal O$ function from the last subsection. + +$$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{} +\quad \infer{\Gamma \vdash s, \overline{s} \leadsto \Gamma''}{ + \Gamma \vdash s \leadsto \Gamma' + & \Gamma' \vdash \overline{s} \leadsto \Gamma'' +}$$ + +$$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leadsto \Gamma, x :: \kappa}{} +\quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{ + \Gamma \vdash c :: \kappa +} +\quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leadsto \Gamma'}{ + \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} \vdash \overline{dc} \leadsto \Gamma' +}$$ + +$$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leadsto \Gamma'}{ + \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} + & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc}) + & \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} = M.z \vdash \overline{dc} \leadsto \Gamma' +}$$ + +$$\infer{\Gamma \vdash \mt{val} \; x : \tau \leadsto \Gamma, x : \tau}{ + \Gamma \vdash \tau :: \mt{Type} +}$$ + +$$\infer{\Gamma \vdash \mt{structure} \; X : S \leadsto \Gamma, X : S}{ + \Gamma \vdash S +} +\quad \infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{ + \Gamma \vdash S +}$$ + +$$\infer{\Gamma \vdash \mt{include} \; S \leadsto \Gamma, \mathcal O(\overline{s})}{ + \Gamma \vdash S + & \Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end} +}$$ + +$$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma, c_1 \sim c_2}{ + \Gamma \vdash c_1 :: \{\kappa\} + & \Gamma \vdash c_2 :: \{\kappa\} +}$$ + +$$\infer{\Gamma \vdash \mt{class} \; x = c \leadsto \Gamma, x :: \mt{Type} \to \mt{Type} = c}{ + \Gamma \vdash c :: \mt{Type} \to \mt{Type} +} +\quad \infer{\Gamma \vdash \mt{class} \; x \leadsto \Gamma, x :: \mt{Type} \to \mt{Type}}{}$$ + \subsection{Signature Compatibility} +To simplify the judgments in this section, we assume that all signatures are alpha-varied as necessary to avoid including mmultiple bindings for the same identifier. This is in addition to the usual alpha-variation of locally-bound variables. + +We rely on a judgment $\Gamma \vdash \overline{s} \leq s'$, which expresses the occurrence in signature items $\overline{s}$ of an item compatible with $s'$. We also use a judgment $\Gamma \vdash \overline{dc} \leq \overline{dc}$, which expresses compatibility of datatype definitions. + $$\infer{\Gamma \vdash S \equiv S}{} \quad \infer{\Gamma \vdash S_1 \equiv S_2}{ \Gamma \vdash S_2 \equiv S_1 @@ -609,22 +666,34 @@ X = S \in \Gamma } \quad \infer{\Gamma \vdash M.X \equiv S}{ - \Gamma \vdash M : S' - & \mt{proj}(M, S', \mt{signature} \; X) = S + \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} + & \mt{proj}(M, \overline{s}, \mt{signature} \; X) = S }$$ $$\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}}{ \Gamma \vdash S \equiv \mt{sig} \; \overline{s^1} \; \mt{con} \; x :: \kappa \; \overline{s_2} \; \mt{end} & \Gamma \vdash c :: \kappa +} +\quad \infer{\Gamma \vdash \mt{sig} \; \overline{s^1} \; \mt{include} \; S \; \overline{s^2} \; \mt{end} \equiv \mt{sig} \; \overline{s^1} \; \overline{s} \; \overline{s^2} \; \mt{end}}{ + \Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end} }$$ $$\infer{\Gamma \vdash S_1 \leq S_2}{ \Gamma \vdash S_1 \equiv S_2 } \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \mt{end}}{} -\quad \infer{\Gamma \vdash \mt{sig} \; \overline{s^1} \; s \; \overline{s^2} \; \mt{end} \leq \mt{sig} \; s' \; \overline{s} \; \mt{end}}{ - \Gamma \vdash s \leq s'; \Gamma' - & \Gamma' \vdash \mt{sig} \; \overline{s^1} \; s \; \overline{s^2} \; \mt{end} \leq \mt{sig} \; \overline{s} \; \mt{end} +\quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; s' \; \overline{s'} \; \mt{end}}{ + \Gamma \vdash \overline{s} \leq s' + & \Gamma \vdash s' \leadsto \Gamma' + & \Gamma' \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \overline{s'} \; \mt{end} +}$$ + +$$\infer{\Gamma \vdash s \; \overline{s} \leq s'}{ + \Gamma \vdash s \leq s' +} +\quad \infer{\Gamma \vdash s \; \overline{s} \leq s'}{ + \Gamma \vdash s \leadsto \Gamma' + & \Gamma' \vdash \overline{s} \leq s' }$$ $$\infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 \leq \mt{functor} (X : S'_1) : S'_2}{ @@ -632,4 +701,68 @@ & \Gamma, X : S'_1 \vdash S_2 \leq S'_2 }$$ +$$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leq \mt{con} \; x :: \kappa}{} +\quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leq \mt{con} \; x :: \kappa}{} +\quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leq \mt{con} \; x :: \mt{Type}}{}$$ + +$$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{con} \; x :: \mt{Type}^{\mt{len}(y)} \to \mt{Type}}{ + \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} + & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc}) +}$$ + +$$\infer{\Gamma \vdash \mt{class} \; x \leq \mt{con} \; x :: \mt{Type} \to \mt{Type}}{} +\quad \infer{\Gamma \vdash \mt{class} \; x = c \leq \mt{con} \; x :: \mt{Type} \to \mt{Type}}{}$$ + +$$\infer{\Gamma \vdash \mt{con} \; x :: \kappa = c_1 \leq \mt{con} \; x :: \mt{\kappa} = c_2}{ + \Gamma \vdash c_1 \equiv c_2 +} +\quad \infer{\Gamma \vdash \mt{class} \; x = c_1 \leq \mt{con} \; x :: \mt{Type} \to \mt{Type} = c_2}{ + \Gamma \vdash c_1 \equiv c_2 +}$$ + +$$\infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{ + \Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'} +}$$ + +$$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{ + \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} + & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc}) + & \Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'} +}$$ + +$$\infer{\Gamma \vdash \cdot \leq \cdot}{} +\quad \infer{\Gamma \vdash X; \overline{dc} \leq X; \overline{dc'}}{ + \Gamma \vdash \overline{dc} \leq \overline{dc'} +} +\quad \infer{\Gamma \vdash X \; \mt{of} \; \tau_1; \overline{dc} \leq X \; \mt{of} \; \tau_2; \overline{dc'}}{ + \Gamma \vdash \tau_1 \equiv \tau_2 + & \Gamma \vdash \overline{dc} \leq \overline{dc'} +}$$ + +$$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{datatype} \; x = \mt{datatype} \; M'.z'}{ + \Gamma \vdash M.z \equiv M'.z' +}$$ + +$$\infer{\Gamma \vdash \mt{val} \; x : \tau_1 \leq \mt{val} \; x : \tau_2}{ + \Gamma \vdash \tau_1 \equiv \tau_2 +} +\quad \infer{\Gamma \vdash \mt{structure} \; X : S_1 \leq \mt{structure} \; X : S_2}{ + \Gamma \vdash S_1 \leq S_2 +} +\quad \infer{\Gamma \vdash \mt{signature} \; X = S_1 \leq \mt{signature} \; X = S_2}{ + \Gamma \vdash S_1 \leq S_2 + & \Gamma \vdash S_2 \leq S_1 +}$$ + +$$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leq \mt{constraint} \; c'_1 \sim c'_2}{ + \Gamma \vdash c_1 \equiv c'_1 + & \Gamma \vdash c_2 \equiv c'_2 +}$$ + +$$\infer{\Gamma \vdash \mt{class} \; x \leq \mt{class} \; x}{} +\quad \infer{\Gamma \vdash \mt{class} \; x = c \leq \mt{class} \; x}{} +\quad \infer{\Gamma \vdash \mt{class} \; x = c_1 \leq \mt{class} \; x = c_2}{ + \Gamma \vdash c_1 \equiv c_2 +}$$ + \end{document} \ No newline at end of file