\[ \newcommand{\target}[2]{\class{mathjax-symbol mathjax-symbol-#1}{#2}} \newcommand{\type}[3]{#1 \target{type}{\vdash} #2 \target{type}{:} #3} \newcommand{\abs}[3]{\target{abs}{\lambda} #1 \target{abs}{:} #2\target{abs}{.} #3} \newcommand{\tabs}[2]{\target{tabs}{\Lambda} #1 \target{tabs}{.} #2} \newcommand{\arrow}{\target{arrowT}{\rightarrow}} \newcommand{\subt}{\target{subT}{<:}} \newcommand{\Int}{\mathsf{Int}} \newcommand{\Bool}{\mathsf{Bool}} \newcommand{\lett}[3]{\mathsf{let}\ \mathit{#1} : #2 = #3\ \mathsf{in}} \newcommand{\letu}[2]{\mathsf{let}\ \mathit{#1} = #2\ \mathsf{in}\ } \newcommand{\ite}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3} \DeclareMathOperator{\proj}{.} \newcommand{\object}[1]{\mathsf{object}\ #1\ \mathsf{end}} \newcommand{\call}[2]{#1 \# \mathit{#2}} \newcommand{\method}[2]{\mathsf{method}\ \mathit{#1} = #2} \newcommand{\self}{\mathit{self}} \newcommand{\super}{\mathit{super}} \newcommand{\refc}{\mathsf{ref}\ } \newcommand{\inherit}[2]{\mathsf{inherit}\ #1\ \mathsf{as}\ \mathit{#2}} \newcommand{\pack}[3]{\mathsf{pack}\ (#1, #2)\ \mathsf{as}\ #3} \newcommand{\unpack}[4]{\mathsf{unpack}\ (#1, #2) = #3\ \mathsf{in}\ #4} \newcommand{\override}{\ \mathsf{override}\ } \newcommand{\loc}[1]{l_{#1}} \]
Typing relation. Usually written \(\type{\Gamma}{e}{\tau}\), where \(\Gamma\) is a map from identifiers to types, \(e\) is an expression, and \(\tau\) is a type.
\(\type{\mathrm{Type Context}}{\mathrm{Expression}}{\mathrm{Type}}\)
Anonymous function.
\(\abs{\mathrm{Parameter Name}}{\mathrm{Parameter Type}}{\mathrm{Body}}\)
Type abstraction.
\(\tabs{\mathrm{Type Variable}}{\mathrm{Body}}\)
Function type.
\(\mathrm{Parameter Type} \arrow \mathrm{Return Type}\)
Subtyping relation.
Read \(\tau \subt \tau'\) as: \(\tau\) is a subtype of \(\tau'\). If \(\tau\) and \(\tau'\) are records, \(\tau\) has a superset of the fields in \(\tau'\). Alternatively, anything that expects a \(\tau'\) can take a \(\tau\).
| Construct | Notation | Python |
|---|---|---|
| Variable | \(x\) | Var('x') |
| Integer literal & type | \(n \qquad \Int\) | Int(n) IntT() |
| Boolean literal & type | \(b \qquad \Bool\) | Bool(b) BoolT() |
| Application | \(e_{1}\ e_{2}\) | App(e1, e2) |
| Abstraction & type | \(\lambda x:\tau. e \qquad \tau_1 \rightarrow \tau_2\) | Lam(x, t, e) ArrowT(t1, t2) |
| Conditional | \(\ite{e_{1}}{e_2}{e_3}\) | If(e1, e2, e3) |
| Operator | \(e_1 \oplus e_2\) | Prim(op, [e1, e2]) |
| Type abstraction & type | \(\Lambda \alpha. e \qquad \forall \alpha. \tau\) | TypeAbs('a', e) ForallT('a', t) |
| Type application | \(e[\tau]\) | TypeApp(e, t) |
| Record & type | \(\{{x_i = e_i}^{i \in 1\dots n}\} \qquad \{{x_i = \tau_i}^{i \in 1\dots n}\}\) | Record({x1 = e1, ..., xn = en}) RecordT({x1 = t1, ..., xn = tn}) |
| Field access | \(e \proj x\) | Proj(e, 'x') |
| Type variable | \(\alpha\) | VarT('a') |
| Top type | \(\top\) | TopT() |
| Existential type | \(\exists \alpha. \tau\) | ExistsT("a", t) |
| Existential packing | \(\pack{\tau_{hidden}}{e}{\tau_{intf}}\) | Pack(t_hidden, e, t_intf) |
| Existential unpacking | \(\unpack{\alpha}{m}{e_{1}}{e_2}\) | Unpack("m", "a", e1, e2) |