Естественные преобразования

В Haskell каждая функция с типом `forall a. F a -> G a` автоматически является естественным преобразованием. Без доказательства. Это теорема - "theorems for free" (Wadler, 1989). Parametricity = naturalness. Haskell type checker при каждой компиляции молча проверяет коммутативность математического квадрата - не зная, что делает именно это. Как система типов гарантирует математическую структуру автоматически?

• **Monad transformers (Haskell/Scala)**: liftA2, fmap, lift - это компоненты естественного преобразования между эндофункторами. Вся иерархия трансформеров (StateT, ReaderT, EitherT) строится на натуральности
• **XLA graph rewriting (TensorFlow/JAX)**: трансформации вычислительного графа должны коммутировать с операциями - иначе семантика меняется. Натуральность - математическое условие корректности оптимизаций компилятора
• **Profunctor optics (Haskell lens)**: van Laarhoven lenses и profunctor optics - прямое следствие леммы Йонеды. Типы `Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t` корректны именно потому, что parametricity гарантирует натуральность

Предварительные знания

• Функторы

Естественное преобразование: семейство морфизмов

В Haskell каждая функция с типом `forall a. F a -> G a` автоматически является естественным преобразованием. Без явного доказательства. Это теорема - "theorems for free" (Wadler, 1989). Parametricity = naturalness. Система типов Haskell при каждой компиляции молча проверяет математическую структуру - коммутативность квадрата. Понять как - и откроется, почему polymorphic functions вообще работают.

Пусть F, G: C -> D - два функтора. Естественное преобразование eta: F => G - это семейство морфизмов {eta_A: F(A) -> G(A)} для каждого объекта A в C, удовлетворяющее условию естественности.

Три уровня абстракции уже знакомы: объекты, морфизмы между объектами, функторы между категориями. Логичный следующий шаг - "морфизмы между функторами". Это и есть естественные преобразования. Если функторы - это переводы между языками, то естественное преобразование - систематический способ перейти от одного перевода к другому, не теряя структуры.

Ключевой инсайт: естественное преобразование работает одинаково для всех типов. Оно не заглядывает внутрь элементов. safeHead не знает, числа в списке или строки - и именно это делает его "естественным". В ML-контексте: monad transformers в Haskell/Scala (liftA2, fmap) - это компоненты естественного преобразования между эндофункторами над типами эффектов.

Условие естественности и примеры

Не каждое семейство морфизмов {eta_A: F(A) -> G(A)} является естественным преобразованием. Компоненты должны быть согласованы - и это согласование выражается через коммутативный квадрат. Два пути от F(A) до G(B) обязаны давать одинаковый результат.

Условие естественности: eta_B o F(f) = G(f) o eta_A для любого f: A -> B. Смысл: "сначала F, потом перейти к G" = "сначала перейти к G, потом G". Порядок не важен - преобразование совместимо со структурой.

Исторический пример из линейной алгебры: определитель det: GL_n -> (-)* - естественное преобразование из функтора обратимых матриц в функтор ненулевых скаляров. Для любого изоморфизма f матриц квадрат коммутирует. Именно "естественность" определителя делает его инвариантом - он не зависит от выбора базиса.

Контрпример важен: `sortAndHead` - сначала сортировать список, потом взять первый элемент - не является естественным преобразованием. Она зависит от структуры элементов (нужен порядок), и для функций, не сохраняющих порядок, квадрат перестаёт коммутировать. TensorFlow/XLA graph rewriting использует именно это: трансформации вычислительного графа должны быть "естественными" (коммутировать с операциями) - иначе семантика программы ломается.

Удвоение double: Id => Id в категории абелевых групп - ещё один чистый пример. Компонента в точке A: x |-> 2x. Для любого гомоморфизма f: A -> B условие double_B o f = f o double_A выполнено: 2*f(x) = f(2*x). Квадрат коммутирует для всей категории Ab сразу.

Превью леммы Йонеды: объект = его морфизмы

Лемма Йонеды - одна из самых неожиданных теорем математики. Она говорит: чтобы полностью понять функтор F, достаточно посмотреть на естественные преобразования из hom-функтора в F. Или, в философской формулировке: объект полностью определяется своими отношениями с другими объектами. Не нужно "заглядывать внутрь".

Лемма Йонеды: для функтора F: C -> Set и объекта A в C существует биекция Nat(Hom(A, -), F) ~= F(A). Множество всех естественных преобразований из Hom(A, -) в F изоморфно множеству F(A).

Hom(A, -) - это функтор, который каждому объекту B ставит в соответствие множество морфизмов A -> B. Лемма говорит: естественное преобразование из "всех функций из A" в F полностью определяется одним элементом F(A). Бесконечное семейство компонент кодируется одной точкой - это поразительная компрессия информации.

Lens/optics в функциональном программировании строится именно на этой идее. Профункторная оптика - это естественные преобразования между hom-функторами. Вся экосистема lens в Haskell (van Laarhoven lenses, profunctor optics) - прямое следствие леммы Йонеды. Типы говорят: "этот lens корректен" именно потому, что система типов проверяет натуральность.

Теперь возврат к hook'у: Wadler "theorems for free" (1989) - это следствие параметричности = натуральности. Haskell type checker при каждой компиляции функции `forall a. F a -> G a` неявно проверяет коммутативность квадрата eta. Не явным образом - через parametricity. Любая функция, знающая что-то о типе a, нарушает условие естественности и не типизируется. Система типов = математика, автоматически.

Ключевые идеи

• **Естественное преобразование** eta: F => G - семейство морфизмов eta_A: F(A) -> G(A), согласованных через коммутативный квадрат
• **Условие естественности**: eta_B o F(f) = G(f) o eta_A - два пути вокруг квадрата дают одинаковый результат. sortAndHead нарушает, safeHead выполняет
• **Лемма Йонеды**: Nat(Hom(A,-), F) ~= F(A) - бесконечное семейство преобразований кодируется одной точкой F(A)
• **Parametricity = naturalness**: в Haskell/Scala parametric polymorphism автоматически гарантирует коммутативность квадрата (Wadler 1989)

Связанные темы

Естественные преобразования - мост к продвинутым конструкциям:

• Функторы — Естественные преобразования - морфизмы между функторами
• Монады — Монада = эндофунктор + два естественных преобразования (unit, join)
• Категории: объекты и морфизмы — Функторы и их преобразования образуют категорию функторов [C,D]

Вопросы для размышления

• Почему parametric polymorphism в Haskell автоматически гарантирует естественность? Что именно запрещает тип `forall a. F a -> G a` делать с элементами?
• sortAndHead нарушает естественность - можно ли его починить, ограничив допустимые морфизмы f? Что это даст теоретически?
• Если функторы - объекты категории [C,D], а естественные преобразования - морфизмы, является ли категория функторов снова категорией? Что такое функтор между категориями функторов?

Связанные уроки

• ct-02 — Функторы - фундамент: естественные преобразования - морфизмы между ними
• ct-04 — Монады строятся как естественные преобразования между эндофункторами
• aa-01-groups-intro — Гомоморфизм групп - частный случай естественного преобразования в Grp
• top-01 — Непрерывные отображения - аналог натуральности в топологических категориях
• aa-03-homomorphisms
• plt-11-typeclasses