เฉพาะ `FlippyFloppyMorphism`` const mempty` หรือไม่

Sep 25 2020

ใน Haskell เรามีความจริงที่น่าสนใจว่าตัวสร้างประเภทใด ๆf :: * -> *ที่พร้อมกัน a Functorและ a Contravariantคือ phantom ในพารามิเตอร์ประเภท:

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

วิธีที่จะนำนี้ก็คือว่าทุกประเภทคอนสตรัคที่เป็นพร้อมกันFunctors และContravariantเป็นธรรมชาติ isomorphic ไปสำหรับบางคนConst xx

นี่หมายความว่าวิธี "เดียว" (ถึง isomorphism) ในการสร้างอินสแตนซ์ของคลาส:

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

เพื่อให้เป็นไปตามกฎหมาย 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)

คือ:

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

คือโมดูโล const idNewtypes,

ฉันพบว่ามันยากที่จะเข้าใจว่าเหตุใดจึงเป็นฟังก์ชันเดียวของประเภทที่ตรงตามข้อ จำกัด แม้ว่าฉันจะสามารถเข้าใจข้อโต้แย้งที่ไม่เป็นทางการต่างๆที่เกี่ยวข้องกับabsurd :: Void -> a/ discard :: a -> ()สาเหตุที่การมีอยู่ของแผนที่ดังกล่าวแสดงถึง functor "is phantom" ในประเภทของมัน พารามิเตอร์.

เพื่อให้เข้าใจได้ดีขึ้นฉันพยายามทำให้ปัญหาง่ายขึ้น แทนที่จะคิดถึง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 จะ monoids ไม่ใช่สับเปลี่ยนก็ยังคงเป็นความจริงที่ว่าเพียงการดำเนินการถูกต้องตามกฎหมายของการFlippyFloppyMorphismเป็นconst mempty? ยังคงเป็นไปได้หรือไม่ที่จะอธิบายว่าทำไม morphism จึงต้องเป็น "phantom" ในอินพุตโมโนด์โดยไม่ต้องมีVoidหรือ()อ้างถึง

คำตอบ

1 AsadSaeeduddin Sep 25 2020 at 14:43

สำหรับฉันแล้วดูเหมือนว่าคำตอบในกรณีทั่วไปคือ "ไม่" เพราะ monoids สามารถสับเปลี่ยนได้

ถ้าโมโนนอยด์มีการสับเปลี่ยนก็Dual aจะเป็นโมโนนอยด์เดียวกันaและEither a aก็เหมือนกับaและด้วยเหตุนี้เราจึงลดระดับลงเมื่อถามว่าffmorphโมโนนอยด์โฮโมมอร์ฟิสซึ่มเดียวa -> bหรือไม่ คำตอบคือ "ไม่"

ตัวอย่างเช่นสำหรับ monoid การสับเปลี่ยนของการบวกเรามี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(ซึ่งฉันยังไม่มีข้อพิสูจน์)