diff options
author | 2008-11-29 11:33:51 -0500 | |
---|---|---|
committer | 2008-11-29 11:33:51 -0500 | |
commit | e2c7097ddf12808ae9f108e911e93ab99e640d80 (patch) | |
tree | ce9174433282dc590125a784cfe65a41177e121f | |
parent | 73de524554aaa11c454e95cec39e8ada98c44cf4 (diff) |
Declaration typing
-rw-r--r-- | doc/manual.tex | 83 |
1 files changed, 81 insertions, 2 deletions
diff --git a/doc/manual.tex b/doc/manual.tex index db679405..4df95230 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -181,8 +181,8 @@ $$\begin{array}{rrcll} &&& \mt{open} \; \mt{constraints} \; M & \textrm{inclusion of just the constraints from a module} \\ &&& \mt{table} \; x : c & \textrm{SQL table} \\ &&& \mt{sequence} \; x & \textrm{SQL sequence} \\ - &&& \mt{class} \; x = c & \textrm{concrete type class} \\ &&& \mt{cookie} \; x : \tau & \textrm{HTTP cookie} \\ + &&& \mt{class} \; x = c & \textrm{concrete type class} \\ \\ \textrm{Modules} & M &::=& \mt{struct} \; d^* \; \mt{end} & \textrm{constant} \\ &&& X & \textrm{variable} \\ @@ -245,8 +245,10 @@ Since there is significant mutual recursion among the judgments, we introduce th \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 S$ is the signature validity judgment. +\item $\Gamma \vdash S \leq S$ is the signature compatibility judgment. \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{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, 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$. \end{itemize} \subsection{Kinding} @@ -521,4 +523,81 @@ $$\infer{\Gamma \vdash \{\overline{x = p}\} \leadsto \Gamma_n; \{\overline{x = \ & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i }$$ +\subsection{Declaration Typing} + +We use an auxiliary judgment $\overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'$, expressing the enrichment of $\Gamma$ with the types of the datatype constructors $\overline{dc}$, when they are known to belong to datatype $x$ with type parameters $\overline{y}$. + +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$. + +$$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{} +\quad \infer{\Gamma \vdash d, \overline{d} \leadsto \Gamma''}{ + \Gamma \vdash d \leadsto \Gamma' + & \Gamma' \vdash \overline{d} \leadsto \Gamma'' +}$$ + +$$\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 : S + & \mt{proj}(M, 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 = e \leadsto \Gamma, x : \tau}{ + \Gamma \vdash e : \tau +}$$ + +$$\infer{\Gamma \vdash \mt{val} \; \mt{rec} \; \overline{x : \tau = e} \leadsto \Gamma, \overline{x : \tau}}{ + \forall i: \Gamma, \overline{x : \tau} \vdash e_i : \tau_i + & \textrm{$e_i$ starts with an expression $\lambda$, optionally preceded by constructor and disjointness $\lambda$s} +}$$ + +$$\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}{ + \Gamma \vdash S +}$$ + +$$\infer{\Gamma \vdash \mt{open} \; M \leadsto \Gamma, \mathcal O(M, S)}{ + \Gamma \vdash M : S +}$$ + +$$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma}{ + \Gamma \vdash c_1 :: \{\kappa\} + & \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 +}$$ + +$$\infer{\Gamma \vdash \mt{table} \; x : c \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_table} \; c}{ + \Gamma \vdash c :: \{\mt{Type}\} +} +\quad \infer{\Gamma \vdash \mt{sequence} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_sequence}}{}$$ + +$$\infer{\Gamma \vdash \mt{cookie} \; x : \tau \leadsto \Gamma, x : \mt{Basis}.\mt{http\_cookie} \; \tau}{ + \Gamma \vdash \tau :: \mt{Type} +}$$ + +$$\infer{\Gamma \vdash \mt{class} \; x = c \leadsto \Gamma, x :: \mt{Type} \to \mt{Type} = c}{ + \Gamma \vdash c :: \mt{Type} \to \mt{Type} +}$$ + +$$\infer{\overline{y}; x; \Gamma \vdash \cdot \leadsto \Gamma}{} +\quad \infer{\overline{y}; x; \Gamma \vdash X \mid \overline{dc} \leadsto \Gamma', X : \overline{y ::: \mt{Type}} \to x \; \overline{y}}{ + \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma' +} +\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}}{ + \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma' +}$$ + \end{document}
\ No newline at end of file |