Единственный ли `FlippyFloppyMorphism` const mempty`?
В 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 ()для ссылки?
Ответы
Мне кажется, что в общем случае ответ отрицательный, потому что моноиды могут быть коммутативными.
Если моноид коммутативен, то 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(для которой у меня до сих пор нет доказательства).