Здесь все с пары 2021 года, если есть что-то интересное добавить, то не стесняйтесь. Также вроде как на википедии умные вещи написаны, чисто выебнуться пойдет.
<aside> 💡 Вывод типов (type inference, type reconstruction) — процедура построения по данному выражению его типа.
</aside>
<aside> 💡 Проверка типов (type checking) — процедура проверки, что данное выражение можно протипизровать данным типом. когда некоторым частям тип приписан
</aside>
очень часто это один и тот же алгоритм.
язык типoв STLC:
$\texttt{⟨typ⟩ ∶∶= ⟨typ⟩ →⟨typ⟩ ∣ (⟨typ⟩) ∣ 𝑇}$
где $T \in G = \{\iota, \kappa, int, string, ...\}$ — ground типы (листы абстрактного синтаксического дерева языка типов)
полиморфмизма нет да да не удивляйтесь
Ниже на картинке выводим снизу вверх.