BatSchool · Алгебраические типы

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

Это и есть тема урока. В прошлом уроке функции научились работать в двух видах, а здесь разговор о данных, которые эти функции принимают. У типа есть число значений, и его можно посчитать почти школьной арифметикой. Когда число значений типа больше числа настоящих состояний, лишние значения кто-нибудь однажды создаст.

Два флажка

Вот тип Ринцвальда:

type FrameState = {
  readonly frame: number;
  readonly sent: boolean;
  readonly acked: boolean;
  readonly sentAt?: number;
  readonly ackedAt?: number;
};

const ghost: FrameState = { frame: 40, sent: false, acked: false };
const liar: FrameState = { frame: 41, sent: false, acked: true, sentAt: 100 };

Оба значения собираются. ghost это кадр, которого никто не отправлял и никто не подтверждал, но запись о нём есть. liar подтверждён и при этом не отправлен, зато у него есть момент отправки. Ни того, ни другого башня не видела, но тип разрешает оба, и функция, которая читает FrameState, обязана что-то с ними делать. Обычно она делает что попало.

Сколько значений у типа

Посчитаем, как Матушка на пальцах. У boolean два значения. У литерала 'sent' одно. У 'sent' | 'acked' два. Число значений типа называют его мощностью.

Объект с двумя полями boolean это пара: первое поле выбирается независимо от второго, поэтому вариантов 2 × 2 = 4. Каждое новое независимое поле умножает число значений, и такой тип называют произведением. Объединение работает иначе: значение берётся из одного члена или из другого, и мощности складываются. Такой тип называют суммой.

type Kind = 'sent' | 'acked'; // 1 + 1 = 2
type Flags = { readonly sent: boolean; readonly acked: boolean }; // 2 × 2 = 4
type Fate = 'pending' | 'confirmed' | 'phantom'; // 1 + 1 + 1 = 3

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

У number значений слишком много, чтобы их перечислять, но формулы работают и с ним. Необязательное поле sentAt?: number это number плюс один случай «поля нет». В типе Ринцвальда получается 2 × 2 × (N + 1) × (N + 1) на каждый номер кадра, где N это число моментов времени. Настоящих состояний у кадра три: ждёт, подтверждён, призрак. Всё остальное это ghost, liar и их родня.

Одна судьба

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

export type Pending = { readonly _tag: 'Pending'; readonly frame: number; readonly sentAt: number };
export type Confirmed = {
  readonly _tag: 'Confirmed';
  readonly frame: number;
  readonly sentAt: number;
  readonly ackedAt: number;
};
export type Phantom = { readonly _tag: 'Phantom'; readonly frame: number; readonly ackedAt: number };
export type Delivery = Pending | Confirmed | Phantom;

Это размеченное объединение из урока 07, только теперь видно, почему оно хорошее. Внутри каждого варианта поля обязательные: подтверждённому кадру нужны оба момента, ждущему только момент отправки, у призрака отправки не было вовсе. Посчитаем: N + N × N + N на номер кадра. Ни ghost, ни liar в эту формулу не помещаются. Невозможное состояние стало непредставимым.

Такую судьбу читают без проверок, у каждого варианта все его поля на месте:

import type { Delivery } from './journal';

const describe = (delivery: Delivery): string => {
  switch (delivery._tag) {
    case 'Pending':
      return `кадр ${delivery.frame}: ждёт ответа`;
    case 'Confirmed':
      return `кадр ${delivery.frame}: ответ через ${delivery.ackedAt - delivery.sentAt} мс`;
    case 'Phantom':
      return `кадр ${delivery.frame}: призрак`;
  }
};

В ветке Confirmed вычитание ackedAt - sentAt не требует ни ?? 0, ни !: оба числа на месте, потому что подтверждённый кадр без них не создать. Проверку, которую Ринцвальд размазал бы по каждому месту чтения, тип сделал один раз, в момент создания.

Перевод с Ук

Попробуй записать подтверждение без момента ответа:

import type { Delivery } from './journal';

const lie: Delivery = { _tag: 'Confirmed', frame: 41, sentAt: 100 };

lie.ts(3,7): error TS2322: Type '{ _tag: "Confirmed"; frame: number; sentAt: number; }' is not assignable to type 'Delivery'.
  Property 'ackedAt' is missing in type '{ _tag: "Confirmed"; frame: number; sentAt: number; }' but required in type 'Confirmed'.

Читаем снизу. Нижняя строка уже назвала вариант: Confirmed. Компилятор увидел _tag: "Confirmed" и сверил объект не со всем объединением, а с одним членом, как в уроке 07. В этом члене поле ackedAt обязательное, а в объекте его нет. Верхняя строка говорит то же целиком: объект не помещается в Delivery. Подтверждение без момента подтверждения не собирается, и это не придирка, а ровно то, чего добивалась Матушка.

Похожая ошибка будет, если дать призраку момент отправки: 'sentAt' does not exist in type 'Phantom'. Лишнее поле так же запрещено, как недостающее.

