На самом деле ученые всегда стремятся к каким-то достижениям. Они думают только о том, удастся ли это им что-то совершить. И они почему-то никогда не задумываются а стоит ли вообще совершать это что-то?
Ян Малкольм, Парк Юрского Периода

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

Денотационный дизайн предназначен для формального описания этих предпочтений. Он позволяет посмотреть на эти интерфейсы и определить, являются ли они корректными.

Этот очерк изложение прекрасной статьи Denotational design with type class morphisms от Conal Elliot.

Пример: ассоциативные контейнеры

Давайте рассмотрим Data.Map.Map. Основной интерфейс выражается следующими операциями:

empty  :: Map k vinsert :: k -> v -> Map k v -> Map k vlookup :: k -> Map k v -> Maybe vunion  :: Map k v -> Map k v -> Map k v

для которых должны выполняться законы:

-- получаем обратно то, что вставилиlookup k   (insert k v m) = Just v-- ключи заменяют друг другаinsert k b (insert k a m) = insert k b m-- empty  единица для операции объединенияunion empty m = munion m empty = m-- union  это просто последовательность insert'овinsert k v m = union (insert k v empty) m

Это далеко не все необходимые условия, но обсуждение недостающих законов уведёт нас слишком далеко от сути поста прим. пер.

Эти законы соответствуют нашим ожиданиям от абстракции, предоставляемой Map, и, более того, точно описывают желаемую семантику этих операций. Хотя явное описание таких очевидных законов может выглядеть глупой тратой времени, именно подобные законы придают абстракциям смысл.

Рассмотрим другой пример:

empathy :: r -> f -> X r f -> X r ffear    :: e -> X e m -> Either () mtaste   :: X o i -> X o i -> X o izoo     :: X z x

При должном внимании можно заметить, что этот X вместе с этими функциями просто результат случайного переименования имён в Map. Имена важны для нас только потому, что они подталкивают нас к смыслам вещей, обозначаемых этими именами. Однако, если мы применим аналогичное переименование к законам Map, они всё ещё будут выражать желаемую семантику. Вывод прост: имена полезны, законы фундаментальны.

Смыслы

Законы выше пример одного из способов определить семантику наших абстракций. Давайте чуть подробнее рассмотрим другой способ.

Введём понятие смыслового функтора . Можно думать о (Map k v) как о смысле Map k v. (Map k v) показывает не реализацию Map k v, а то, как мы должны рассуждать о ней, какую метафору использовать для Map. Функтор , как и любой другой (эндо)функтор, отображает типы на типы, а функции на функции.

Map можно закодировать как функцию, а потенциальное отсутствие ключа выразить через Maybe:

(Map k v) = k -> Maybe v

После того, как мы определились со смыслом нашего типа, можно определить смыслы примитивных операций на Map.

Пустой контейнер просто возвращает Nothing для любого ключа:

(empty) = \k -> Nothing

Поиск ключа это просто вызов функции с соответствующим аргументом и возврат полученного значения:

(lookup k m) = (m) k

Если ключ, который мы ищем, равен только что вставленному, то вернём его:

(insert k' v m) = \k ->  if k == k'    then Just v    else (m) k

Поиск ключа в объединении двух мап это поиск сначала в левой, а потом, при неуспехе, в правой:

(union m1 m2) = \k ->  case (m1) k of    Just v  -> Just v    Nothing -> (m2) k

Эти определения выражают интуитивные (пусть и, возможно, наивные) смысл и реализацию Map. Независимо от окончательной реализации, это функтор, который преобразует эту реализацию в такую же структуру (что бы это ни значило) из функций.

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

Конечно же, это не значит, что X = (X). Вопросы производительности или другие инженерные соображения могут сделать такое равенство неразумным в самом деле, было бы полным безумием на самом деле реализовать Map как огромную цепочку вложенных if. Достаточно того, что никакая часть фактической реализации не имеет права разрушить нашу хрупкую веру в то, что мы на самом деле работаем с (Map). Как ни странно, это весьма желательное свойство: мы гораздо лучше знакомы с обычными функциями и другими базовыми типами, чем с остальной экосистемой языка (включая, возможно, довольно тёмные её уголки).

Условие X (X) ограничивает нас гораздо больше, чем это могло бы показаться на первый взгляд. Например, это условие требует, чтобы все инстансы всех тайпклассов совпадали на X и на (X), так как иначе нам бы удалось их различить.

Наша Map очевидным образом является моноидом, так что давайте это выразим:

instance Monoid (Map k v) where  mempty  = empty  mappend = union

Хотя это, конечно, корректный моноид, у нас уже возникли проблемы. Инстанс Monoid, который для функций в общем виде выглядит как Monoid b => Monoid (a -> b), для (Map) после специализации для наших конкретных типов будет выглядеть так:

instance Monoid v => Monoid (k -> Maybe v) where  ...

Сразу ясно, что эти два определения моноидов никак не могут совпадать. Чёрт. Кажется, что-то пошло не так, и наш (Map) на самом деле не является денотацией Map. Впрочем, ничего страшного: ошибки случаются. А мы остались с интересным вопросом: ошибка в нашем смысловом функторе, или же исходный API некорректен?

Гомоморфизмы

Наши инстансы Monoid (Map k v) и Monoid (Map k v) не совпадают, то есть, (Map) не может быть денотацией для Map. Мы вынуждены жить с тяжёлым знанием о том, что то ли , то ли сама Map неверна, но без какой-то дополнительной информации мы ничего не можем исправить.

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

Например, давайте посмотрим на определение Functor для типа-пары (a, b):

instance Functor ((,) a) where  fmap f (a, b) = (a, f b)

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

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

instance Functor (X) where  (fmap f x) = fmap f (x)instance Applicative (X) where  (pure x)  = pure x  (f <*> x) = (f) <*> (x)

и так далее.

Теперь у нас есть простой тест на корректность смыслового функтора: если какой-либо инстанс не эквивалентен такой форме, то смысл точно неправильный. Давайте посмотрим на реализацию mempty:

(mempty) = \k -> Nothing          = \k -> mempty          = const mempty          = mempty  -- (1)

В (1) мы сворачиваем const mempty в mempty, так как это определение для Monoid ((->) a). Пока что наш смысл выглядит как настоящая денотация. Давайте посмотрим на mappend:

(mappend m1 m2) = \k ->  case (m1) k of    Just v  -> Just v    Nothing -> (m2) k

Сходу непонятно, как это превратить в гомоморфизм, так что давайте зайдём с другой стороны и посмотрим, получится ли у нас что-то разумное:

mappend (m1) (m2)    = mappend (\k -> v1) (\k -> v2)    = \k -> mappend v1 v2    = \k ->        case v1 of   -- (2)          z@(Just a) ->            case v2 of              Just b  -> Just $ mappend a b              Nothing -> z          Nothing -> v2

В (2) мы используем определение mappend для Maybe.

Дальше опять непонятно, как продвигаться, но, к счастью, уже ясно, что наши инстансы не совпадают. mappend для (Map) предпочитает ключи слева, тогда как mappend для денотации нет.

Получается, наш смысловой функтор неверен: либо представление (Map) неправильно, либо (mappend). К счастью, мы вольны поменять их так, чтобы всё совпадало. При этом мы уверены, что предпочтение левых ключей желаемое поведение, так что нужно менять представление.

К счастью, есть простое исправление: в Data.Monoid есть тип-обёртка First, как раз предоставляющий нужную семантику. Подстановка даёт нам

(Map k v) = k -> First v

Последующий анализ для этого определения (Map) показывает, что требование гомоморфизмов удовлетворено. Соответствующая проверка представляется читателю в качестве упражнения.

(Де)композиция функторов

Мы вывели денотацию Map и даже получили разумный инстанс Monoid. Возникает следующий вопрос: какие ещё инстансы мы должны обеспечить для Map?

Разумеется, Map Functor, но является ли она Applicative? Конечно, есть реализации Applicative (Map k), но неочевидно, какую из них мы должны дать. В частности, какова должна быть семантика pure 17? Возможно, мы должны получить Map с одним значением (собственно, 17), но какому ключу оно должно соответствовать? Мы не знаем, если не потребуем, чтобы k было моноидом.

С другой стороны, мы могли бы вернуть Map, в которой каждый ключ отображается в 17. Эта реализация согласуется с аппликативным инстансом для (Map), но не согласуется с нашей интуицией хотя переводчик тут бы поспорил на мой взгляд, это вполне разумная семантика . А вообще мы могли бы последовать за Data.Map.Map, которая здесь ни рыба, ни мясо, и вообще не предоставляет инстанса Applicative.

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

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

Возьмём тип Compose и снова подумаем о принятых нами ранее решениях (что вообще распространённая практика в денотационном дизайне):

data Compose f g a = Compose  { getCompose :: f (g a)  }

Compose прекрасный инструмент для создания новых типов как композиций других типов. Например, рассмотрим смысл (Map k v) = \k -> First v. Если мы хотим fmapнуть v, нам придётся писать fmap дважды:

           f  ::         v  ->         wfmap (fmap f) :: (Map k v) -> (Map k w)

Выглядит как несущественная ерунда, но на самом деле тут скрыта большая проблема. Нам не только нужно продираться через два слоя функторов, но, что куда хуже, мы можем сломать нашу абстракцию, используя один fmap. Например, fmap (const 5) превратит наш (Map k v) в функцию k -> 5, которая, конечно, уже никак не связана с Map. Блин.

Вместо этого мы можем снова поправить определение (Map k v):

(Map k v) = Compose ((->) k) First v

Теперь становится видна ещё одна интерпретация нашего типа. (Map) это композиция какого-то отображения ((->) k) и частичности (First). Отображение, конечно, является основой нашей концепции, но частичность обосновать сложнее. С одной стороны, можно сказать, что Nothing используется для обозначения отсутствующего ключа, но есть и другая интерпретация: Nothing это значение по умолчанию.

Если немного пораздумывать о второй интерпретации, то становится ясно, что частичное отображение k -> Maybe v это просто частный случай тотального отображения k -> v, где само значение частичное. Возможно, частичность вообще неважна для семантики, которую мы хотим выразить.

В качестве нашей окончательной (и в итоге правильной) попытки, мы определяем

(Map k v) = \k -> v

Теперь вопрос о том, какие тайпклассы нужно реализовать, становится очевидным эквивалентные таковым для k -> v. Вопрос о том, что должен делать инстанс Applicative, тоже разрешается: то же, что и для стрелки.

Стоит отдельно отметить, что хоть мы и определили смысл Map k v как k -> v, это не значит, что такой же должна быть и реализация. Например, можно представить себе такое определение Map:

data Map k v = Map  { mapDefVal :: v  , mapTree   :: BalancedTree k v  }lookup :: Ord k => Map k v -> k -> vlookup m = fromMaybe (mapDefVal m) . treeLookup (mapTree m)

Такая реализация даёт нам все асимптотики деревьев вместе с денотациями функций (и, как следствие, рассуждениями о Map как о функциях).

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