Слои как морфизмы: категорная модель гексагональной архитектуры

Слоистую и гексагональную архитектуру обычно объясняют картинкой: кружок ядра, вокруг порты, снаружи адаптеры, стрелки зависимостей смотрят внутрь. Картинка обещает три вещи:

1. Слой знает только интерфейс того, кто под ним, а не его устройство.
2. Адаптер можно заменить, и всё, что выше, продолжит работать без правок.
3. Слои складываются в стопку любой высоты, и неважно, как ты группируешь соседние пары.

Пока это обещания, их нельзя проверить. В этом уроке ты превратишь их в теоремы. Для этого понадобятся три вещи: категория контейнеров, где интерфейс становится объектом, утверждение «слой один к одному это естественное преобразование функторов» и свободная монада, которая даёт композицию слоёв даром. По дороге выяснится, почему ответ HTTP всегда идёт против стрелки, то есть контравариантен.

Урок продолжает описание против интерпретации: там программа становилась данными, здесь ты узнаешь, какой структурой обладают все такие интерпретаторы сразу. Определения функтора и монады повторены ниже, но на уровне урока о функторах и монадах их стоит уже знать.

Минимум теории категорий

Определение 1. Категория $\mathcal{C}$ состоит из объектов, множеств морфизмов $\mathcal{C}(A,B)$ для каждой пары объектов, тождественного морфизма ${\mathrm{id}}_A$ и композиции $g\circ f:A\to C$ для $f:A\to B$ и $g:B\to C$. Требуются два закона: $f\circ {\mathrm{id}}_A=f={\mathrm{id}}_B\circ f$ и $h\circ (g\circ f)=(h\circ g)\circ f$.

Главный пример для нас это $\mathbf{Set}$: объекты это множества, морфизмы это всюду определённые функции. Множества здесь играют роль типов, функции играют роль чистых функций между ними.

Определение 2. Функтор $F:\mathcal{C}\to \mathcal{D}$ сопоставляет каждому объекту $A$ объект $FA$, каждому морфизму $f:A\to B$ морфизм $Ff:FA\to FB$ и сохраняет тождество и композицию: $F\mathrm{id}=\mathrm{id}$, $F(g\circ f)=Fg\circ Ff$. Функтор $\mathbf{Set}\to \mathbf{Set}$ это то, что в коде называют контейнерным типом с map.

Определение 3. Естественное преобразование $\alpha :F\Rightarrow G$ между функторами $F,G:\mathcal{C}\to \mathcal{D}$ это семейство морфизмов ${\alpha }_X:FX\to GX$, по одному на объект, такое, что для любого $h:X\to Y$ коммутирует квадрат:

$$\begin{array}{ccc}FX& \stackrel{{\alpha }_X}{\to }& GX\\ Fh\downarrow & & \downarrow Gh\\ FY& \underset{{\alpha }_Y}{\to }& GY\end{array}$$

То есть $Gh\circ {\alpha }_X={\alpha }_Y\circ Fh$. В коде это полиморфная функция <X>(fx: F<X>) => G<X>, которая не смотрит на элементы: ей всё равно, сначала переложить содержимое и потом применить map, или наоборот.

Функторы $\mathbf{Set}\to \mathbf{Set}$ с естественными преобразованиями сами образуют категорию $[\mathbf{Set},\mathbf{Set}]$. Композиция там покомпонентная: $(\beta \circ \alpha {)}_X={\beta }_X\circ {\alpha }_X$. Законы категории проверять не нужно: они выполняются в каждой компоненте, потому что выполняются в $\mathbf{Set}$. Запомни этот приём. Весь урок построен на том, чтобы получить законы композиции слоёв по наследству, а не доказывать их для каждой архитектуры заново.

Интерфейс как контейнер

Порт в гексагональной архитектуре это набор команд, и на каждую команду есть свой тип ответа. Команде findByEmail отвечают «пользователь или ничего», команде insert отвечают «готово». Тип ответа зависит от команды. Ровно это и описывает контейнер.

Определение 4. Контейнер $S◃P$ это множество форм $S$ и семейство множеств позиций $P:S\to \mathbf{Set}$, по одному множеству $P(s)$ на каждую форму $s\in S$.

Определение 5. Расширение контейнера это функтор $[[S◃P]]:\mathbf{Set}\to \mathbf{Set}$:

$$[[S◃P]]X=\sum _{s\in S}(P(s)\to X),[[S◃P]]h(s,k)=(s,h\circ k).$$

