유일한`FlippyFloppyMorphism``const mempty`입니까?

Question

Haskell에서 우리는 f :: * -> *a Functor와 a Contravariant가 동시에 존재 하는 모든 타입 생성자 가 그 타입 매개 변수에서 유령 이라는 흥미로운 사실을 가지고 있습니다 .

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

이것을 넣는 또 다른 방법은 Functors와 a Contravariant가 동시에있는 모든 유형 생성자가 Const x일부에 대해 자연스럽게 동형 이라는 것 입니다 x.

이것은 클래스를 인스턴스화하는 "유일한"방법 (동형까지)을 의미합니다.

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)

is :

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 비 교환 법칙이 성립 monoids을하는 , 그것의 유일한 합법적 구현하는 것이 여전히 사실 FlippyFloppyMorphism이다 const mempty? 참조 할 Void또는 a 없이 입력 모노 이드에서 형태가 "가상"이어야하는 이유를 설명 할 ()수 있습니까?

Answer 1

모노 이드는 교환적일 수 있기 때문에 일반적인 경우의 대답은 "아니오"인 것 같습니다.

만약 모노 이드가 교환 적이라면,는와 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(아직도 증거가 없습니다) 일 수 있다고 생각합니다 .