Advanced type-level

Последний урок раздела, финальный заглядывание под капот. В уроке 40 мы готовили глаза к сигнатурам Servant, а весь проект 3 опирался на машинерию, которую принимали как данность. Пора её разобрать: функции на типах (type families), автовывод инстансов через GHC.Generics, и кусок реальных внутренностей Servant. А заодно честно поговорим, сколько всё это стоит.

Type family: функция на типах

Уже знаешь, что типы можно поднимать на уровень значений. Type family это функция, считающая по типам. Закрытая (closed) перечисляет все уравнения сразу, как case на типах:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}

type family Not (b :: Bool) :: Bool where
  Not 'True = 'False
  Not 'False = 'True

Not это вычисление, которое GHC проводит во время компиляции: Not 'True упрощается до 'False прямо в проверке типов. Открытая (open) семья не закрыта списком уравнений, к ней можно добавлять случаи инстансами из разных модулей:

type family Element c   -- открытая: тип элемента контейнера
type instance Element [a] = a
type instance Element (Maybe a) = a

Closed берут, когда все случаи известны и важен порядок (как в case), open когда семья расширяемая, как класс.

Инъективность: TypeFamilyDependencies

У обычной type family есть подвох: по результату нельзя восстановить аргумент. Если Element c дала Int, GHC не знает, был ли c это [Int] или Maybe Int. Иногда это мешает выводу типов. TypeFamilyDependencies позволяет объявить семью инъективной: разным аргументам разные результаты.

{-# LANGUAGE TypeFamilyDependencies #-}

type family Id a = r | r -> a where
  Id a = a

Запись r | r -> a это обещание: по результату r однозначно восстанавливается аргумент a. Теперь GHC умеет выводить аргумент по результату, и в сигнатурах исчезают лишние аннотации типов.

GHC.Generics изнутри: как aeson выводит инстансы

В проекте 3 мы писали instance ToJSON Game с пустым телом, и aeson сам выводил сериализацию. Как? Через GHC.Generics. Класс Generic даёт типу единое структурное представление Rep и пару переходов:

class Generic a where
  type Rep a          -- структура типа: сумма произведений
  from :: a -> Rep a x  -- упаковать в обобщённое представление
  to   :: Rep a x -> a  -- собрать обратно

Rep описывает любой тип единообразно: суммы (это :+:, выбор конструктора), произведения (:*:, поля рядом), обёртки над полями. Запись Game с тремя полями превращается в произведение трёх компонент, sum-тип в сумму веток.

Дальше фокус: aeson пишет сериализацию один раз поверх Rep, а не для каждого типа. Класс-помощник GToJSON определён индукцией по структуре: как сериализовать сумму, как произведение, как одно поле. Когда ты пишешь instance ToJSON Game, метод по умолчанию делает genericToJSON, то есть from переводит Game в Rep, обобщённый код сериализует структуру, готово. Тот же механизм стоит за deriving anyclass (FromJSON, ToJSON) из урока 42: код пишется для формы, а не для конкретного типа.

Кусок внутренностей Servant

Теперь, вооружившись type families, разберём, как Servant превращает тип API в сервер. Сердце это класс HasServer и связанная type family ServerT:

class HasServer api context where
  type ServerT api (m :: Type -> Type) :: Type
  route :: ... -- как маршрутизировать запрос

ServerT api m это функция на типах: она по типу API вычисляет тип обработчиков. Инстансы определены индукцией по комбинаторам, ровно как GToJSON по Rep:

-- два маршрута через :<|> дают пару обработчиков
instance (HasServer a ctx, HasServer b ctx) => HasServer (a :<|> b) ctx where
  type ServerT (a :<|> b) m = ServerT a m :<|> ServerT b m

-- Capture добавляет аргумент обработчику
instance (FromHttpApiData a, HasServer api ctx) => HasServer (Capture sym a :> api) ctx where
  type ServerT (Capture sym a :> api) m = a -> ServerT api m

Прочитай второй инстанс: ServerT (Capture sym a :> api) m = a -> ServerT api m. Вот откуда в уроке 43 у обработчика getGame :: Int64 -> Handler Game взялся аргумент Int64: его добавила эта строчка type family. Когда ты пишешь сервер и забываешь аргумент после Capture, не компилируется именно потому, что ServerT вычислила другую форму. Никакой магии: рекурсивная функция на типах, разобранная индукцией по структуре API.