Элемент расширения это пара: форма $s$ и функция $k$, которая каждой позиции формы сопоставляет значение из $X$. Законы функтора очевидны: $\mathrm{id}\circ k=k$ и $(g\circ h)\circ k=g\circ (h\circ k)$.

Привычные типы данных оказываются контейнерами:

• Maybe: формы $\{\mathsf{nothing},\mathsf{just}\}$, $P(\mathsf{nothing})=\varnothing$, $P(\mathsf{just})=\{\ast \}$. Функция из пустого множества одна, поэтому у nothing нет содержимого.
• Список: формы это длины $n\in \mathbb{N}$, позиции $P(n)=\{0,\dots ,n-1\}$, функция $k$ это сами элементы.

Для архитектуры нужно другое прочтение. Пусть формы это команды, а позиции это возможные ответы на команду. Тогда элемент $(s,k)\in [[S◃P]]X$ это один шаг взаимодействия: «отправь команду $s$; когда придёт ответ $p\in P(s)$, продолжай как $k(p)$». Такое прочтение интерфейсов идёт от Хэнкока и Сетцера.

Порты нашего примера:

$$\mathsf{Repo}=\{\mathsf{findByEmail}(e),\mathsf{insert}(u)\}◃P_{\mathsf{Repo}},P_{\mathsf{Repo}}(\mathsf{findByEmail}(e))=\mathrm{User}+1,P_{\mathsf{Repo}}(\mathsf{insert}(u))=1.$$ $$\mathsf{Http}=\mathrm{Req}◃\mathrm{Resp}.$$

У $\mathsf{Http}$ позиции постоянны: на любой запрос отвечают значением одного типа $\mathrm{Resp}$. Тогда расширение упрощается до $[[\mathrm{Req}◃\mathrm{Resp}]]X=\mathrm{Req}\times (\mathrm{Resp}\to X)$. Запомни, где тут стоит $\mathrm{Resp}$: слева от стрелки функции. К этому месту мы вернёмся.

Морфизм контейнеров и категория Cont

Как выглядит слой, который каждую свою команду обслуживает ровно одной командой нижнего порта? Он должен перевести команду вниз, а когда придёт ответ снизу, перевести его обратно наверх. Направления у двух переводов противоположные.

Определение 6. Морфизм контейнеров $(u,f):S◃P\to T◃Q$ это функция на формах $u:S\to T$ и семейство функций на позициях $f_s:Q(u(s))\to P(s)$ для каждой $s\in S$.

Формы идут вперёд, позиции идут назад. Слой отправляет вниз команду $u(s)$, получает ответ из $Q(u(s))$ и превращает его в ответ на исходную команду.

Определение 7. Композиция морфизмов $(u,f):S◃P\to T◃Q$ и $(v,g):T◃Q\to U◃R$:

$$(v,g)\circ (u,f)=(v\circ u,s\mapsto f_s\circ g_{u(s)}).$$

Проверь типы: $g_{u(s)}:R(v(u(s)))\to Q(u(s))$, затем $f_s:Q(u(s))\to P(s)$. Итог $R(v(u(s)))\to P(s)$, как и требует определение 6. Обрати внимание на порядок: на формах сначала $u$, потом $v$; на позициях сначала $g$, потом $f$.

Предложение 1. Контейнеры с их морфизмами образуют категорию $\mathbf{Cont}$ с тождеством $({\mathrm{id}}_S,s\mapsto {\mathrm{id}}_{P(s)})$.

Доказательство. Единица: $(u,f)\circ \mathrm{id}=(u\circ \mathrm{id},s\mapsto \mathrm{id}\circ f_s)=(u,f)$, вторая сторона так же. Ассоциативность для третьего морфизма $(w,h)$: на формах обе стороны дают $w\circ v\circ u$, потому что композиция функций ассоциативна. На позициях левая группировка даёт $s\mapsto f_s\circ (g_{u(s)}\circ h_{v(u(s))})$, правая $s\mapsto (f_s\circ g_{u(s)})\circ h_{v(u(s))}$, и это одна функция по той же причине. $\square$

Если вычеркнуть зависимость, то есть взять постоянные позиции, морфизм $(\mathrm{Req}◃\mathrm{Resp})\to (\mathrm{Cmd}◃\mathrm{Res})$ становится парой функций $u:\mathrm{Req}\to \mathrm{Cmd}$ и $f:\mathrm{Req}\times \mathrm{Res}\to \mathrm{Resp}$. Это ровно линза: get вперёд и put назад, причём put снова видит исходный запрос. Поэтому морфизмы контейнеров называют зависимыми линзами.

