Gradual Typing

\begin{align*} e ::=&\quad c && \text{constant} \\ &|\quad x && \text{variable} \\ &|\quad e\ e &&\text{application} \\ &|\quad \lambda x : \tau.\ e &&\text{abstraction} \\ \tau ::=&\quad \mathsf{Int} && \text{integer type} \\ &|\quad \mathsf{Bool} && \text{boolean type} \\ &|\quad \tau \rightarrow \tau && \text{function type} \end{align*}

\begin{gather} \tag{T-Abs} \frac{\type{\Gamma, x:\tau}{e}{\tau'}}{\type{\Gamma}{(\abs{x}{\tau}{e})}{\tau \arrow \tau'}} \\[2ex] \tag{T-App} \frac{\type{\Gamma}{e}{\tau' \arrow \tau} \quad \type{\Gamma}{e'}{\tau'}}{\type{\Gamma}{e\ e'}{\tau}} \\[2ex] \tag{T-Var} \frac{ x : \tau \in \Gamma }{ \type{\Gamma}{x}{\tau} }\\[2ex] \tag{T-Const} \frac{c \text{ has type } \tau}{\type{\Gamma}{c}{\tau}} \end{gather}

\begin{align*} e ::=&\quad c && \text{constant} \\ &|\quad x && \text{variable} \\ &|\quad e\ e &&\text{application} \\ &|\quad \lambda x : \tau.\ e &&\text{abstraction} \\ \tau ::=&\quad \mathsf{Int} && \text{integer type} \\ &|\quad \mathsf{Bool} && \text{boolean type} \\ &|\quad \tau \rightarrow \tau && \text{function type} \\ &|\quad \boxed{\que} && \text{any type} \end{align*}

\begin{gather} \tau \sim \tau\ \text{(C-Refl)} \quad \frac{\tau_{1} \sim \tau_{1}' \quad \tau_{2} \sim \tau_{2}'}{\tau_{1} \rightarrow \tau_{2} \sim \tau_{1}' \rightarrow \tau_{2}'}\ \text{(C-Fun)} \\[2ex] \tau \sim \que\ \text{(C-UnR)} \quad \que \sim \tau\ \text{(C-UnL)} \end{gather}

\begin{gather} \frac{\type{\Gamma, x:\tau}{e}{\tau'}}{\type{\Gamma}{(\abs{x}{\tau}{e})}{\tau \arrow \tau'}} \quad \text{(T-Abs)} \\[2ex] \boxed{\frac{\type{\Gamma}{e}{\que} \quad \type{\Gamma}{e'}{\tau'}}{\type{\Gamma}{e\ e'}{\que}}} \quad \text{(T-App-1)} \\[2ex] \boxed{\frac{\type{\Gamma}{e}{\tau'' \arrow \tau} \quad \type{\Gamma}{e'}{\tau'} \quad \tau \sim \tau''}{\type{\Gamma}{e\ e'}{\tau}}} \quad \text{(T-App-2)} \\[2ex] \frac{ x : \tau \in \Gamma }{ \type{\Gamma}{x}{\tau} } \quad \text{(T-Var)} \\[2ex] \frac{ c \text{ has type } \tau }{ \type{\Gamma}{c}{\tau} } \quad \text{(T-Const)} \end{gather}

\begin{align*} e ::=&\quad c && \text{constant} \\ &|\quad x && \text{variable} \\ &|\quad e\ e &&\text{application} \\ &|\quad \lambda x : \tau.\ e &&\text{abstraction} \\ &|\quad \boxed{\langle \tau \rangle e} && \text{type cast} \\ \tau ::=&\quad \mathsf{Int} && \text{integer type} \\ &|\quad \mathsf{Bool} && \text{boolean type} \\ &|\quad \tau \rightarrow \tau && \text{function type} \\ &|\quad \que && \text{any type} \end{align*}

