Can I haz? Ударим программированием на типах по дженерикам16.10.2019 19:33

Привет, Хабр.

В прошлый раз мы описали Has-паттерн, обрисовали проблемы, которые он решает, и написали несколько конкретных инстансов:

instance HasDbConfig AppConfig where
  getDbConfig = dbConfig
instance HasWebServerConfig AppConfig where
  getWebServerConfig = webServerConfig
instance HasCronConfig AppConfig where
  getCronConfig = cronConfig

Выглядит неплохо. Какие тут могут возникнуть сложности?

Ну, давайте подумаем, какие ещё инстансы нам могут понадобиться. В первую очередь конкретные типы с конфигурацией сами по себе хорошие кандидаты на (тривиальную) реализацию этих тайпклассов, что даёт нам ещё три инстанса, где каждый метод реализуется через id, например

instance HasDbConfig DbConfig where
  getDbConfig = id

Они позволяют нам легко писать отдельные тесты или вспомогательные утилиты, не зависящие от всего AppConfig.
Это уже скучновато, но таки продолжим. Легко представить, что некоторые интеграционные тесты проверяют взаимодействие какой-то пары модулей, и мы всё ещё не хотим зависеть от конфигурации всего приложения целиком, так что теперь нам надо написать шесть инстансов (по два на тип), каждый из которых будет сводиться к fst или snd. Например, для DbConfig:

instance HasDbConfig (DbConfig, b) where
  getDbConfig = fst
instance HasDbConfig (a, DbConfig) where
  getDbConfig = snd

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

Если интересно, как решить эту задачу в общем виде, причём тут зависимые типы, и как всё это в итоге будет выглядеть на хаскеле — велкам под кат.

Во-первых, заметим, что для разных окружений у нас разные классы. Это может помешать сделать универсальное решение, так что вынесем окружение в отдельный параметр:

class Has part record where
  extract :: record -> part

Можно сказать, что Has part record означает, что из значения типа record можно извлечь какое-то значение типа part. В этих терминах наш старый добрый HasDbConfig становится Has DbConfig, и аналогично для прочих тайпклассов, которые мы написали ранее. Получается практически чисто синтаксическое изменение, и, например, тип одной из функций из нашего предыдущего поста превращается из

doSmthWithDbAndCron :: (MonadReader r m, HasDbConfig r, HasCronConfig r) => ...

в

doSmthWithDbAndCron :: (MonadReader r m, Has DbConfig r, Has CronConfig r) => ...

Единственное изменение — пара пробелов в нужных местах.

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

Теперь, когда нам не важен конкретный тип окружения, посмотрим, какие record могут реализовывать тайпкласс Has part record для фиксированного part. У этой задачи есть хорошая индуктивная структура:

Каждый тип имеет сама себя: Has record record реализуется тривиальным образом (extract = id).
Если record — произведение типов rec1 и rec2, то Has part record реализуетcя тогда и только тогда, когда реализуется либо Has part rec1, либо Has part rec2.
Если record — сумма типов rec1 и rec2, то Has part record реализуется тогда и только тогда, когда реализуется и Has part rec1, и Has part rec2. Хотя практическая распространённость этого случая в этом контексте неочевидна, но его всё равно стоит упомяунть для полноты.

Итак, похоже, мы сформулировали набросок алгоритма для автоматического определения, реализуется ли Has part record для данных part и record!

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

Я не буду писать ещё один туторил по дженерикам, поэтому просто перейдём к коду.

Воспользуемся классическим способом Generic-реализации нашего Has через вспомогательный класс GHas:

class GHas part grecord where
  gextract :: grecord p -> part

Здесь grecord — Generic-представление нашего типа record.

Реализации GHas следуют индуктивной структуре, которую мы заметили выше:

instance GHas record (K1 i record) where
  gextract (K1 x) = x

instance GHas part record => GHas part (M1 i t record) where
  gextract (M1 x) = gextract x

instance GHas part l => GHas part (l :*: r) where
  gextract (l :*: _) = gextract l

instance GHas part r => GHas part (l :*: r) where
  gextract (_ :*: r) = gextract r