Слой это морфизм функторов

Морфизм контейнеров переводит шаги взаимодействия: шаг верхнего интерфейса становится шагом нижнего. На расширениях он задаёт семейство функций

$${\alpha }_X^{(u,f)}:[[S◃P]]X\to [[T◃Q]]X,{\alpha }_X^{(u,f)}(s,k)=(u(s),k\circ f_s).$$

Типы сходятся: $k:P(s)\to X$ и $f_s:Q(u(s))\to P(s)$, значит $k\circ f_s:Q(u(s))\to X$. Продолжение $k$ ждало ответ верхнего уровня; теперь оно сначала переводит нижний ответ через $f_s$. Естественность: $h\circ (k\circ f_s)=(h\circ k)\circ f_s$, то есть квадрат из определения 3 коммутирует.

Оказывается, других естественных преобразований между расширениями нет.

Теорема 1 (Abbott, Altenkirch, Ghani). Сопоставление $S◃P\mapsto [[S◃P]]$, $(u,f)\mapsto {\alpha }^{(u,f)}$ это полностью точный функтор $[[-]]:\mathbf{Cont}\to [\mathbf{Set},\mathbf{Set}]$. Иначе говоря, каждое естественное преобразование $[[S◃P]]\Rightarrow [[T◃Q]]$ имеет вид ${\alpha }^{(u,f)}$ ровно для одного морфизма $(u,f)$.

Доказательство. Сначала функториальность. Тождество переходит в $(s,k)\mapsto (s,k)$. Для композиции посчитай ${\alpha }^{(v,g)}({\alpha }^{(u,f)}(s,k))={\alpha }^{(v,g)}(u(s),k\circ f_s)=(v(u(s)),k\circ f_s\circ g_{u(s)})$, а это ${\alpha }^{(v,g)\circ (u,f)}(s,k)$ по определению 7.

Теперь биекция. Обозначим $y^A=\mathbf{Set}(A,-)$, представимый функтор. Определение 5 говорит, что расширение это сумма представимых: $[[S◃P]]={\sum }_{s\in S}{y}^{P(s)}$. Для любого функтора $G$ получаем цепочку биекций:

$$\mathrm{Nat}(\sum _{s\in S}{y}^{P(s)},G)\cong \prod _{s\in S}\mathrm{Nat}(y^{P(s)},G)\cong \prod _{s\in S}G(P(s)).$$

Первый шаг: сумма в категории функторов считается покомпонентно, и отображение из суммы задаётся своими ограничениями на слагаемые. Второй шаг это лемма Йонеды: преобразование $\beta :y^A\Rightarrow G$ определяется элементом ${\beta }_A({\mathrm{id}}_A)\in G(A)$, и обратно элемент $x$ даёт ${\beta }_X(k)=G(k)(x)$.

Подставь $G=[[T◃Q]]$:

$$\prod _{s\in S}\sum _{t\in T}(Q(t)\to P(s))\cong \sum _{u:S\to T}\prod _{s\in S}(Q(u(s))\to P(s)).$$

Это перестановка произведения и суммы: выбор пары $(t,f)$ для каждого $s$ это то же самое, что функция $u$, выбирающая $t$, плюс семейство $f_s$. В $\mathbf{Set}$ здесь работает аксиома выбора, в зависимой теории типов это просто теорема. Правая часть по определению 6 и есть множество морфизмов $S◃P\to T◃Q$.

Осталось убедиться, что цепочка переводит $(u,f)$ именно в ${\alpha }^{(u,f)}$. Морфизму соответствует семейство элементов $(u(s),f_s)\in [[T◃Q]](P(s))$. Обратный ход Йонеды восстанавливает преобразование: $(s,k)\mapsto [[T◃Q]]k(u(s),f_s)=(u(s),k\circ f_s)$. Это определение ${\alpha }^{(u,f)}$. $\square$

Отсюда первая точная формулировка: слой, который обслуживает каждую команду одним вызовом вниз, это естественное преобразование между функторами интерфейсов, и ничего, кроме морфизма контейнеров, он содержать не может. Естественность здесь значит в точности обещание 1 из начала урока: слой не смотрит в продолжение $k$, то есть не знает, что верхний код сделает с ответом. А стрелка $\mathsf{Http}\to \mathsf{App}$ смотрит туда же, куда стрелка зависимости на картинке гексагона: сверху вниз.