\begin{gather} \frac{\cast{\Gamma, x:\tau}{e}{e'}{\tau'}}{\cast{\Gamma}{\abs{x}{\tau}{e}}{\abs{x}{\tau}{e'}}{\tau \arrow \tau'}}\quad \text{(I-Abs)} \\[2ex] \frac{ x : \tau \in \Gamma }{ \cast{\Gamma}{x}{x}{\tau} } \quad \text{(I-Var)} \\[2ex] \frac{ c \text{ has type } \tau}{\cast{\Gamma}{c}{c}{\tau}} \quad \text{(I-Const)} \end{gather}

\begin{gather} \frac{ \cast{\Gamma}{e_{1}}{e_{1}'}{\que} \quad \cast{\Gamma}{e_{2}}{e_{2}'}{\tau_{2}} }{ \cast{\Gamma}{e_{1}\ e_{2}}{(\langle \tau_{2} \rightarrow \que \rangle e_{1}')\ e_{2}'}{\que} } \quad \text{(I-App-1)} \\[2ex] \frac{ \begin{gathered} \cast{\Gamma}{e_{1}}{e_{1}'}{\tau \rightarrow \tau'} \\ \cast{\Gamma}{e_{2}}{e_{2}'}{\tau_{2}} \quad \tau_{2} \neq \tau \quad \tau_{2} \sim \tau \end{gathered} }{ \cast{\Gamma}{e_{1}\ e_{2}}{e_{1}'\ (\langle \tau \rangle e_{2}')}{\tau'} }\quad \text{(I-App-2)} \\[2ex] \frac{ \cast{\Gamma}{e_{1}}{e_{1}'}{\tau' \arrow \tau} \quad \cast{\Gamma}{e_{2}}{e_{2}'}{\tau'} }{ \cast{\Gamma}{e_{1}\ e_{2}}{e_{1}'\ e_{2}'}{\tau} } \quad \text{(I-App-3)} \end{gather}

\begin{align*} v ::=&\quad c && \text{constant} \\ &|\quad x && \text{variable} \\ &|\quad \lambda x : \tau.\ e &&\text{abstraction} \\ % v ::=&|\quad s && \text{simple values} \\ % &|\quad \langle \que \rangle s && \text{boxed value} \\ \varepsilon ::=&\quad \mathsf{CastError} && \text{failed cast} \\ r ::=&\quad \varepsilon ~|~ v && \text{result} \end{align*}

\begin{gather} \frac{ e \Downarrow v \quad \type{\emptyset}{v}{\mathsf{Int}} } { \langle \mathsf{Int} \rangle e \Downarrow v } \quad \text{(E-Cast-Int)} \\[2ex] \frac{ \begin{gathered} e \Downarrow v \quad \type{\emptyset}{v}{\tau_2 \rightarrow \tau_2'} \\ \tau_2 \rightarrow \tau_2' \sim \tau_1 \rightarrow \tau_1' \quad x\ \text{is fresh} \end{gathered} } { \langle \tau_1 \rightarrow \tau_1' \rangle e \Downarrow \lambda x: \tau_1.\ (\langle \tau_1' \rangle (v (\langle \tau_2 \rangle x))) } \quad \text{(E-Cast-Func)} \\[2ex] \frac{ e \Downarrow v } { \langle \que \rangle e \Downarrow v } \quad \text{(E-Cast-Any)} \\[2ex] \frac{ e \Downarrow v \quad \type{\emptyset}{v}{\tau'} \quad \tau \not \sim \tau' } { \langle \tau \rangle e \Downarrow \mathsf{CastError} } \quad \text{(E-Cast-Err)} \\[2ex] \end{gather}

\begin{gather} \lambda x:\tau.\ e \Downarrow \lambda x:\tau.\ e \quad \text{(E-Abs)} \\[2ex] \frac{ e \Downarrow \lambda x:\tau.\ e'' \quad e' \Downarrow v' \quad e''[v'/x] \Downarrow v } { e\ e' \Downarrow v } \quad \text{(E-App)} \\[2ex] c \Downarrow c \quad \text{(E-Const)} \end{gather}

\begin{gather} \frac{e \Downarrow \varepsilon}{\langle \tau \rangle e \Downarrow \varepsilon} \quad \text{(E-Cast-Prop)} \\[2ex] \frac{e \Downarrow \varepsilon}{e\ e' \Downarrow \varepsilon} \quad \text{(E-App-Prop-1)} \\[2ex] \frac{e \Downarrow \lambda x:\tau.\ e'' \quad e' \Downarrow \varepsilon}{e\ e' \Downarrow \varepsilon} \quad \text{(E-App-Prop-2)} \\[2ex] \end{gather}