Раздел 2 · Программирование / CS

Типы и системы типов: фундамент

junior~50 мин

без входаВойди, чтобы отмечать прогресс, вести заметки и решать задачи в редакторе. войти

Типы и системы типов: фундамент

Представь: ты уже готов обсуждать монады, парсеры и персистентные структуры. Но прежде чем углубляться, нужно договориться о базе: что такое тип, зачем языку система типов и какими словами про неё разговаривать, чтобы тебя понимали. Слова «строгая типизация» и «слабая типизация» в интернете означают что угодно; после этого урока ты будешь различать четыре независимые оси и перестанешь путать их в обсуждениях.

У урока есть вторая нить, и она важнее словаря. Типы прежде всего служат инструментом проектирования, а не синтаксисом. Эту мысль мы возьмём у двух классических книг, SICP и How to Design Programs: первая учит строить барьеры абстракции, вторая учит проектировать данные раньше кода. Обе написаны для языков, где статической проверки типов нет вообще, и именно поэтому они так хорошо показывают, что типы живут в голове проектировщика, а компилятор лишь помогает их не терять. Дальше этот словарь работает везде: в разделе про TypeScript он уже используется, а в ФП-серии на него ложатся алгебраические типы и функции.

Что такое тип и система типов

Тип классифицирует данные и определяет две вещи:

· множество допустимых значений: number включает все числа, литерал 'idle' содержит ровно одну строку; · множество допустимых операций над этими значениями: для чисел доступна арифметика, для строк доступна конкатенация.

Система типов задаёт правила, по которым язык назначает типы конструкциям программы (выражениям, переменным, функциям) и проверяет их согласованность.

У системы типов четыре главные задачи. Давай разберём каждую на коротком примере.

Безопасность (Safety)

Предотвращение целых классов ошибок до того, как они случились. Формулировка Робина Милнера: well-typed programs don’t go wrong.

type User = { email: string | null };

const shout = (user: User) => user.email.toUpperCase();
// ошибка компиляции: email может быть null

const shoutSafe = (user: User) =>
  user.email === null ? '' : user.email.toUpperCase();

Заметь: исчезает не одна ошибка, а целый класс. «Вызвал метод у null» в строго проверяемом коде невозможен, сколько бы новых функций ты ни написал.

Абстракция

Детали реализации прячутся за интерфейсом типа. Снаружи ты видишь только контракт: какие операции доступны. Как значение устроено внутри, знать не нужно, и это не вежливость, а гарантия: внутренности можно поменять, не сломав пользователей. Эта задача настолько важна, что ей посвящён следующий раздел целиком.

Документация

Сигнатура функции служит машинно-проверяемой спецификацией. Комментарий устаревает в первый же рефакторинг, сигнатура устареть не может: компилятор не даст.

const parsePrice = (raw: string): { ok: true; value: number } | { ok: false; reason: string } => {
  const value = Number(raw);
  return Number.isFinite(value)
    ? { ok: true, value }
    : { ok: false, reason: `не число: ${raw}` };
};

Из одной строки сигнатуры читается всё: функция принимает сырую строку, может не справиться, и в случае неудачи объяснит причину. Ни одного комментария не понадобилось.

Оптимизация

Компилятор использует знание типов, чтобы генерировать более эффективный код: число известного размера кладётся в регистр, поле структуры находится по фиксированному смещению без поиска по имени. Есть нюанс про наш стек: типы TypeScript стираются при компиляции, движок JS их не видит и оптимизирует по собственным скрытым классам. Но сама задача никуда не делась, просто в JS её решает JIT в рантайме, а в Rust или Go компилятор заранее.

Абстракция: барьеры из SICP

SICP формулирует идею, на которой стоит всё проектирование: барьер абстракции. Покажем на классическом примере книги, рациональных числах. Дробь нельзя честно представить как number, точность утечёт, поэтому строим свой тип: конструктор и два селектора.

type Rational = { numerator: number; denominator: number };

const makeRational = (numerator: number, denominator: number): Rational => {
  const divisor = gcd(numerator, denominator);
  return { numerator: numerator / divisor, denominator: denominator / divisor };
};

const numer = (r: Rational) => r.numerator;
const denom = (r: Rational) => r.denominator;

const addRational = (a: Rational, b: Rational) =>
  makeRational(numer(a) * denom(b) + numer(b) * denom(a), denom(a) * denom(b));

const mulRational = (a: Rational, b: Rational) =>
  makeRational(numer(a) * numer(b), denom(a) * denom(b));

Программа выстроилась слоями, и между слоями стоят барьеры:

