xi experimental type system

The type system presented below is based on the one developed be Dunfield and Krishnaswami [[dunfield2013complete]] (DK). The sets of rules below, except where indicated, are taken directly from their paper.

\( \def\ea{\widehat{\alpha}} \def\eb{\widehat{\beta}} \def\sep{ \quad\quad} \newcommand{\mark}[1]{\blacktriangleright_{#1}} \newcommand{\expr}[3]{#1\ \vdash\ #2\ \dashv\ #3} \)

Grammar

\[\begin{split} \text{Terms} \sep e\ &:= () \sep & \text{nothing} \\ &|\ x \sep & \text{var} \\ &|\ \lambda x .\ e \sep & \text{abstraction} \\ &|\ e e \sep & \text{application} \\ &|\ e\ ::\ A \sep & \text{annotation} \\ &|\ x=e\ ;\ e \sep & \text{declaration} \\ &|\ x\ ::\ A\ ; e \sep & \text{signature} \\ &|\ [e1, e2, …] \sep & \text{homogenous list} \\ &|\ (e1, e2, …) \sep & \text{tuple} \\ \end{split}\]

\[\begin{split} \text{Types} \sep A,B,C\ &:= 1 \sep & \text{unit} \\ &|\ \alpha \sep & \text{var} \\ &|\ A \rightarrow B \sep & \text{function} \\ &|\ \forall \alpha. A \sep & \text{universal quantification} \\ &|\ \alpha\ A \sep & \text{parameterization} \end{split}\]

The terms describe a typed lambda calculus. The declaration and signature expressions are additions that allow construction of larger programs. We depart from Hindley-Milner (HM) by excluding a let term. In HM, expressions bound in let are generalized, allowing statements such as:

let f = (forall a . a -> a) in
    x = (f 42, f "lettuce")

Where \(f\) is generalized, allowing it to retain its polymorphism. The same is not true of variables bound in functions (in HM at least). For example, the following Haskell expression fails to typecheck:

foo :: (a -> a) -> (Int, String)
foo f = (f 42, f "lettuce")

We do not suport let expressions or let-polymorphism, instead we generalize expressions only if they are bound at the top-level (i.e. in declaration terms). This follows the practice argued for in [[vytiniotis2010let]].

Algorithmic Rules

Subtyping and instantiation

The subtyping rules come directly from DK, except for the new rule for type application. This extension allows types to take an arbitrary number of type parameters. For example, the type of a hashmap from strings to integers might be written as Map Str Int. We also support [a] as a shortcut for List a.

Table 1. Subtyping Rules
\(\frac{}{\expr{\Gamma[\alpha]}{\alpha\ <:\ \alpha}{\Gamma[\alpha]}}\) <:Var \(\quad\quad\) \(\frac{}{\expr{\Gamma}{1\ <:\ 1}{\Gamma}}\) <:Unit \(\quad\quad\) \(\frac{}{\expr{\Gamma[\ea]}{\ea\ <:\ \ea}{\Gamma[\ea]}}\) <:Exvar \(\frac{\expr{\Gamma}{B_1\ <:\ A_1}{\Theta} \quad \expr{\Theta}{[\Theta]A_2\ <:\ [\Theta]B_2}{\Delta}}{\expr{\Gamma}{A_1 \rightarrow A_2\ <:\ B_1 \rightarrow B_2}{\Delta}}\) <:→ \(\frac{A_1\ <:\ B_1 \quad A_2\ <:\ B_2}{\expr{\Gamma}{A_1\ A_2\ <:\ B_1\ B_2}{\Delta}}\) <:App \(\frac{\expr{\Gamma,\mark{\ea},\ea}{[\ea/\alpha]A\ <:\ B}{\Delta,\mark{\ea},\Theta}}{\expr{\Gamma}{\forall \alpha . A\ <:\ B}{\Delta}}\) <:∀L \(\quad\quad\) \(\frac{\expr{\Gamma,\alpha}{A<:B}{\Delta,\alpha,\Theta}}{\expr{\Gamma}{A <: \forall \alpha . B}{\Delta}}\) <:∀R \(\frac{\ea \notin FV(A) \quad \expr{\Gamma[\ea]}{\ea\ :\leqq\ A}{\Delta}}{\expr{\Gamma[\ea]}{\ea\ <:\ A}{\Delta}}\) <:InstantiateL \(\quad\quad\) \(\frac{\ea \notin FV(A) \quad \expr{\Gamma[\ea]}{A\ :\leqq\ \ea}{\Delta}}{\expr{\Gamma[\ea]}{A\ <:\ \ea}{\Delta}}\) <:InstantiateR
\(\text{subtype} :: A \rightarrow B \rightarrow \Gamma \rightarrow \Delta\)

Table 2. Instantiation Rules
\(\frac{\Gamma\ \vdash\ \tau}{\expr{\Gamma,\ea,\Gamma'}{\ea\ :\leqq\ \tau}{\Gamma,\ea=\tau,\Gamma'}}\) InstLSolve \(\quad\quad\) \(\frac{}{\expr{\Gamma[\ea][\eb]}{\ea :\leqq \eb}{\Gamma[\ea][\eb=\ea]}}\) InstLReach \(\frac{\expr{\Gamma[\ea_2,\ea_1,\ea=\ea_2\rightarrow\ea_1]}{A_1 :\leqq \ea_1}{\Theta} \quad \expr{\Theta}{\ea_2 :\leqq [\Theta]A_2}{\Delta}}{\expr{\Gamma[\ea]}{\ea\ :\leqq\ A_1 \rightarrow A_2}{\Delta}}\) InstLArr \(\quad\quad\) \(\frac{\expr{\Gamma[\ea],\beta}{\ea\ :\leqq\ B}{\Delta,\beta,\Delta'}}{\expr{\Gamma[\ea}{\ea\ :\leqq\ \forall \beta . B}{\Delta}}\) InstLAllR
\(\frac{\Gamma\ \vdash\ \tau}{\expr{\Gamma,\ea,\Gamma'}{\tau\ :\leqq\ \ea}{\Gamma,\ea=\tau,\Gamma'}}\) InstRSolve \(\quad\quad\) \(\frac{}{\expr{\Gamma[\ea][\eb]}{\eb :\leqq \ea}{\Gamma[\ea][\eb=\ea]}}\) InstRReach \(\frac{\expr{\Gamma[\ea_2,\ea_1,\ea=\ea_2\rightarrow\ea_1]}{\ea_1 :\leqq A_1}{\Theta} \quad \expr{\Theta}{[\Theta]A_2 :\leqq \ea_2}{\Delta}}{\expr{\Gamma[\ea]}{A_1 \rightarrow A_2\ :\leqq\ \ea}{\Delta}}\) InstRArr \(\quad\quad\) \(\frac{\Gamma[\widehat{\alpha}],\blacktriangleright \widehat{\beta},\widehat{\beta}\ \vdash [\widehat{\beta}/\beta]B\ :\leqq\ \widehat{\alpha}\ \dashv\ \Delta,\blacktriangleright \widehat{\beta},\Delta'}{\Gamma[\widehat{\alpha}\ \vdash\ \forall \beta . B\ :\leqq\ \widehat{\alpha}\ \dashv\ \Delta}\) InstRAllL
\(\text{instantiate}\ ::\ A \rightarrow B \rightarrow \Gamma \rightarrow \Delta\)

Typechecking rules — bidirectional or tridirectional?

We add new typechecking rules that add support for primitives, containers, declarations and signatures. The primitive rules are axioms where the types are inferred by the lexer. The only currently supported container is a homogenous list (e.g., [Num] for a list of numbers). A declaration allows a variable to be assigned to an expression. Top-level shadowing is not allowed (i.e. no re-assignment). Also the types are generalized, with all remaining existential variables pulled out as universal quantifiers.

Table 3. infer
\(\frac{}{\expr{\Gamma}{\text{number} \Rightarrow \text{Num}}{\Gamma}}\) Num⇒ \(\quad\quad\) \(\frac{}{\expr{\Gamma}{\text{int} \Rightarrow \text{Int}}{\Gamma}}\) Int⇒ \(\quad\quad\) \(\frac{}{\expr{\Gamma}{\text{string} \Rightarrow \text{Str}}{\Gamma}}\) Str⇒ \(\quad\quad\) \(\frac{}{\expr{\Gamma}{\text{bool} \Rightarrow \text{Bool}}{\Gamma}}\) Bool⇒ \(\frac{x \notin \text{FV}(\Gamma) \quad \expr{\Gamma}{e_1\ \Rightarrow\ A}{\Gamma,\Theta} \quad \Gamma\ \dashv\ \text{Gen}(A)=A' \quad \expr{\Gamma,x:A'}{e_2\ \Rightarrow\ B}{\Delta}}{\expr{\Gamma}{x=e_1\ ;\ e_2}{\Delta}}\) Declaration \(\quad\quad\) \(\frac{\expr{\Gamma, x:A}{e_2 \Rightarrow A}{\Delta}}{\expr{\Gamma}{x\ ::\ A\ ;\ e_2}{\Delta}}\) Signature \(\frac{\expr{\Gamma}{x_1 \Rightarrow A}{\Delta_1} \quad \expr{\Delta_1}{x_1 \Leftarrow A}{\Delta_2}\ ... \quad \expr{\Delta_{n-1}}{x_n \Leftarrow A}{\Delta_n}}{\expr{\Gamma}{[x_1,x_2, ... x_n]}{\Delta_n,\ \text{List}\ A}}\) List \(\quad\quad\) \(\frac{\expr{\Gamma}{x_1 \Rightarrow A_1}{\Delta_1} \quad ... \quad \expr{\Delta_{n-1}}{x_n \Rightarrow A_n}{\Delta_n}}{\expr{\Gamma}{(x_1,x_2, ... x_n)}{\Delta_n,\ \text{Tuple}\ A_1\ ...\ A_n}}\) Tuple \(\frac{}{\expr{\Gamma}{() \Rightarrow 1}{\Gamma}}\) 1l⇒ \(\quad\quad\) \(\frac{(x:A) \in \Gamma}{\expr{\Gamma}{x\ \Rightarrow A}{\Gamma}}\) Var \(\quad\quad\) \(\frac{\expr{\Gamma,\ea,\eb,x:\ea}{e \Leftarrow \eb}{\Delta, x:\ea, \Theta}}{\expr{\Gamma}{\lambda x.e\ \Rightarrow\ \ea\rightarrow \eb}{\Delta}}\) →I⇒ \(\quad\quad\) \(\frac{\expr{\Gamma}{e_1\ \Rightarrow\ A}{\Theta} \quad\quad \expr{\Theta}{[\Theta]A \bullet e_2 \Rightarrow\Rightarrow C}{\Delta}}{\expr{\Gamma}{e_1 e_2 \Rightarrow C}{\Delta}}\) →E \(\quad\quad\) \(\frac{\Gamma\ \vdash\ A \quad\quad \expr{\Gamma}{e \Leftarrow A}{\Delta}}{\expr{\Gamma}{(e:A)\ \Rightarrow\ A}{\Delta}}\) Anno
\(\text{infer} :: \Gamma \rightarrow e \rightarrow (\Delta, A)\)

Table 4. check
\(\frac{}{\expr{\Gamma}{() \Leftarrow 1}{\Gamma}}\) 1I \(\quad\quad\) \(\frac{\expr{\Gamma,x:A}{e \Leftarrow B}{\Delta,x:A,\Theta}}{\expr{\Gamma}{\lambda x.e \Leftarrow A \rightarrow B}{\Delta}}\) →I \(\quad\quad\) \(\frac{\expr{\Gamma,\alpha}{e \Leftarrow A}{\Delta,\alpha,\Theta}}{\expr{\Gamma}{e \Leftarrow \forall \alpha . A}{\Delta}}\) ∀I \(\quad\quad\) \(\frac{\expr{\Gamma}{e \Rightarrow A}{\Theta} \quad\quad \expr{\Theta}{[\Theta]A\ <:\ [\Theta]B}{\Delta}}{\expr{\Gamma}{e \Leftarrow B}{\Delta}}\) Sub \(\quad\quad\)
\(\text{check} :: \Gamma \rightarrow e \rightarrow A \rightarrow (\Delta, B)\)

Table 5. derive
\(\frac{\expr{\Gamma[\ea_2,\ea_1,\ea=\ea_1 \rightarrow \ea_2]}{e \Leftarrow\ \ea_1}{\Delta}}{\expr{\Gamma[\ea]}{\ea\ \bullet\ e \Rightarrow\Rightarrow \ea_2}{\Delta}}\) \(\ea\)App \(\quad\quad\) \(\frac{\expr{\Gamma,\ea}{[\ea/\alpha]A\ \bullet\ e \Rightarrow\Rightarrow C}{\Delta}}{\expr{\Gamma}{\forall\alpha . A\ \bullet\ e \Rightarrow\Rightarrow C}{\Delta}}\) ∀App \(\quad\quad\) \(\frac{\expr{\Gamma}{e \Leftarrow A}{\Delta}}{\expr{\Gamma}{A \rightarrow C\ \bullet\ e \Rightarrow\Rightarrow C}{\Delta}}\) →App \(\quad\quad\)
\(\text{derive} :: \Gamma \rightarrow e \rightarrow A \rightarrow (\Delta, B)\)

References

J. Dunfield & N. R. Krishnaswami, Complete and easy bidirectional typechecking for higher-rank polymorphism. ACM SIGPLAN Notices (ACM, 2013), pp. 429–442.
D. Vytiniotis, S. Peyton Jones, & T. Schrijvers, Let should not be generalized. Proceedings of the 5th ACM SIGPLAN workshop on Types in language design and implementation (ACM, 2010), pp. 39–50.