appendix sectionnotation

Hindley–Milner inference

symbol	meaning	owner
symbol	meaning	owner
$τ, σ$	monotype and rank-one type scheme	chapter 3
$σ ≽ τ$	$τ$ is one monotype instance of $σ$	definition 3.8
$σ_{1} ⊒ σ_{2}$	every instance of $σ_{2}$ is an instance of $σ_{1}$	definition 3.8
$ftv (a)$	free type variables of a type, scheme, substitution, or context	chapter 3
${Gen}_{Γ} (τ)$	quantify exactly the variables of $τ$ not fixed by $Γ$	definition 3.12
$τ [S], σ [S], Γ [S]$	postfix action of a finite type substitution	definition 3.5
$S; T$	right-action composition: first $S$ , then $T$	definition 3.5
$S =_{X} T$	substitutions agree on the finite variable set $X$	definition 3.5
$E = (τ_{i} ≐ ρ_{i})_{i}$	ordered finite type-equation work list	definition 3.20
$unify (E)$	deterministic substitution-based most-general unifier	definition 3.22
$Γ ⊢_{c} e : τ ∣ E$	let-free constraint generation with provisional type $τ$	section 3.3
$Γ ⊢_{s} e : τ$	syntax-directed HM typing	definition 3.31
$Θ; Γ ⊢_{ev} d : τ$	checking an explicitly instantiated HM evidence term	definition 4.51
$W (Γ, e) = (S, τ)$	Algorithm W result: substitution and principal monotype	definition 3.28
$Γ ⊢_{Σ} e : σ$	run-time typing relative to store typing $Σ$	definition 4.68
$(μ, e) ⟶ (μ^{'}, e^{'})$	one store-configuration transition	definition 4.68