Tek "FlippyFloppyMorphism" "const mempty" mi?

Sep 25 2020

Haskell'de, f :: * -> *eşzamanlı olarak a Functorve a olan herhangi bir tür kurucusunun Contravarianttür parametresinde hayali olması ilginç bir gerçeğe sahibiz :

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

Bunu ifade etmenin başka bir yolu da, aynı anda a Functors ve a olan her tür kurucu , bazıları için Contravariantdoğal olarak izomorfiktir .Const xx

Bu, sınıfı somutlaştırmanın "tek" yolunun (izomorfizme kadar) olduğu anlamına gelir:

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

functor yasalarına uyması için:

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)

dır-dir:

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

yani modulo yeni türler const id,.

Bu tatmin kısıtlamaları, ben dahil çeşitli gayri argümanlar anlayabiliyorum tür rağmen o kendi türünde tek fonksiyonudur neden anlamada güçlük absurd :: Void -> a/ discard :: a -> ()onun tipinde "hayalet olduğunu" Böyle bir haritanın varlığı functor ima neden olarak parametre.

Daha iyi anlamak için sorunu basitleştirmeye çalıştım. Düşünmek yerine şunu FlippyFloppyFunctordüşünelim:

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

benzer yasalarla:

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)

Varsayarsak ave b sigara değişmeli Monoids edilir , bunun sadece yasal uygulama hala doğrudur FlippyFloppyMorphismolduğunu const mempty? Girdi monoidlerinde morfizmin neden "hayali" olması gerektiğini, a Voidveya a'ya sahip olmadan açıklamak hala mümkün mü ()?

Yanıtlar

1 AsadSaeeduddin Sep 25 2020 at 14:43

Bana öyle geliyor ki genel durumda cevap "hayır", çünkü monoidler değişmeli olabilir.

Monoid değişmeli ise, o zaman Dual aaynı monoiddir ave Either a aaynıdır ave bu nedenle ffmorphtek homomorfizm olup olmadığını sormak için dejenere oluruz a -> b. Cevap hayır".

Örneğin, değişmeli toplama monoid için replicate 'a' :: Either (Sum Int) (Sum Int) -> String, burada:

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)

Bununla birlikte, _non_commutative monoidler için, olası tek uygulamanın const mempty(hala kanıtlayamadığım) durum olabileceğini düşünüyorum .