K1 соответствует базовому случаю.
M1 — Generics-специфичные метаданные, которые нам в нашей задаче не нужны, поэтому мы их просто игнорируем и проходим их насквозь.
Первый инстанс для типа-произведения l :*: r соответствует случаю, когда «левая» часть произведения имеет нужное нам значение типа part (возможно, рекурсивно).
Аналогично второй инстанс для типа-произведения l :*: r соответствует случаю, когда «правая» часть произведения имееет нужное нам значение типа part (естественно тоже, возможно, рекурсивно).

Мы здесь поддерживаем только типы-произведения. Моё субъективное впечатление — суммы не так часто используются в контекстах для MonadReader и тому подобных классов, так что ими можно пренебречь для упрощения рассмотрения.

Кроме того, тут полезно заметить, что каждый $n$ -арный тип-произведение (a1, ..., an) может быть представлен как композиция $n-1$ пар (a1, (a2, (a3, (..., an)))), так что я позволю себе ассоциировать типы-произведения c парами.

Имея наш GHas, можно написать реализацию по умолчанию для Has, использующую дженерики:

class Has part record where
  extract :: record -> part

  default extract :: Generic record => record -> part
  extract = gextract . from

Готово.

Или нет?

Если мы попробуем скомпилировать этот код, то увидим, что он не тайпчекается даже безо всяких попыток использовать эту реализацию по умолчанию, сообщая о каких-то там overlapping instances. Хуже того, эти инстансы в некотором cмысле одинаковы. Похоже, пришла пора разобраться с тем, как работает механизм разрешения инстансов в хаcкеле.

Пусть у нас есть

instance context => Foo barPattern bazPattern where
  ...

(кстати, вот эта штука после => называется instance head.)

Выглядит естественным прочитать это как

Пусть нам надо выбрать инстанс для Foo bar baz. Если context удовлетворён, то можно выбрать этот инстанс при условии, что bar и baz соответствуют barPattern и bazPattern.

Однако это неправильная интерпретация, и всё как раз наоборот:

Пусть нам надо выбрать инстанс для Foo bar baz. Если bar и baz соответствуют barPattern и bazPattern, то мы выбираем этот инстанс и добавляем context в список констрейнтов, которые надо разрешить.

Теперь очевидно, в чём проблема. Давайте повнимательнее рассмотрим следующую пару инстансов:

instance GHas part l => GHas part (l :*: r) where
  gextract (l :*: _) = gextract l

instance GHas part r => GHas part (l :*: r) where
  gextract (_ :*: r) = gextract r

Они имеют одинаковые instance heads, так что неудивительно, они пересекаются! Кроме того, ни одиз из них не является более специфичным, чем другой.

Кроме того, не существует способа как-то уточнить эти инстансы, чтобы они перестали пересекаться. Ну, кроме добавления ещё параметров GHas.

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

Так как мы договорились не поддерживать типы-суммы, путь — это в прямом смысле последовательность поворотов налево или направо в типах-произведениях (то есть, выборов первого или второго компонента пары), завершающаяся большим указателем «ЗДЕСЬ», как только мы нашли нужный тип. Запишем это:

data Path = L Path | R Path | Here deriving (Show)

Например

Рассмотрим следующие типы:

data DbConfig = DbConfig
  { dbAddress :: DbAddress
  , dbUsername :: Username
  , dbPassword :: Password
  }

data AppConfig = AppConfig
  { dbConfig :: DbConfig
  , webServerConfig :: WebServerConfig
  , cronConfig :: CronConfig
  }

Какие могут быть примеры путей из AppConfig?

К DbConfig ⟶ L Here.
К WebServerConfig ⟶ R (L Here).
К CronConfig ⟶ R (R Here).
К DbAddress ⟶ L (L Here).

Каким может быть результат поиска значения нужного типа? Два варианта очевидны: мы его можем либо найти, либо не найти. Но на самом деле всё чуточку сложнее: мы можем найти более одного значения данного типа. По-видимому, наиболее разумным поведением в этом неоднозначном случае тоже будет сообщение об ошибке. Любой выбор конкретного значения будет иметь известную долю произвольности.

Действительно, рассмотрим наш стандартный пример веб-сервиса. Если кто-то хочет получить значение типа (Host, Port), то должен ли это быть адрес сервера БД или адрес веб-сервера? Уж лучше не рисковать.

В любом случае, давайте выразим это в коде:

data MaybePath = NotFound | Conflict | Found Path deriving (Show)

