Алгоритм получения естественной карты

Эта запись Reddit Эдварда Кметта дает конструктивное определение < strong>естественная карта, та, что из теоремы о свободе для fmap (которую я прочитал в еще одном сообщение Эдварда Кметта):

Для заданных f, g, h и k таких, что f . g = h . k: $map f . fmap g = fmap h . $map k, где $map — естественная карта для данного конструктора.

Я не совсем понимаю алгоритм. Давайте подойдем к этому шаг за шагом:

Мы можем определить естественную карту с помощью индукции по любому конкретному выбору F, который вы даете. В конечном счете любой такой АТД состоит из сумм, произведений, (->), 1, 0, a, вызовов других функторов и т. д.

Рассмотреть возможность:

data Smth a = A a a a | B a (Maybe a) | U | Z Void deriving ...

Никаких стрел. Давайте посмотрим, как fmap (который я считаю естественным выбором для любого АТД без (->)) будет работать здесь:

instance Functor Smth where
  fmap xy (A x x1 x2)  = A (xy x) (xy x1) (xy x2)
  fmap xy (B x xPlus1) = B (xy x) (fmap xy xPlus1) 
  -- One can pattern-match 'xPlus1' as 'Just x1' and 'Nothing'.
  -- From my point of view, 'fmap' suits better here. Reasons below.
  fmap _xy U     = U 
  fmap _xy (Z z) = absurd z

Что кажется естественным. Говоря более формально, мы применяем xy к каждому x, применяем fmap xy к каждому T x, где T — это Functor, оставляем все единицы без изменений и передаем каждое Void в absurd. Это работает и для рекурсивных определений!

data Lst a = Unit | Prepend a (Lst a) deriving ...

instance Functor Lst where
    fmap xy Unit             = Unit
    fmap xy (Prepend x lstX) = Prepend (xy x) (fmap xy lstX)

А для неиндуктивных типов: _{(Подробное объяснение в этом ответе под связанным постом.)}

Graph a = Node a [Graph a]

instance Functor Graph where
    fmap xy (Node x children) = Node (xy x) (fmap (fmap xy) children) 

Эта часть ясна.

Когда мы разрешаем (->), у нас появляется первое, что смешивает дисперсию. Аргумент левого типа (->) находится в контравариантной позиции, правая часть находится в ковариантной позиции. Таким образом, вам нужно отслеживать конечную переменную типа по всему АТД и смотреть, встречается ли она в положительной и/или отрицательной позиции.

Теперь включаем (->)s. Попробуем продолжить эту индукцию:

Каким-то образом мы получили естественные карты для T a и S a. Таким образом, мы хотим рассмотреть следующее:

data T2S a = T2S (T a -> S a)

instance ?Class? T2S where
    ?map? ?? (T2S tx2sx) = T2S $ \ ty -> ???

И я считаю, что это тот момент, когда мы начинаем выбирать. У нас есть следующие варианты:

• (Phantom) a не встречается ни в T, ни в S. a в T2S является фантомным, поэтому мы можем реализовать как fmap, так и contramap как const phantom.
• (Ковариант) a встречается в S a и не встречается в T a. Таким образом, это что-то из строк ReaderT с S a (которое на самом деле не зависит от a) как окружение, которое заменяет ?Class? на Functor, ?map? на fmap, ???, ?? на xy на:

  let tx = phantom ty 
      sx = tx2sx tx
      sy = fmap xy sx
  in sy
  

• (контравариант) a встречается в T a и не встречается в S a. Я не вижу способа сделать эту штуку ковариантным функтором, поэтому мы реализуем здесь экземпляр Contravariant, который заменяет ?map? на contramap, ?? на yx, ??? на:

  let tx = fmap yx ty 
      sx = tx2sx tx
      sy = phantom sx 
  in sy
  

• (неизменяемый) a встречается как в T a, так и в S a. Мы больше не можем использовать phantom, что очень кстати. Существует модуль Data.Functor.Invariant от Эдварда Кметта. . Он предоставляет следующий класс с картой:

  class Invariant f where
    invmap :: (a -> b) -> (b -> a) -> f a -> f b
    -- and some generic stuff...
  

  И все же я не вижу способа превратить это во что-то, что мы могли бы включить в свободную теорему для fmap — этот тип требует дополнительной функции-аргумента, которая мы не можем отмахнуться как id или что-то в этом роде. Так или иначе, мы ставим invmap вместо ?map?, xy yx вместо ?? и следующее вместо ???:

  let tx = fmap yx ty 
      sx = tx2sx tx
      sy = fmap xy sx
  in sy
  

Итак, правильно ли я понимаю такой алгоритм? Если да, то как нам правильно обработать случай Invariant?