RISE Type System

Well-formed Types

Kinds

$\kappa ::= \mathsf{type} \mid \mathsf{data} \mid \mathsf{nat} \mid \mathsf{nat}\hspace{-.25em}\rightarrow\hspace{-.25em}\mathsf{data} \mid \mathsf{nat}\hspace{-.25em}\rightarrow\hspace{-.25em}\mathsf{nat} \mid \mathsf{addrSpace}$

Kinding Structural Rule

$\cfrac{x : \kappa \in \Delta}{\Delta \vdash x : \kappa}$

Type Equality

$\cfrac{\models \forall \sigma : \mathit{dom}(\Delta) \to \mathbb{N} . \sigma(N) = \sigma(M)}{\Delta \vdash N \equiv M : \mathsf{nat}}$

Address Spaces

$\cfrac{A \in \{\mathsf{global}, \mathsf{local}, \mathsf{private}, \mathsf{constant}\}}{\Delta \vdash A : \mathsf{addrSpace}}$

Nat to Nat Type Level Functions

$\cfrac{\Delta, n : \mathsf{nat} \vdash M : \mathsf{nat}}{\Delta \vdash n \mapsto M : \mathsf{nat}\hspace{-.25em}\rightarrow\hspace{-.25em}\mathsf{nat}}$

Nat to Data Type Level Functions

$\cfrac{\Delta, n : \mathsf{nat} \vdash T : \mathsf{data}}{\Delta \vdash n \mapsto T : \mathsf{nat}\hspace{-.25em}\rightarrow\hspace{-.25em}\mathsf{data}}$

Natural numbers

$\cfrac{}{\Delta \vdash \underline{\ell} : \mathsf{nat}}\qquad \cfrac{\Delta \vdash N : \mathsf{nat} \quad \Delta \vdash M : \mathsf{nat} \quad \oplus \in \{+, *, \ldots\}}{\Delta \vdash N \oplus M : \mathsf{nat}}\\[1em] \cfrac{\Delta \vdash F_N : \mathsf{nat}\hspace{-.25em}\rightarrow\hspace{-.25em}\mathsf{nat} \quad \Delta \vdash M : \mathsf{nat}}{\Delta \vdash F_N\ M : \mathsf{nat}}$

Data Types

$\cfrac{}{\Delta \vdash \mathsf{scalar} : \mathsf{data}}\qquad \cfrac{}{\Delta \vdash \mathsf{natType} : \mathsf{data}}\qquad \cfrac{\Delta \vdash N : \mathsf{nat}}{\Delta \vdash \mathsf{idx}[N] : \mathsf{data}}\\[1em] \cfrac{\Delta \vdash N : \mathsf{nat} \qquad \Delta \vdash T : \mathsf{data}}{\Delta \vdash \mathsf{vec}[T, N] : \mathsf{data}}\\[1em] \cfrac{\Delta \vdash S : \mathsf{data} \quad \Delta \vdash T : \mathsf{data}}{\Delta \vdash (S,\ T) : \mathsf{data}}\\[1em] \cfrac{\Delta \vdash N : \mathsf{nat} \quad \Delta \vdash T : \mathsf{data}}{\Delta \vdash N_\bullet T : \mathsf{data}}\\[1em] \cfrac{\Delta, n : \mathsf{nat} \vdash T : \mathsf{data}}{\Delta \vdash (n: \mathsf{nat}\ \ast\ast\ T) : \mathsf{data}}\\[1em] \cfrac{\Delta \vdash N : \mathsf{nat} \quad \Delta \vdash F_T : \mathsf{nat}\hspace{-.25em}\rightarrow\hspace{-.25em}\mathsf{data}}{\Delta \vdash N_{\bullet\bullet} F_T : \mathsf{data}}\\[1em] \cfrac{\Delta \vdash F_T : \mathsf{nat}\hspace{-.25em}\rightarrow\hspace{-.25em}\mathsf{data} \quad \Delta \vdash N : \mathsf{nat}}{\Delta \vdash F_T\ N : \mathsf{data}}$

Types

$\cfrac{\Delta \vdash T : \mathsf{data}}{\Delta \vdash T : \mathsf{type}}\qquad \cfrac{\Delta \vdash \theta_1 : \mathsf{type} \quad \Delta \vdash \theta_2 : \mathsf{type}}{\Delta \vdash \theta_1 \rightarrow \theta_2 : \mathsf{type}}\\[1em] \cfrac{\Delta, x : \kappa \vdash \theta : \mathsf{type} \qquad \kappa \in \{\mathsf{addrSpace}, \mathsf{nat}\hspace{-.25em}\rightarrow\hspace{-.25em}\mathsf{nat}, \mathsf{nat}\hspace{-.25em}\rightarrow\hspace{-.25em}\mathsf{data}, \mathsf{nat}, \mathsf{data}\}}{\Delta \vdash (x: \kappa) \rightarrow \theta : \mathsf{type}}$

Typing Rules

Structural Rules

$\cfrac{x : \theta \in \Gamma}{\Delta \mid \Gamma \vdash x : \theta}\qquad \cfrac{\Delta \mid \Gamma \vdash E : \theta_1 \quad \Delta \vdash \theta_1 \equiv \theta_2 : \mathsf{type}}{\Delta \mid \Gamma \vdash E : \theta_2}\qquad \cfrac{\mathsf{prim} : \theta \in \mathsf{Primitives}}{\Delta \mid \Gamma \vdash \mathsf{prim} : \theta}$

Introduction and Elimination Rules

$\cfrac{\Delta \mid \Gamma, x : \theta_1 \vdash E : \theta_2}{\Delta \mid \Gamma \vdash \lambda x. E : \theta_1 \rightarrow \theta_2}\qquad \cfrac{\Delta \mid \Gamma_1 \vdash E_1 : \theta_1 \rightarrow \theta_2 \quad \Delta \mid \Gamma_2 \vdash E_2 : \theta_1}{\Delta \mid \Gamma_1, \Gamma_2 \vdash E_1\ E_2 : \theta_2}\\[1em] \cfrac{\Delta, x : \kappa \mid \Gamma \vdash E : \theta \quad x \not\in ftv(\Gamma)}{\Delta \mid \Gamma \vdash \Lambda x. E : (x: \kappa) \rightarrow \theta}\qquad \cfrac{\Delta \mid \Gamma \vdash E : (x: \kappa) \rightarrow \theta \quad \Delta \vdash \tau : \kappa}{\Delta \mid \Gamma \vdash E\ \tau : \theta[\tau/x]}$