Мы разделяем NotFound и Conflict, так как обработка этих случаев принципиально различается: если мы получим NotFound в одной из веток нашего типа-произведения, то это не помешает найти нужное значение в какой-то другой ветке, тогда как Conflict в любой ветке сразу означает полную неудачу.

Теперь рассмотрим частный случай типов-произведений (которые, как мы договорились, мы считаем парами). Как в них найти значение нужного типа? Можно запустить поиcк рекурсивно в каждой компоненте пары, получить результаты p1 и p2 соответственно, и затем каким-то образом их скомбинировать.

Так как мы говорим о выборе инстансов тайпклассов, что происходит во время компиляции, то нам на самом деле нужны компилтайм-вычисления, которые в хаскеле выражаются через вычисления на типах (пусть даже типы представлены через поднятые во вселенную типов термы при помощи DataKinds). Соответственно, такая функция на типах представляется как type family:

type family Combine p1 p2 where
  Combine ('Found path) 'NotFound = 'Found ('L path)
  Combine 'NotFound ('Found path) = 'Found ('R path)
  Combine 'NotFound 'NotFound = 'NotFound
  Combine _ _ = 'Conflict

Эта функция представляет несколько случаев:

Если один из рекурсивных поисков успешен, а другой привёл к NotFound, то мы берём путь из успешного поиска и дописываем поворот в нужную сторону.
Если оба рекурсивных поиска завершились с NotFound, то, очевидно, и весь поиск завершается с NotFound.
В любом другом случае мы получаем Conflict.

Теперь напишем тайп-левел-функцию, которая принимает part, который нужно найти, и Generic-представление типа, в котором нужно найти part, и производит поиск:

type family Search part (grecord :: k -> *) :: MaybePath where
  Search part (K1 _ part) = 'Found 'Here
  Search part (K1 _ other) = 'NotFound
  Search part (M1 _ _ x) = Search part x
  Search part (l :*: r) = Combine (Search part l) (Search part r)
  Search _ _ = 'NotFound

Заметим, что мы получили что-то очень похожее по смыслу на нашу предыдущую попытку с GHas. Это вполне ожидаемо, так как мы на самом деле воспроизводим алгоритм, который мы пытались выразить через тайпклассы.

К слову о GHas, всё, что нам осталось — добавить к этому классу дополнительный параметр, отвечающий за найденный ранее путь, и который будет служить для выбора конкретных инстансов:

class GHas (path :: Path) part grecord where
  gextract :: Proxy path -> grecord p -> part

Мы также добавили дополнительный аргумент для gextract, чтобы компилятор мог выбрать правильный инстанс для данного пути (который для этого должен упоминаться в сигнатуре функции).

Теперь инстансы написать довольно легко:

instance GHas 'Here record (K1 i record) where
  gextract _ (K1 x) = x

instance GHas path part record => GHas path part (M1 i t record) where
  gextract proxy (M1 x) = gextract proxy x

