$$<math>{
\begin{array}{lccl}
\text{Identifiers（識別子）} & x &     & \\
\text{Expressions（式）} & e & ::= & x\\
                   &   & |   & e_0 \enspace e_1\\
                   &   & |   & \lambda x . e\\
                   &   & |   & \textbf{let} \enspace x = e_0 \enspace \textbf{in} \enspace e_1\\
                   &   & |   & \textbf{over} \enspace x :: \sigma \enspace \textbf{in} \enspace e\\
                   &   & |   & \textbf{inst} \enspace x :: \sigma = e_0 \enspace \textbf{in} \enspace e_1\\
\text{Type Variables（型変数）} & \alpha & & \\
\text{Type Constructors（型構築子）} & \chi & & \\
\text{Types（型）} & \tau & ::= & (\tau \rightarrow \tau ') \enspace | \enspace \alpha \enspace | \enspace \chi (\tau_1 \cdots \tau_n )\\
\text{Predicated Types（述語付きの型）} & \rho & ::= & (x :: \tau) . \rho \enspace | \enspace \tau\\
\text{Type-schemes（型スキーム）} & \sigma & ::= & \forall \alpha . \sigma \enspace | \enspace \rho
\end{array}
$$}