Стрелочка поворачивается: поговорим об обобщениях, или зачем программисту математика

Привет.

Прошло довольно много времени с публикации предыдущей статьи об обобщённой реализации паттерна Has, где мы успешно победили скуку и однообразный код при написании инстансов соответствующего класса, заодно поигравшись с дженериками и семействами типов одновременно, но давайте всё же добьём цикл и заодно лишний раз посмотрим, зачем программисту математика.

Итак, с обобщённой реализацией паттерна Has мы разобрались. Какой следующий интересный вопрос можно задать? Ну, например, можем ли мы обобщить наше решение, которое, к слову, является обобщением (Has Foo) обобщения (HasFoo) обобщения (MonadReader Foo) обобщения (Reader Foo) понятия параметра функции (Foo ->)? И, оказывается, что да, можем, и аж в двух ортогональных измерениях!

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

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

В данном конкретном случае у нас есть одна стрелка extract в структуре Has:

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

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

class CoHas copart corecord where
  coextract :: copart -> corecord

У творчески настроенного читателя уже могла появиться интуиция на тему получившейся структуры, но давайте продолжим предельно тупо и формально поворачивать стрелки, на этот раз в Generic-реализации методов этого класса.

Path и Combine не имеют какой-то хорошей алгебраической структуры, поэтому с ними ничего не происходит. Search же будет поинтереснее. Вспомним его определение для Has:

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 r) (Search part r)
  Search _ _ = 'NotFound

Заметим, что предпоследний случай упоминает произведение типов :*:. Дуальный к произведению объект — сумма, так что дуальная к Search функция будет выглядеть как

type family CoSearch copart (gcorecord :: k -> *) :: MaybePath where
  CoSearch copart (K1 _ copart) = 'Found 'Here
  CoSearch copart (K1 _ other) = 'NotFound
  CoSearch copart (M1 _ _ x) = CoSearch copart x
  CoSearch copart (l :+: r) = Combine (CoSearch copart l) (CoSearch copart r)
  CoSearch _ _ = 'NotFound

С GCoHas всё аналогично, поворачиваем стрелки и приписываем co:

class GCoHas (path :: Path) copart gcorecord where
  gcoextract :: Proxy path -> copart -> gcorecord p

С инстансами, естественно, всё совершенно аналогично:

instance GCoHas 'Here corecord (K1 i corecord) where
  gcoextract _ = K1

instance GCoHas path copart corecord => GCoHas path copart (M1 i t corecord) where
  gcoextract proxy = M1 . gcoextract proxy