Под капотом

Ноль для сложения это never, тип без значений. Прибавь его к любому типу, и ничего не изменится:

const n: number | never = 'x';

never.ts(1,7): error TS2322: Type 'string' is not assignable to type 'number'.

В сообщении стоит number, а не number | never: компилятор сам выбросил пустое слагаемое. Поэтому в уроке 13 ошибки двух задач E | never складывались в E, а задача без ошибок подходила куда угодно.

Единица для умножения это тип с одним значением, например литерал. Тег _tag: 'Pending' умножает мощность варианта на один: { _tag: 'Pending'; frame; sentAt } содержит столько же значений, сколько пара [frame, sentAt]. Тег не добавляет состояний, он их подписывает. Поэтому размеченное объединение ничего не стоит по сравнению с «голой» суммой, а различать варианты становится можно.

Как судьба меняется

Судьба кадра складывается из записей журнала по порядку. Первая запись решает, кем кадр начинает: отправка даёт Pending, подтверждение без отправки даёт Phantom. Дальше переход один: ждущий кадр, на который пришло подтверждение, становится Confirmed.

Было	Пришло	Стало
ничего	отправка в `at`	`Pending`, `sentAt = at`
ничего	подтверждение в `at`	`Phantom`, `ackedAt = at`
`Pending`	подтверждение в `at`	`Confirmed`, `sentAt` прежний, `ackedAt = at`
`Pending`	повторная отправка	без изменений: первая отправка остаётся
`Confirmed` или `Phantom`	что угодно	без изменений

Последняя строка стоит внимания. Подтверждение, пришедшее раньше отправки, уже сделало кадр призраком, и поздняя отправка его не оправдывает: в момент подтверждения кадра не было. Так же считает phantomAcks из урока 17, и две функции не спорят друг с другом.

Таблицу тоже можно посчитать. «Было» бывает четырёх видов (ничего и три судьбы), «пришло» двух, пар восемь. Последняя строка сжимает четыре пары в одну, но ни одну не пропускает, и из каждой пары ведёт ровно одна дорога.

Где тут дыра

type Status = {
  readonly status: 'pending' | 'confirmed' | 'phantom';
  readonly frame: number;
  readonly sentAt?: number;
  readonly ackedAt?: number;
};

const delay = (s: Status): number => (s.ackedAt ?? 0) - (s.sentAt ?? 0);

console.log(delay({ status: 'confirmed', frame: 1, sentAt: 100, ackedAt: 250 }));
console.log(delay({ status: 'confirmed', frame: 40, ackedAt: 300 }));

150
300

На первом кадре всё честно: 150 мс от отправки до ответа. Второй кадр подписан как подтверждённый, хотя отправки не было: это призрак Магистрали с чужой этикеткой. Тип Ринцвальда его пустил, ?? 0 подставил отправку в нулевой момент, и в отчёте появилась задержка 300 мс. Совершенно обычное число, на которое никто не посмотрит дважды. Так выглядят зелёные отчёты: ложь, которая выглядит как нормальная цифра.

Не надо. Но тип это разрешает, а запись придёт с провода, где пишет не Ринцвальд. Разница между «не надо» и «нельзя» и есть разница между договорённостью и типом.

Котёл, этап 7

Котёл учится говорить о судьбе каждого кадра, а не о флажках. Ты опишешь Pending, Confirmed и Phantom с их полями, сложишь их в Delivery и напишешь deliveries, который проходит журнал по порядку и по таблице переходов выше решает судьбу каждого кадра. Тесты сверят судьбы с тем, что считает phantomAcks, и проверят, что подтверждение без момента ответа не собирается.

EF-23-1★

Посчитай мощность типов: { readonly kind: 'sent' | 'acked'; readonly urgent: boolean }, 'T-1' | 'T-2' | 'T-3', readonly ['open' | 'closed', boolean], { readonly _tag: 'Ping' } | { readonly _tag: 'Lost'; readonly late: boolean }. Какой из них сумма, какой произведение, а какой и то и другое?

EF-23-2★★

Ринцвальд хочет четвёртый вариант: Lost, кадр, который ждал ответа дольше таймаута. Добавить его в Delivery или считать из Pending и момента now, как overdue в уроке 18? Подумай, что станет с deliveries: откуда она узнает время и останется ли вычислением. Запиши ответ одним предложением.

Практика

Глубже в архиве

Сумма и произведение пришли из языков, где они встроены и называются прямо: в Haskell тип с вариантами пишут одной строкой, и компилятор следит за полнотой разбора сам. Как из таких типов собирают модель предметной области, разбирает урок «Алгебраические типы и моделирование домена».

Дальше

Судьбы кадров разложены по трём полкам, ghost и liar больше не создать. Ринцвальд листает доску башен и хмурится.

undefined проскочил в отчёт, и ноль вместо него выглядит как настоящий момент. Как сказать «ответа нет» так, чтобы никто не забыл это проверить, разберём в следующем уроке.