haskell - すべての代替モナドはフィルター可能ですか?

Question

セットのカテゴリは、デカルト モノイドとコデカルト モノイドの両方です。これら 2 つのモノイド構造を示す正準同型のタイプを以下に示します。

type x + y = Either x y
type x × y = (x, y)

data Iso a b = Iso { fwd :: a -> b, bwd :: b -> a }

eassoc :: Iso ((x + y) + z) (x + (y + z))
elunit :: Iso (Void + x) x
erunit :: Iso (x + Void) x

tassoc :: Iso ((x × y) × z) (x × (y × z))
tlunit :: Iso (() × x) x
trunit :: Iso (x × ()) x

---

この質問の目的のために、テンソルの下の Hask からテンソルAlternativeの下の Hask への緩いモノイド関手であると定義します(それ以上ではありません)。Either(,)

class Functor f => Alt f
  where
  union :: f a × f b -> f (a + b)

class Alt f => Alternative f
  where
  nil :: () -> f Void

法則は、緩いモノイド関手の場合のものです。

結合性:

fwd tassoc >>> bimap id union >>> union
=
bimap union id >>> union >>> fmap (fwd eassoc)

左ユニット:

fwd tlunit
=
bimap nil id >>> union >>> fmap (fwd elunit)

右ユニット:

fwd trunit
=
bimap id nil >>> union >>> fmap (fwd erunit)

Alternative以下は、緩いモノイド ファンクター エンコーディングのコヒーレンス マップに関して、型クラスのより使い慣れた操作を復元する方法です。

(<|>) :: Alt f => f a -> f a -> f a
x <|> y = either id id <$> union (Left <$> x, Right <$> y)

empty :: Alternative f => f a
empty = absurd <$> nil ()

---

ファンクターを、テンソルの下の Hask からテンソルの下の Hask へのoplaxモノイド ファンFilterableクターと定義します。Either(,)

class Functor f => Filter f
  where
  partition :: f (a + b) -> f a × f b

class Filter f => Filterable f
  where
  trivial :: f Void -> ()
  trivial = const ()

その法則を後ろ向きに持つと、緩いモノイド関手の法則が得られます:

結合性:

bwd tassoc <<< bimap id partition <<< partition
=
bimap partition id <<< partition <<< fmap (bwd eassoc)

左ユニット:

bwd tlunit
=
bimap trivial id <<< partition <<< fmap (bwd elunit)

右ユニット:

bwd trunit
=
bimap id trivial <<< partition <<< fmap (bwd erunit)

oplax モノイド ファンクター エンコーディングのようなmapMaybeおよびに関する標準のフィルター y 関数の定義は、関心のある読者への演習として残されています。filter

mapMaybe :: Filterable f => (a -> Maybe b) -> f a -> f b
mapMaybe = _

filter :: Filterable f => (a -> Bool) -> f a -> f a
filter = _

---

Alternative Monad問題は次のとおりFilterableです。

テトリスを実装する方法を入力できます。

instance (Alternative f, Monad f) => Filter f
  where
  partition fab = (fab >>= either return (const empty), fab >>= either (const empty) return)

しかし、この実装は常に合法ですか? それは時々合法ですか（「時々」の正式な定義について）？証明、反例、および/または非公式の議論はすべて非常に役立ちます。ありがとう。