Mercurial > urweb

comparison doc/manual.tex @ 534:65c253a9ca92

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pattern typing
author Adam Chlipala <adamc@hcoop.net>
date Sat, 29 Nov 2008 10:49:47 -0500
parents 419f51b1e68d
children b742bf4e377b
comparison
equal deleted inserted replaced
533:419f51b1e68d 534:65c253a9ca92
241 \item $\Gamma \vdash c :: \kappa$ assigns a kind to a constructor in a context. 241 \item $\Gamma \vdash c :: \kappa$ assigns a kind to a constructor in a context.
242 \item $\Gamma \vdash c \sim c$ proves the disjointness of two record constructors; that is, that they share no field names. We overload the judgment to apply to pairs of field names as well. 242 \item $\Gamma \vdash c \sim c$ proves the disjointness of two record constructors; that is, that they share no field names. We overload the judgment to apply to pairs of field names as well.
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 M : S$ is the module signature checking judgment. 248 \item $\Gamma \vdash M : S$ is the module signature checking judgment.
249 \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$. 249 \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$.
250 \end{itemize} 250 \end{itemize}
251 251
395 \quad \infer{\Gamma \vdash \mt{fold} \; f \; i \; (\mt{map} \; f' \; c) 395 \quad \infer{\Gamma \vdash \mt{fold} \; f \; i \; (\mt{map} \; f' \; c)
396 \equiv \mt{fold} \; (\lambda (x_1 :: \mt{Name}) (x_2 :: \kappa) \Rightarrow f \; x_1 \; (f' \; x_2)) \; i \; c}{}$$ 396 \equiv \mt{fold} \; (\lambda (x_1 :: \mt{Name}) (x_2 :: \kappa) \Rightarrow f \; x_1 \; (f' \; x_2)) \; i \; c}{}$$
397 397
398 $$\infer{\Gamma \vdash \mt{map} \; f \; (c_1 \rc c_2) \equiv \mt{map} \; f \; c_1 \rc \mt{map} \; f \; c_2}{}$$ 398 $$\infer{\Gamma \vdash \mt{map} \; f \; (c_1 \rc c_2) \equiv \mt{map} \; f \; c_1 \rc \mt{map} \; f \; c_2}{}$$
399 399
400 \subsection{Typing} 400 \subsection{Expression Typing}
401 401
402 We assume the existence of a function $T$ assigning types to literal constants. It maps integer constants to $\mt{Basis}.\mt{int}$, float constants to $\mt{Basis}.\mt{float}$, and string constants to $\mt{Basis}.\mt{string}$. 402 We assume the existence of a function $T$ assigning types to literal constants. It maps integer constants to $\mt{Basis}.\mt{int}$, float constants to $\mt{Basis}.\mt{float}$, and string constants to $\mt{Basis}.\mt{string}$.
403 403
404 We also refer to a function $\mathcal I$, such that $\mathcal I(\tau)$ ``uses an oracle'' to instantiate all constructor function arguments at the beginning of $\tau$ that are marked implicit; i.e., replace $x_1 ::: \kappa_1 \to \ldots \to x_n ::: \kappa_n \to \tau$ with $[x_1 \mapsto c_1]\ldots[x_n \mapsto c_n]\tau$, where the $c_i$s are inferred and $\tau$ does not start like $x ::: \kappa \to \tau'$. 404 We also refer to a function $\mathcal I$, such that $\mathcal I(\tau)$ ``uses an oracle'' to instantiate all constructor function arguments at the beginning of $\tau$ that are marked implicit; i.e., replace $x_1 ::: \kappa_1 \to \ldots \to x_n ::: \kappa_n \to \tau$ with $[x_1 \mapsto c_1]\ldots[x_n \mapsto c_n]\tau$, where the $c_i$s are inferred and $\tau$ does not start like $x ::: \kappa \to \tau'$.
405 405
483 \Gamma \vdash c_1 :: \{\kappa\} 483 \Gamma \vdash c_1 :: \{\kappa\}
484 & \Gamma \vdash c_2 :: \{\kappa\} 484 & \Gamma \vdash c_2 :: \{\kappa\}
485 & \Gamma, c_1 \sim c_2 \vdash e : \tau 485 & \Gamma, c_1 \sim c_2 \vdash e : \tau
486 }$$ 486 }$$
487 487
488 \subsection{Pattern Typing}
489
490 $$\infer{\Gamma \vdash \_ \leadsto \Gamma; \tau}{}
491 \quad \infer{\Gamma \vdash x \leadsto \Gamma, x : \tau; \tau}{}
492 \quad \infer{\Gamma \vdash \ell \leadsto \Gamma; T(\ell)}{}$$
493
494 $$\infer{\Gamma \vdash X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{
495 X : \overline{x ::: \mt{Type}} \to \tau \in \Gamma
496 & \textrm{$\tau$ not a function type}
497 }
498 \quad \infer{\Gamma \vdash X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{
499 X : \overline{x ::: \mt{Type}} \to \tau'' \to \tau \in \Gamma
500 & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
501 }$$
502
503 $$\infer{\Gamma \vdash M.X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{
504 \Gamma \vdash M : S
505 & \mt{proj}(M, S, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau
506 & \textrm{$\tau$ not a function type}
507 }$$
508
509 $$\infer{\Gamma \vdash M.X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{
510 \Gamma \vdash M : S
511 & \mt{proj}(M, S, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau'' \to \tau
512 & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
513 }$$
514
515 $$\infer{\Gamma \vdash \{\overline{x = p}\} \leadsto \Gamma_n; \{\overline{x = \tau}\}}{
516 \Gamma_0 = \Gamma
517 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
518 }
519 \quad \infer{\Gamma \vdash \{\overline{x = p}, \ldots\} \leadsto \Gamma_n; \$([\overline{x = \tau}] \rc c)}{
520 \Gamma_0 = \Gamma
521 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
522 }$$
523
488 \end{document} 524 \end{document}