1.1.1 — фундамент теории языков1.1.1 — the foundation of language theory
λ-исчисление — минимальная формальная модель вычислений, состоящая только из определения и применения функций. Системы типов накладывают на эту модель дисциплину, которая отсекает бессмысленные программы ещё до их запуска — от этого выбора зависит, что вообще значит «корректная программа» в конкретном языке.Lambda calculus is a minimal formal model of computation built from nothing but function definition and application. Type systems impose a discipline on top of that model which rules out meaningless programs before they ever run — that choice shapes what "a correct program" even means in a given language.
λ-исчисление (Alonzo Church, 1930-е) — система записи из трёх конструкций: переменная x, абстракция λx.M (функция, берущая x и возвращающая M) и применение M N (вызов M с аргументом N). Всё остальное — числа, булевы значения, рекурсия, структуры данных — кодируется через эти три конструкции. Это не игрушечная модель: это доказанный Тьюринг-полный фундамент, на котором стоит семантика каждого функционального языка.Lambda calculus (Alonzo Church, 1930s) is a notation built from three constructs: a variable x, an abstraction λx.M (a function taking x and returning M), and an application M N (calling M with argument N). Everything else — numbers, booleans, recursion, data structures — is encoded through just these three. This isn't a toy model: it's a proven Turing-complete foundation that the semantics of every functional language rest on.
Система типов — набор правил, приписывающих выражениям типы и отклоняющих выражения, для которых типы не сходятся (1 + "a"). Просто типизированное λ-исчисление (Church, 1940) добавляет к бестиповому ядру аннотации типов и правило: применение M N допустимо только если тип M — это функция из типа N. Ключевое следствие: в просто типизированном λ-исчислении невозможно закодировать неограниченную рекурсию — оно строго слабее бестипового варианта по вычислительной мощности (не Тьюринг-полное), но зато гарантированно завершается (strong normalization).A type system is a set of rules that assigns types to expressions and rejects expressions whose types don't line up (1 + "a"). Simply-typed lambda calculus (Church, 1940) adds type annotations to the untyped core plus one rule: an application M N is only valid if the type of M is a function from the type of N. Key consequence: simply-typed lambda calculus cannot encode unbounded recursion — it is strictly weaker than the untyped version in computational power (not Turing-complete), but in exchange it's guaranteed to terminate (strong normalization).
Формулировка: типы — это утверждения, программы — это доказательства (propositions as types, proofs as programs). Тип функции A → B соответствует логической импликации «из A следует B»; написать функцию с этой сигнатурой и предъявить доказательство импликации — формально одна и та же задача. Тип-произведение (A, B) — это конъюнкция «A и B», тип-сумма A | B — дизъюнкция «A или B».The statement: types are propositions, programs are proofs. A function type A → B corresponds to the logical implication "A implies B"; writing a function with that signature and producing a proof of the implication are, formally, the same task. A product type (A, B) is the conjunction "A and B"; a sum type A | B is the disjunction "A or B".
Если функция компилируется с сигнатурой (a: A, b: B) -> A, тайпчекер только что проверил доказательство тривиальной теоремы «A и B влечёт A». Языки с зависимыми типами (Idris, Agda, Coq) доводят эту идею до предела: там можно закодировать в типе произвольное математическое утверждение и заставить компилятор отказаться собирать код, пока утверждение не доказано телом функции.If a function compiles with the signature (a: A, b: B) -> A, the typechecker has just verified a proof of the trivial theorem "A and B implies A." Dependently-typed languages (Idris, Agda, Coq) push this to its limit: you can encode an arbitrary mathematical statement in a type and force the compiler to refuse to build until the function body proves it.
Ось независима от «сильная/слабая» типизации (это про то, разрешены ли неявные конверсии). Статическая/динамическая — это про момент проверки типов.This axis is independent from "strong vs weak" typing (which is about whether implicit conversions are allowed). Static vs dynamic is about the point in time when types are checked.
Типы проверяются на этапе компиляции; несовпадение — ошибка компиляции, до запуска программы. Тип каждой переменной известен статически, даже если выведен через let без аннотации.Types are checked at compile time; a mismatch is a compile error, before the program ever runs. Every variable's type is known statically, even when inferred through an unannotated let.
let x: i32 = 5;
let y: &str = "5";
// x + y — ошибка компиляции, типы не совпадают// x + y — a compile error, the types don't matchТип привязан к значению, а не к переменной, и проверяется в момент выполнения операции. Одна и та же строка кода может упасть или отработать в зависимости от того, что реально передали в рантайме.The type belongs to the value, not the variable, and is checked at the moment the operation executes. The exact same line of code can crash or succeed depending on what was actually passed in at runtime.
def add(x, y):
return x + y
add(2, 3) # 5 — работает# 5 — works
add(2, "3") # TypeError — только в момент вызова# TypeError — only at call timeКомпромисс: статические аннотации проверяются компилятором (tsc), но стираются при компиляции в JS — на рантайме типов не существует вообще, и any в любой момент выключает проверку локально.A compromise: static annotations are checked by the compiler (tsc), but they're erased when compiling down to JS — at runtime, types don't exist at all, and any can locally switch off checking at any point.
function add(x: number, y: number): number {
return x + y;
}
add(2, "3"); // ошибка tsc, но JS ниже всё равно выполнит "23"// tsc error, but the underlying JS would still happily produce "23"C — статически типизированный язык, но void*-касты и неявные конверсии делают его типовую систему дырявой. Статическая типизация гарантирует только момент проверки, а не её полноту — за строгость отвечает отдельная ось (сильная/слабая типизация).C is statically typed, but void* casts and implicit conversions make its type system leaky. Static typing only guarantees the timing of the check, not how thorough it is — strictness is a separate axis (strong vs weak typing).
Частая ошибка — считать, что добавление типов к λ-исчислению ничего не меняет в мощности модели. На деле типизация запрещает самоприменение x x (нужно было бы, чтобы тип x был одновременно и аргументом, и функцией над самим собой), а вместе с ним — комбинатор неподвижной точки Y и неограниченную рекурсию.A common mistake is assuming that adding types to lambda calculus doesn't change the model's power. In fact, typing forbids self-application x x (which would require x's type to be simultaneously its own argument and a function over itself), and with it, the Y fixed-point combinator and unbounded recursion.
Duck typing («если крякает как утка») — это про структурную совместимость (наличие метода/поля), а динамическая типизация — про момент проверки. Go и TypeScript структурно типизированы, но статически; Python и Ruby структурны и динамичны одновременно — это две независимые оси, которые часто путают.Duck typing ("if it quacks like a duck") is about structural compatibility (having the right method/field), while dynamic typing is about the timing of the check. Go and TypeScript are structurally typed but static; Python and Ruby are structural and dynamic at the same time — these are two independent axes that get conflated often.