instance GCoHas path copart l => GCoHas ('L path) copart (l :+: r) where
  gcoextract _ = L1 . gcoextract (Proxy :: Proxy path)

instance GCoHas path copart r => GCoHas ('R path) copart (l :+: r) where
  gcoextract _ = R1 . gcoextract (Proxy :: Proxy path)

Заметим, что с Proxy тут ничего не происходит, потому что Proxy на самом деле нам тут нужен исключительно для помощи тайпчекеру, какую-то глубинную алгебраическую структуру он не отображает.

Реализация самого класса CoHas при этом очевидна:

class CoHas copart corecord where
  coextract :: copart -> corecord

  default coextract :: forall path. (Generic corecord, SuccessfulSearch copart corecord path) => copart -> corecord
  coextract = to . gcoextract (Proxy :: Proxy path)

Интерпретация

Давайте теперь подумаем, что вcё это значит.

• record — какой-то тип-произведение, corecord ему дуален, так что это какой-то тип-сумма. Возможно, имя sum будет получше.
• part — поле в типе-произведении record, copart ему дуален, так что это одна из опций типа-суммы sum. Возможно, имя option будет получше.
• extract берёт record и производит part. coextract же, напротив, берёт option и производит sum. Естественная интерпретация (которая, кроме того, соответствует реализации) — coextract всего лишь создаёт значение типа-суммы, имея одну из опций этого типа. Назовём его, пожалуй, inject.

Итого: CoHas option sum означает, что мы можем, имея значение типа-опции option, получить значение типа-суммы sum, включающей этот тип option. Каноническим примером будет Either:

instance SuccessfulSearch a (Either l r) path => CoHas a (Either l r)

Так что если l отличается от r, то мы можем создать Either l r из l (и из r, конечно же), используя класс CoHas и метод inject.

Да, у нас есть те же гарантии типобезопасности: CoHas option sum выводится (через Generics) тогда и только тогда, когда существует единственный способ создать sum, содержащий значение типа option. Например, следующее не сработает:

data AppError = QaDbError DbError
              | ProdDbError DbError
              deriving (CoHas DbError)

Где может быть полезен наш CoHas? Можно рассмотреть, например, следующий паттерн имени нас номер 1.

CoHas в сочетании с MonadError

Что означает констрейнт MonadReader r m, Has FooEnv r? Это значит, что мы ожидаем некоторое доступное для чтения окружение r, из которого можно получить значение типа FooEnv. Аналогично мы можем записать MonadError e m, CoHas FooErr e, чтобы обозначить требование контекста обработки ошибок, способного обработать значение ошибки типа FooErr.

CoHas с MonadError (как и Has с MonadReader) позволяет писать более модульный код. Вспомним о различных модулях нашего старого-доброго веб-приложения: БД-слое, веб-cервере и cron-подобном планировщике. Каждый из них теперь может иметь свой собственный тип-ошибку, и мы можем легко и просто их скомбинировать в один общий тип:

data AppError
  = AppDbError DbError
  | AppWebServerError WebServerError
  | AppCronError CronError
  deriving (Generic, CoHas DbError, CoHas WebServerError, CoHas CronError)

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

Итого: используя исключительно алгебраические соображения, мы получили ещё одно полезное (и бесплатное!) обобщение нашего подхода.

Обновляем записи

Итак, вернёмся к нашему классу Has. Мы научились извлекать значения некоторого типа part из нашего типа-произведения record. Что ещё интересненького можно сделать?

Пусть у нас есть функция f :: part -> part. Тогда мы можем получить функцию, преобразующую record, путём применения f к соответствующему полю внутри этого record:

update :: (part -> part) -> record -> record

Знакомый с концепцией линз читатель может заметить, что update вместе с extract может служить основой для построения своих собственных линз, и это неспроста, но углубляться в эту тему мы не будем.

В любом случае, после всех наших упражнений с extract и inject/coextract написание обобщённого кода для update — скукотища.

Сначала добавляем метод gupdate во вспомогательный класс GHas. Единственное отличие от gextract в том, что результат нашей функции — generic-представление записи вместо конкретного «реального» типа:

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

Затем мы добавляем реализацию gupdate к уже имеющимся инстансам GHas, имея в виду, что мы должны произвести соответствующее Generic-значение:

instance GHas 'Here rec (K1 i rec) where
  ...
  gupdate _ f (K1 x) = K1 $ f x

instance GHas path part record => GHas path part (M1 i t record) where
  ...
  gupdate proxy f (M1 x) = M1 (gupdate proxy f x)

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

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

Последним шагом мы добавляем соответствующий update-метод в класс Has и пишем реализацию по умолчанию:

class Has part record where
  ...

  update :: (part -> part) -> record -> record

  default update :: forall path. (Generic record, SuccessfulSearch part record path) => (part -> part) -> record -> record
  update f = to . gupdate (Proxy :: Proxy path) f . from

Вот и всё! Легкотня.

update и MonadState

Наш старый добрый extract особенно хорошо себя показывает в связке с MonadReader: он позволяет заменить MonadReader Foo m на (MonadReader r m, Has Foo r) для большей модульности. Зачем же может быть нужен update?

Для MonadReader update действительно не очень-то и нужен, но есть довольно близкий по духу монадический класс, естественным образом предполагающий обновления: MonadState. Так что теперь вместо MonadState FooState m мы можем писать (MonadState s m, Has FooState s), получая композабельные и повторно используемые стейтфул-функции!

Или, иными словами, мы получили обобщение Has-паттерна на окружения, доступные для записи.

С другой стороны, моё личное впечатление — потребность в композабельном состоянии возникает куда реже, чем аналогичная потребность в композабельном окружении для чтения (как с MonadReader), так что, возможно, это не столь полезно на практике.

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

Итого

Что мы сделали за эти три поста? Мы описали, что такое паттерн Has и чем он может быть полезен в контексте MonadReader. Затем мы реализовали его обобщённую версию, чтобы сократить количество скучной и однообразной писанины. И, наконец, сегодня мы применили немножко алгебраического мышления, чтобы получить дуальный Has паттерн для MonadError, ну и заодно уже без всякой алгебры (хотя она там на самом деле есть, но это совсем другая история) обобщили наш Has для работы с изменяемым состоянием в MonadState.

Автор: 0xd34df00d

Источник