Единственный ли `FlippyFloppyMorphism` const mempty`?

Sep 25 2020

В Haskell у нас есть интересный факт, что любой конструктор типа, f :: * -> *который одновременно является a Functorи a, Contravariantявляется фантомом в своем параметре типа:

phantom :: (Functor f, Contravariant f) => f x -> f y

Другими словами, каждый конструктор типа, который одновременно является Functors и a , для некоторых Contravariantестественно изоморфен .Const xx

Это означает, что «единственный» способ (с точностью до изоморфизма) создать экземпляр класса:

class FlippyFloppyFunctor f
  where
  ffmap :: Either (y -> x) (x -> y) -> f x -> f y

так что он подчиняется законам функторов:

ffmap (Left id)       = id
ffmap (Right id)      = id
ffmap (Left  (g . f)) = ffmap (Left f)  . ffmap (Left g)
ffmap (Right (f . g)) = ffmap (Right f) . ffmap (Right g)

является:

weirdmap :: Either (y -> x) (x -> y) -> Const r x -> Const r y
weirdmap = const $ \(Const x) -> Const x

т.е. по модулю Newtypes, const id.

Мне трудно понять, почему это единственная функция своего типа, которая удовлетворяет ограничениям, хотя я могу как бы понять различные неформальные аргументы, включающие absurd :: Void -> a/ discard :: a -> ()относительно того, почему существование такой карты подразумевает, что функтор "является фантомом" в своем типе параметр.

Чтобы лучше понять это, я попытался упростить задачу. Вместо того, чтобы думать о чем-то FlippyFloppyFunctor, давайте подумаем:

class (Monoid a, Monoid b) => FlippyFloppyMorphism a b
  where
  ffmorph :: Either a a -> b

с аналогичными законами:

ffmorph (Left mempty)    = mempty
ffmorph (Right mempty)   = mempty
ffmorph (Left  (y <> x)) = ffmorph (Left x)  <> ffmorph (Left y)
ffmorph (Right (x <> y)) = ffmorph (Right x) <> ffmorph (Right y)

Предполагая, что aи b являются некоммутативными моноидами , правда ли, что единственная законная реализация FlippyFloppyMorphism- это const mempty? Можно ли еще объяснить, почему морфизм должен быть «фантомом» во входных моноидах, не имея a Voidили a ()для ссылки?

Ответы

1 AsadSaeeduddin Sep 25 2020 at 14:43

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

Если моноид коммутативен, то Dual aэто тот же моноид a, что и, и Either a aто же самое a, что и, и, следовательно, мы просто вырождаемся к вопросу, ffmorphявляется ли моноид единственным гомоморфизмом a -> b. Ответ - нет".

Например, для коммутативного моноида сложения replicate 'a' :: Either (Sum Int) (Sum Int) -> String, где:

replicateA (Left  0) = ""
replicateA (Right 0) = ""
replicateA (Left  (y + x)) = replicateA (Left x) ++ replicateA (Left y)
replicateA (Right (x + y)) = replicateA (Left x) ++ replicateA (Left y)

Однако я думаю, что для _non_commutative monoids единственная возможная реализация const mempty(для которой у меня до сих пор нет доказательства).