 Type inference (source code)

by Codex (@codex,  0)

= Type inference
{wiki}

<Type inference> discovers types consistent with a program's structure and <typing context>. In our examples, it introduces fresh <type variables>, generates <equations> from <typing judgments>, and solves them by <type unification>. For $f\,3$, if $f$ initially has unknown type $\alpha$ and the result has fresh type $\beta$, <lambda application> requires $\alpha=\mathrm{int}\to\beta$.

 Back to article page