УровеньЧем пользуется
программы про дробиaddRational, mulRational
арифметика дробейmakeRational, numer, denom
представлениеобъект с двумя полями

Код выше барьера никогда не лезет в .numerator напрямую. Зачем такая дисциплина? Затем, что представление теперь можно менять свободно. Сейчас дробь сокращается в конструкторе. Захотелось сокращать лениво, при чтении? Переносим gcd в селекторы, и ни одна строка выше барьера не меняется. В этом весь смысл: барьер локализует решение, а значит и будущие изменения.

SICP доводит мысль до предела: данные вообще не обязаны быть «структурой». Пара значений прекрасно живёт внутри замыкания:

type Pair<A, B> = <R>(selector: (first: A, second: B) => R) => R;

const cons = <A, B>(first: A, second: B): Pair<A, B> =>
  (selector) => selector(first, second);

const car = <A, B>(pair: Pair<A, B>) => pair((first) => first);
const cdr = <A, B>(pair: Pair<A, B>) => pair((_, second) => second);

Здесь нет ни объекта, ни массива, только функция, но car(cons(1, 2)) честно возвращает 1. Вывод, который стоит запомнить: данные определяются контрактом (что обещают конструкторы и селекторы), а не представлением. Тип формально записывает этот контракт.

Из SICP же приходит приём мечтательного проектирования: пиши addRational так, будто makeRational уже существует, и интерфейс нижнего уровня спроектируется сам, по реальным потребностям верхнего.

Последнее наблюдение: языки строят барьеры по-разному, и это нормально. Java прячет представление за private в классе, OCaml за сигнатурой модуля, Scheme за замыканием, Go за маленькой буквой в имени поля. В TypeScript барьер чаще всего держится на дисциплине экспорта: модуль экспортирует конструктор и операции, но не само представление. Механизм разный, идея одна, и в уроке про ООП мы увидим, что инкапсуляция воплощает ту же идею.

Звучность (Soundness)

Система типов называется звуковой (sound), если она гарантирует: если программа прошла проверку типов, то в ней не будет ошибок времени выполнения указанного класса. Несозвучная (unsound) система может пропустить ошибки, которые проявятся в рантайме.

TypeScript, например, сознательно допускает несколько источников unsoundness (см. «The Seven Sources of Unsoundness in TypeScript» из ресурсов). Это цена за удобство и совместимость с JS. Звуковая система, напротив, даёт математическую гарантию: ты можешь полагаться на неё при проектировании.

Рецепт HtDP: данные раньше кода

«How to Design Programs» учит: сначала определи структуру данных, потом пиши функции над ней. Структура функции повторяет структуру данных.

Возьмём пример из раздела про алгебру типов: RemoteData<T>. Сначала мы описали все возможные состояния как сумму: idle, loading, success, error. Затем написали render, который покрывает все случаи через исчерпывающий switch.

Этот подход называется «Make illegal states unrepresentable»: спроектируй типы так, чтобы некорректное состояние нельзя было даже сконструировать. Тогда проверки на корректность не нужны: некорректных значений не существует. Принцип вернётся в уроке про типы и ошибки и в моделировании с FSM.

В нетипизированном Racket это была дисциплина проектирования; в TS это синтаксис и проверка. ADT существует как дисциплина даже в языке без типов; типизированный язык лишь материализует её.

Что такое абстракция на самом деле

Слово «абстракция» звучит в каждом втором обсуждении кода, и при этом авторитетные авторы не могут договориться даже о базовом. Олаф Тилке пишет «interfaces are abstractions», Марк Симан в «Code That Fits in Your Head» отвечает «interfaces are not abstractions», Эрик Эллиотт определяет абстракцию как «поиск похожих кусков кода и вынос общей логики в именованный компонент». Три определения, три разных вещи. Спор «что хуже, дублирование или неправильная абстракция» без общего определения превращается в спор о вкусах.

Четыре оси систем типов

Типы и их системы можно анализировать по четырём независимым осям:

· Статика и динамика: когда проверяется тип, при компиляции или в рантайме? · Сильная и слабая: насколько строги правила совместимости типов? · Sound и unsound: гарантирует ли система отсутствие ошибок определённого класса? · Номинативная и структурная: как сравниваются типы, по имени или по структуре?

Эти оси независимы: система может быть статической и unsound, или динамической и sound. Понимание осей поможет тебе избегать путаницы в обсуждениях.

дальше после входа

Урок целиком открыт всем, кто вошёл. Войди по своему email, чтобы читать дальше.

Вход пока по приглашению. Если хочешь учиться, напиши Vassiliy.