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

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

File:
1 edited

Legend:

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

    r2424 r2425  
    1010\usepackage{prooftree}
    1111
     12\newcommand{\cons}{{::}}
    1213\newcommand{\ent}{\vdash}
     14\newcommand{\fall}[2]{\forall{#1}.#2}
    1315\newcommand{\funarr}{\rightarrow}
    1416\newcommand{\lam}[2]{\lambda{#1}.{#2}}
    1517\newcommand{\letin}[3]{\mathbf{let}\ {#1}\ {:=}\ {#2}\ \mathbf{in}\ {#3}}
     18\newcommand{\match}[3]{\mathbf{match}\ #1\ \mathbf{with}\ #2\ \Rightarrow #3}
    1619\newcommand{\pair}[2]{\langle #1, #2 \rangle}
     20\newcommand{\polytag}[1]{{`}#1}
    1721\newcommand{\rulefont}[1]{\ensuremath{(\mathbf{#1})}}
    1822
     
    131135\begin{gather*}
    132136\begin{prooftree}
    133 (\Gamma(x) = \phi)
    134 \justifies
    135 K; \Gamma \ent x : \phi
     137(\Gamma(x) = \sigma)
     138\justifies
     139K; \Gamma \ent x : \sigma
    136140\using\rulefont{{\Gamma}x}
    137141\end{prooftree}
     
    152156\\[1.5ex]
    153157\begin{prooftree}
    154 K; \Gamma \ent r : \phi \quad K; \Gamma, x:\phi \ent s : \psi
     158K; \Gamma \ent r : \sigma \quad K; \Gamma, x:\sigma \ent s : \psi
    155159\justifies
    156160K; \Gamma \ent \letin{x}{r}{s} : \psi
     
    159163\qquad
    160164\begin{prooftree}
     165K;\Gamma \ent r : \sigma \quad (a \not\in ftv(\Gamma))
     166\justifies
     167K;\Gamma \ent r : \fall{a}{\sigma}
     168\using\rulefont{{\Gamma}{\forall}{a}}
     169\end{prooftree}
     170\\[1.5ex]
     171\begin{prooftree}
     172K;\Gamma \ent r : \fall{a}{\sigma} \quad K;\Gamma \ent s : \psi
     173\justifies
     174K;\Gamma \ent rs : \sigma[a := \psi]
     175\using\rulefont{{\Gamma}inst{a}}
     176\end{prooftree}
     177\\[1.5ex]
     178\begin{prooftree}
    161179(L \subseteq L' \quad H \subseteq H')
    162180\justifies
    163181K \oplus i_{{\geq \pair{L}{U}}} \ent i \geq \pair{L'}{H'}
    164182\using\rulefont{{K}i}
     183\end{prooftree}
     184\qquad
     185\begin{prooftree}
     186K;\Gamma \ent r : \phi \quad K \ent i \geq \pair{tag}{\top}
     187\justifies
     188K;\Gamma \ent \polytag{tag(r)} : [ i \mid tag : \phi \cons T ]
     189\using\rulefont{{K}variant}
     190\end{prooftree}
     191\\[1.5ex]
     192\begin{prooftree}
     193K;\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
     194K;\Gamma, x_k : \phi_k \ent r_k : \psi \quad (1 \leq k \leq n)
     195\justifies
     196K;\Gamma \ent \mathbf{match}\ r\ \mathbf{with}\ \{ \polytag{tag_k(x_k)} \Rightarrow r_k \}^n_1 : \psi
     197\using\rulefont{{K}match}
     198\end{prooftree}
     199\\[1.5ex]
     200\begin{prooftree}
     201K;\Gamma \ent r : \sigma \quad (\rho \not\in ftv(\Gamma))
     202\justifies
     203K;\Gamma \ent r : \fall{\rho}{\sigma}
     204\using\rulefont{{K}{\forall}{\rho}}
     205\end{prooftree}
     206\qquad
     207\begin{prooftree}
     208K;\Gamma \ent r : \fall{\rho}{\sigma} \quad K;\Gamma \ent s : T
     209\justifies
     210K;\Gamma \ent rs : \sigma[\rho := T]
     211\using\rulefont{{K}inst{\rho}}
     212\end{prooftree}
     213\\[1.5ex]
     214\begin{prooftree}
     215K \oplus i_{\geq \pair{L}{U}};\Gamma \ent r : \sigma
     216\justifies
     217K;\Gamma \ent r : \fall{i_{\geq \pair{L}{U}}}{\sigma}
     218\using\rulefont{{K}{\forall}{i}}
     219\end{prooftree}
     220\qquad
     221\begin{prooftree}
     222K;\Gamma \ent r : \fall{i_{\geq \pair{L}{U}}}{\sigma} \quad K \ent i' \geq \pair{L, U}
     223\justifies
     224K;\Gamma \ent r : \sigma[i := i']
     225\using\rulefont{{K}inst{i}}
    165226\end{prooftree}
    166227\end{gather*}
Note: See TracChangeset for help on using the changeset viewer.