Có phải chỉ `FlippyFloppyMorphism`` const mempty` không?

Question

Trong Haskell, chúng ta có một thực tế thú vị rằng bất kỳ hàm tạo kiểu f :: * -> *nào đồng thời là a Functorvà a Contravariantđều là ảo trong tham số kiểu của nó:

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

Một cách khác để giải thích điều này là mọi hàm tạo kiểu đồng thời là Functors và a Contravariantđều là đẳng cấu đối với Const x, đối với một số x.

Điều này ngụ ý rằng cách "duy nhất" (tối đa là đẳng cấu) để khởi tạo lớp:

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

để nó tuân theo luật functor:

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)

Là:

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

tức là kiểu mới modulo , const id.

Tôi cảm thấy khó hiểu tại sao đây là hàm duy nhất của loại nó đáp ứng các ràng buộc, mặc dù tôi có thể hiểu nhiều đối số không chính thức khác nhau liên quan đến absurd :: Void -> a/ discard :: a -> ()tại sao sự tồn tại của một bản đồ như vậy ngụ ý hàm functor "là ma" trong loại của nó tham số.

Để hiểu rõ hơn, tôi đã cố gắng đơn giản hóa vấn đề. Thay vì nghĩ về FlippyFloppyFunctor, hãy nghĩ về:

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

với các luật tương tự:

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)

Giả sử avà b được monoids phi giao hoán , là nó vẫn còn đúng rằng việc thực hiện hợp pháp duy nhất của FlippyFloppyMorphismlà const mempty? Vẫn có thể giải thích tại sao biến hình phải là "ma" trong các đơn chất đầu vào, mà không có a Voidhoặc a ()để tham chiếu?

Answer 1

Đối với tôi, dường như câu trả lời trong trường hợp chung là "không", bởi vì các đơn thức có thể mang tính chất giao hoán.

Nếu monoid là giao hoán, thì Dual amonoid giống như a, và Either a agiống như a, và do đó chúng ta chỉ suy biến thành câu hỏi liệu có phải ffmorphlà phép đồng hình monoid duy nhất hay không a -> b. Câu trả lời là không".

Ví dụ, đối với đơn thức giao hoán của phép cộng, chúng ta có replicate 'a' :: Either (Sum Int) (Sum Int) -> String, trong đó:

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)

Tuy nhiên, tôi nghĩ có thể xảy ra trường hợp đối với _non_commutative monoids, cách triển khai duy nhất có thể xảy ra const mempty(mà tôi vẫn chưa có bằng chứng).