# Changeset 2425

Ignore:
Timestamp:
Oct 31, 2012, 3:33:33 PM (7 years ago)
Message:

Garrigue's stuff completely added to the paper. Need to explain the typing relation properly.

File:
1 edited

Unmodified
Added
Removed
• ## Papers/polymorphic-variants-2012/polymorphic-variants.tex

 r2424 \usepackage{prooftree} \newcommand{\cons}{{::}} \newcommand{\ent}{\vdash} \newcommand{\fall}[2]{\forall{#1}.#2} \newcommand{\funarr}{\rightarrow} \newcommand{\lam}[2]{\lambda{#1}.{#2}} \newcommand{\letin}[3]{\mathbf{let}\ {#1}\ {:=}\ {#2}\ \mathbf{in}\ {#3}} \newcommand{\match}[3]{\mathbf{match}\ #1\ \mathbf{with}\ #2\ \Rightarrow #3} \newcommand{\pair}[2]{\langle #1, #2 \rangle} \newcommand{\polytag}[1]{{`}#1} \newcommand{\rulefont}[1]{\ensuremath{(\mathbf{#1})}} \begin{gather*} \begin{prooftree} (\Gamma(x) = \phi) \justifies K; \Gamma \ent x : \phi (\Gamma(x) = \sigma) \justifies K; \Gamma \ent x : \sigma \using\rulefont{{\Gamma}x} \end{prooftree} \\[1.5ex] \begin{prooftree} K; \Gamma \ent r : \phi \quad K; \Gamma, x:\phi \ent s : \psi K; \Gamma \ent r : \sigma \quad K; \Gamma, x:\sigma \ent s : \psi \justifies K; \Gamma \ent \letin{x}{r}{s} : \psi \qquad \begin{prooftree} K;\Gamma \ent r : \sigma \quad (a \not\in ftv(\Gamma)) \justifies K;\Gamma \ent r : \fall{a}{\sigma} \using\rulefont{{\Gamma}{\forall}{a}} \end{prooftree} \\[1.5ex] \begin{prooftree} K;\Gamma \ent r : \fall{a}{\sigma} \quad K;\Gamma \ent s : \psi \justifies K;\Gamma \ent rs : \sigma[a := \psi] \using\rulefont{{\Gamma}inst{a}} \end{prooftree} \\[1.5ex] \begin{prooftree} (L \subseteq L' \quad H \subseteq H') \justifies K \oplus i_{{\geq \pair{L}{U}}} \ent i \geq \pair{L'}{H'} \using\rulefont{{K}i} \end{prooftree} \qquad \begin{prooftree} K;\Gamma \ent r : \phi \quad K \ent i \geq \pair{tag}{\top} \justifies K;\Gamma \ent \polytag{tag(r)} : [ i \mid tag : \phi \cons T ] \using\rulefont{{K}variant} \end{prooftree} \\[1.5ex] \begin{prooftree} K;\Gamma \ent r : [ i \mid \{ tag_k : \phi_k \}^n_1 \cons T ] \quad K \ent i \geq \pair{\bot}{\{tag_k\}^n_1} \quad K;\Gamma, x_k : \phi_k \ent r_k : \psi \quad (1 \leq k \leq n) \justifies K;\Gamma \ent \mathbf{match}\ r\ \mathbf{with}\ \{ \polytag{tag_k(x_k)} \Rightarrow r_k \}^n_1 : \psi \using\rulefont{{K}match} \end{prooftree} \\[1.5ex] \begin{prooftree} K;\Gamma \ent r : \sigma \quad (\rho \not\in ftv(\Gamma)) \justifies K;\Gamma \ent r : \fall{\rho}{\sigma} \using\rulefont{{K}{\forall}{\rho}} \end{prooftree} \qquad \begin{prooftree} K;\Gamma \ent r : \fall{\rho}{\sigma} \quad K;\Gamma \ent s : T \justifies K;\Gamma \ent rs : \sigma[\rho := T] \using\rulefont{{K}inst{\rho}} \end{prooftree} \\[1.5ex] \begin{prooftree} K \oplus i_{\geq \pair{L}{U}};\Gamma \ent r : \sigma \justifies K;\Gamma \ent r : \fall{i_{\geq \pair{L}{U}}}{\sigma} \using\rulefont{{K}{\forall}{i}} \end{prooftree} \qquad \begin{prooftree} K;\Gamma \ent r : \fall{i_{\geq \pair{L}{U}}}{\sigma} \quad K \ent i' \geq \pair{L, U} \justifies K;\Gamma \ent r : \sigma[i := i'] \using\rulefont{{K}inst{i}} \end{prooftree} \end{gather*}
Note: See TracChangeset for help on using the changeset viewer.