instance GHas path part l => GHas ('L path) part (l :*: r) where
  gextract _ (l :*: _) = gextract (Proxy :: Proxy path) l

instance GHas path part r => GHas ('R path) part (l :*: r) where
  gextract _ (_ :*: r) = gextract (Proxy :: Proxy path) r

Действительно, мы просто выбираем нужный инстанс, основываясь на пути в path, который мы рассчитали ранее.

Как теперь написать нашу default-реализацию функции extract :: record -> part в классе Has? У нас есть несколько условий:

record должен реализовывать Generic, чтобы можно было применять механизм дженериков, так что мы получаем Generic record.
Функция Search должна найти part в record (вернее, в Generic-представлении record, которое выражается как Rep record). В коде это выглядит чуть более непривычно: Search part (Rep record) ~ 'Found path. Эта запись означает ограничение, что результат Search part (Rep record) должен быть равен 'Found path для некоторого path (которое нам, собственно, и интересно).
Мы должны иметь возможность использовать GHas вместе с part, дженерик-представлением record и path c прошлого шага, что превращается в GHas path part (Rep record).

Мы встретим последние два констрейнта ещё несколько раз, так что полезно их вынести в отдельный констрейнт-синоним:

type SuccessfulSearch part record path = (Search part (Rep record) ~ 'Found path, GHas path part (Rep record))

С учётом этого синонима, мы получаем

class Has part record where
  extract :: record -> part

  default extract :: forall path. (Generic record, SuccessfulSearch part record path) => record -> part
  extract = gextract (Proxy :: Proxy path) . from

Теперь всё!

Чтобы посмотреть на всё это в деле, напишем несколько общих инстансов для туплов:

instance SuccessfulSearch a (a0, a1) path => Has a (a0, a1)
instance SuccessfulSearch a (a0, a1, a2) path => Has a (a0, a1, a2)
instance SuccessfulSearch a (a0, a1, a2, a3) path => Has a (a0, a1, a2, a3)

Здесь SuccessfulSearch a (a0, ..., an) path отвечает за то, что a встречается среди a0, ..., an ровно один раз.

Пусть теперь у нас есть наш старый-добрый

data AppConfig = AppConfig
  { dbConfig :: DbConfig
  , webServerConfig :: WebServerConfig
  , cronConfig :: CronConfig
  }

и мы хотим вывести Has DbConfig, Has WebServerConfig и Has CronConfig. Достаточно включить расширения DeriveGeneric и DeriveAnyClass и дописать правильное deriving-объявление:

data AppConfig = AppConfig
  { dbConfig :: DbConfig
  , webServerConfig :: WebServerConfig
  , cronConfig :: CronConfig
  } deriving (Generic, Has DbConfig, Has WebServerConfig, Has CronConfig)

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

Безопасность превыше всего

Что, если у нас нет какого-то типа?

data AppConfig = AppConfig
  { dbConfig :: DbConfig
  , webServerConfig :: WebServerConfig
  } deriving (Generic, Has CronConfig)

Неа, мы получаем ошибку прямо в точке определения типа:

Spec.hs:35:24: error:
    • Couldn't match type ‘'NotFound’
                     with ‘'Found path0’
        arising from the 'deriving' clause of a data type declaration
    • When deriving the instance for (Has CronConfig AppConfig)
   |
35 |   } deriving (Generic, Has CronConfig)
   |                        ^^^^^^^^^^^^^^

Не самое дружелюбное сообщение об ошибке, но даже по нему всё ещё можно понять, в чём проблема: чётотам чётотам NotFound чётотам чётотам CronConfig.

Что, если у нас есть несколько полей с одним и тем же типом?

data AppConfig = AppConfig
  { prodDbConfig :: DbConfig
  , qaDbConfig :: DbConfig
  , webServerConfig :: WebServerConfig
  , cronConfig :: CronConfig
  } deriving (Generic, Has DbConfig)

Неа, как и ожидалось:

Spec.hs:37:24: error:
    • Couldn't match type ‘'Conflict’
                     with ‘'Found path0’
        arising from the 'deriving' clause of a data type declaration
    • When deriving the instance for (Has DbConfig AppConfig)
   |
37 |   } deriving (Generic, Has DbConfig)
   |                        ^^^^^^^^^^^^

Похоже, что всё действительно хорошо.

Итак, попробуем кратко сформулировать предложенный метод.

Пусть у нас есть какой-то тайпкласс, и мы хотим автоматически выводить его инстансы согласно каким-то рекурсивным правилам. Тогда мы можем избежать неоднозначностей (и вообще выразить эти правила, если они нетривиальны и не укладываются в стандартный механизм разрешения инстансов) следующим образом:

Закодируем рекурсивные правила в виде индуктивного типа данных T.
Напишем функцию на типах (в виде type family) для предварительного расчёта значения v этого типа T (или, в терминах хаскеля, типа v сорта T — где ж мои зависимые типы), описывающего конкретную последовательность шагов, которые надо предпринять.
Использовать этот v как дополнительный аргумент Generic-хелперу для определения конкретной последовательности инстансов, которые теперь матчатся на значения v.

Ну и всё!

В следующих постах мы рассмотрим некоторые изящные расширения (а также изящные ограничения) этого подхода.

А, ну и да. Интересно отследить последовательность наших обобщений.

Начали с Env -> Foo.
Недостаточно общо, завернёмся в монаду Reader Env.
Недостаточно общо, перепишем с тайпклассом MonadReader Env m.
Недостаточно общо, перепишем как MonadReader r m, HasEnv r.
Недостаточно общо, напишем как MonadReader r m, Has Env r и добавим дженериков, чтобы компилятор там всё сам делал.
Теперь норм.