¿Todas las mónadas alternativas se pueden filtrar?

La categoría de conjuntos es tanto monoidal cartesiana como monoidal cocartesiana. Los tipos de isomorfismos canónicos que presencian estas dos estructuras monoidales se enumeran a continuación:

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

A los fines de esta pregunta, defino que soy Alternativeun functor monoidal laxo desde Hask bajo el Eithertensor hasta Hask bajo el (,)tensor (y no más):

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

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

Las leyes son solo las de un functor monoidal laxo.

Asociatividad:

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

Unidad izquierda:

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

Unidad correcta:

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

Aquí se explica cómo recuperar las operaciones más familiares para la Alternativeclase de tipos en términos de los mapas de coherencia de la codificación del functor monoidal laxo:

(<|>) :: 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 ()

Defino Filterablefuntores ser oplax funtores monoidales de Hask bajo el Eithertensor a Hask bajo el (,)tensor:

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 ()

Teniendo para sus leyes solo leyes de functor monoidal laxas hacia atrás:

Asociatividad:

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

Unidad izquierda:

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

Unidad correcta:

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

La definición de funciones de filtro y estándar como mapMaybey filteren términos de la codificación del functor monoidal oplax se dejó como ejercicio para el lector interesado:

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

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

La pregunta es esta: ¿es cada Alternative Monadtambién Filterable?

Podemos tetris tetris nuestro camino a una implementación:

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

Pero, ¿es esta implementación siempre legal? ¿A veces es legal (para alguna definición formal de "a veces")? Las pruebas, contraejemplos y / o argumentos informales serían muy útiles. Gracias.

Aquí va un argumento que apoya ampliamente su hermosa idea.

Primera parte: mapMaybe

Mi plan aquí es replantear el problema en términos de mapMaybe, con la esperanza de que hacerlo nos lleve a un terreno más familiar. Para hacerlo, Eitherusaré algunas funciones de utilidad que cambian:

maybeToRight :: a -> Maybe b -> Either a b
rightToMaybe :: Either a b -> Maybe b
leftToMaybe :: Either a b -> Maybe a
flipEither :: Either a b -> Either b a

(Tomé los primeros tres nombres de relude , y el cuarto de errores . Por cierto, ofertas de erroresmaybeToRight y rightToMaybecomo notey hushrespectivamente, en Control.Error.Util).

Como notó, mapMaybese puede definir en términos de partition:

mapMaybe :: Filterable f => (a -> Maybe b) -> f a -> f b
mapMaybe f = snd . partition . fmap (maybeToRight () . f)

De manera crucial, también podemos dar la vuelta:

partition :: Filterable f => f (Either a b) -> (f a, f b)
partition = mapMaybe leftToMaybe &&& mapMaybe rightToMaybe

Esto sugiere que tiene sentido reformular sus leyes en términos de mapMaybe. Con las leyes de identidad, hacerlo nos da una gran excusa para olvidarnos por completo de trivial:

-- Left and right unit
mapMaybe rightToMaybe . fmap (bwd elunit) = id  -- [I]
mapMaybe leftToMaybe . fmap (bwd erunit) = id   -- [II]

En cuanto a la asociatividad, podemos usar rightToMaybey leftToMaybedividir la ley en tres ecuaciones, una para cada componente que obtenemos de las particiones sucesivas:

-- Associativity
mapMaybe rightToMaybe . fmap (bwd eassoc)
    = mapMaybe rightToMaybe . mapMaybe rightToMaybe  -- [III]
mapMaybe rightToMaybe . mapMaybe leftToMaybe . fmap (bwd eassoc)
    = mapMaybe leftToMaybe . mapMaybe rightToMaybe   -- [IV]
mapMaybe leftToMaybe . fmap (bwd eassoc)
    = mapMaybe leftToMaybe . mapMaybe leftToMaybe    -- [V]

Parametricity significa mapMaybees agnóstico con respecto a los Eithervalores que estamos tratando aquí. Siendo así, podemos usar nuestro pequeño arsenal de Eitherisomorfismos para barajar las cosas y mostrar que [I] es equivalente a [II], y [III] es equivalente a [V]. Ahora tenemos tres ecuaciones:

mapMaybe rightToMaybe . fmap (bwd elunit) = id       -- [I]
mapMaybe rightToMaybe . fmap (bwd eassoc)
    = mapMaybe rightToMaybe . mapMaybe rightToMaybe  -- [III]
mapMaybe rightToMaybe . mapMaybe leftToMaybe . fmap (bwd eassoc)
    = mapMaybe leftToMaybe . mapMaybe rightToMaybe   -- [IV]

La parametricidad nos permite tragar la fmapin [I]:

mapMaybe (rightToMaybe . bwd elunit) = id

Eso, sin embargo, es simplemente ...

mapMaybe Just = id

... que es equivalente a la ley de conservación / identidad de Witherable 'sFilterable :

mapMaybe (Just . f) = fmap f

Eso Filterabletambién tiene una ley de composición:

-- The (<=<) is from the Maybe monad.
mapMaybe g . mapMaybe f = mapMaybe (g <=< f)

¿Podemos también derivar esto de nuestras leyes? Comencemos desde [III] y, una vez más, hagamos que la parametricidad haga su trabajo. Este es más complicado, así que lo escribiré en su totalidad:

mapMaybe rightToMaybe . fmap (bwd eassoc)
    = mapMaybe rightToMaybe . mapMaybe rightToMaybe  -- [III]

-- f :: a -> Maybe b; g :: b -> Maybe c
-- Precomposing fmap (right (maybeToRight () . g) . maybeToRight () . f)
-- on both sides:
mapMaybe rightToMaybe . fmap (bwd eassoc)
  . fmap (right (maybeToRight () . g) . maybeToRight () . f)
    = mapMaybe rightToMaybe . mapMaybe rightToMaybe 
      . fmap (right (maybeToRight () . g) . maybeToRight () . f)

mapMaybe rightToMaybe . mapMaybe rightToMaybe 
  . fmap (right (maybeToRight () . g) . maybeToRight () . f)  -- RHS
mapMaybe rightToMaybe . fmap (maybeToRight () . g)
  . mapMaybe rightToMaybe . fmap (maybeToRight () . f)
mapMaybe (rightToMaybe . maybeToRight () . g)
 . mapMaybe (rightToMaybe . maybeToRight () . f)
mapMaybe g . mapMaybe f

mapMaybe rightToMaybe . fmap (bwd eassoc)
  . fmap (right (maybeToRight () . g) . maybeToRight () . f)  -- LHS
mapMaybe (rightToMaybe . bwd eassoc 
    . right (maybeToRight () . g) . maybeToRight () . f)
mapMaybe (rightToMaybe . bwd eassoc 
    . right (maybeToRight ()) . maybeToRight () . fmap @Maybe g . f)
-- join @Maybe
--     = rightToMaybe . bwd eassoc . right (maybeToRight ()) . maybeToRight ()
mapMaybe (join @Maybe . fmap @Maybe g . f)
mapMaybe (g <=< f)  -- mapMaybe (g <=< f) = mapMaybe g . mapMaybe f

En la otra dirección:

mapMaybe (g <=< f) = mapMaybe g . mapMaybe f
-- f = rightToMaybe; g = rightToMaybe
mapMaybe (rightToMaybe <=< rightToMaybe)
    = mapMaybe rightToMaybe . mapMaybe rightToMaybe
mapMaybe (rightToMaybe <=< rightToMaybe)  -- LHS
mapMaybe (join @Maybe . fmap @Maybe rightToMaybe . rightToMaybe)
-- join @Maybe
--     = rightToMaybe . bwd eassoc . right (maybeToRight ()) . maybeToRight ()
mapMaybe (rightToMaybe . bwd eassoc 
    . right (maybeToRight ()) . maybeToRight ()
      . fmap @Maybe rightToMaybe . rightToMaybe)
mapMaybe (rightToMaybe . bwd eassoc 
    . right (maybeToRight () . rightToMaybe) 
      . maybeToRight () . rightToMaybe)
mapMaybe (rightToMaybe . bwd eassoc)  -- See note below.
mapMaybe rightToMaybe . fmap (bwd eassoc)
-- mapMaybe rightToMaybe . fmap (bwd eassoc)
--     = mapMaybe rightToMaybe . mapMaybe rightToMaybe

(Nota: mientras maybeToRight () . rightToMaybe :: Either a b -> Either () bno lo esté id, en la derivación arriba los valores de la izquierda se descartarán de todos modos, por lo que es justo tacharlo como si lo fuera id).

Por lo tanto, [III] es equivalente a la ley de composición de witherable 's Filterable.

En este punto, podemos usar la ley de composición para tratar [IV]:

mapMaybe rightToMaybe . mapMaybe leftToMaybe . fmap (bwd eassoc)
    = mapMaybe leftToMaybe . mapMaybe rightToMaybe   -- [IV]
mapMaybe (rightToMaybe <=< leftToMaybe) . fmap (bwd eassoc)
    = mapMaybe (letfToMaybe <=< rightToMaybe)
mapMaybe (rightToMaybe <=< leftToMaybe . bwd eassoc)
    = mapMaybe (letfToMaybe <=< rightToMaybe)
-- Sufficient condition:
rightToMaybe <=< leftToMaybe . bwd eassoc = letfToMaybe <=< rightToMaybe
-- The condition holds, as can be directly verified by substiuting the definitions.

Esto es suficiente para mostrar que su clase equivale a una formulación bien establecida de Filterable, que es un resultado muy bueno. Aquí hay un resumen de las leyes:

mapMaybe Just = id                            -- Identity
mapMaybe g . mapMaybe f = mapMaybe (g <=< f)  -- Composition

Como señalan los doctores , estas son leyes de functor para un functor desde Kleisli Maybe hasta Hask .

Segunda parte: alternativa y mónada

Ahora podemos abordar su pregunta real, que era sobre mónadas alternativas. Su implementación propuesta de partitionfue:

partitionAM :: (Alternative f, Monad f) => f (Either a b) -> (f a, f b)
partitionAM
    = (either return (const empty) =<<) &&& (either (const empty) return =<<)

Siguiendo mi plan más amplio, pasaré a la mapMaybepresentación:

mapMaybe f
snd . partition . fmap (maybeToRight () . f)
snd . (either return (const empty) =<<) &&& (either (const empty) return =<<)
    . fmap (maybeToRight () . f)
(either (const empty) return =<<) . fmap (maybeToRight () . f)
(either (const empty) return . maybeToRight . f =<<)
(maybe empty return . f =<<)

Y así podemos definir:

mapMaybeAM :: (Alternative f, Monad f) => (a -> Maybe b) -> f a -> f b
mapMaybeAM f u = maybe empty return . f =<< u

O, en una ortografía sin puntos:

mapMaybeAM = (=<<) . (maybe empty return .)

Algunos párrafos anteriores, noté que las Filterableleyes dicen que mapMaybees el mapeo de morfismo de un functor desde Kleisli Maybe hasta Hask . Dado que la composición de los functores es un functor, y (=<<)el mapeo de morfismo de un functor de Kleisli f a Hask , (maybe empty return .)el mapeo de morfismo de un functor de Kleisli Quizás a Kleisli f es suficiente para mapMaybeAMser legal. Las leyes de functor relevantes son:

maybe empty return . Just = return  -- Identity
maybe empty return . g <=< maybe empty return . f
    = maybe empty return . (g <=< f)  -- Composition

Esta ley de identidad es válida, así que centrémonos en la composición uno:

maybe empty return . g <=< maybe empty return . f
    = maybe empty return . (g <=< f)
maybe empty return . g =<< maybe empty return (f a)
    = maybe empty return (g =<< f a)
-- Case 1: f a = Nothing
maybe empty return . g =<< maybe empty return Nothing
    = maybe empty return (g =<< Nothing)
maybe empty return . g =<< empty = maybe empty return Nothing
maybe empty return . g =<< empty = empty  -- To be continued.
-- Case 2: f a = Just b
maybe empty return . g =<< maybe empty return (Just b)
    = maybe empty return (g =<< Just b)
maybe empty return . g =<< return b = maybe empty return (g b)
maybe empty return (g b) = maybe empty return (g b)  -- OK.

Por lo tanto, mapMaybeAMes legal si es maybe empty return . g =<< empty = emptypor alguno g. Ahora, si emptyse define como absurd <$> nil (), como lo ha hecho aquí, podemos probarlo f =<< empty = emptypara cualquier f:

f =<< empty = empty
f =<< empty  -- LHS
f =<< absurd <$> nil ()
f . absurd =<< nil ()
-- By parametricity, f . absurd = absurd, for any f.
absurd =<< nil ()
return . absurd =<< nil ()
absurd <$> nil ()
empty  -- LHS = RHS

Intuitivamente, si emptyestá realmente vacío (como debe ser, dada la definición que estamos usando aquí), no habrá valores para faplicar, por f =<< emptylo que no puede resultar en nada más que empty.

Un enfoque diferente aquí sería investigar la interacción de las clases Alternativey Monad. Da la casualidad que hay una clase de mónadas alternativas: MonadPlus. En consecuencia, un rediseñado mapMaybepodría verse así:

-- Lawful iff, for any f, mzero >>= maybe empty mzero . f = mzero
mmapMaybe :: MonadPlus m => (a -> Maybe b) -> m a -> m b
mmapMaybe f m = m >>= maybe mzero return . f

Si bien existen diversas opiniones sobre qué conjunto de leyes es el más apropiado MonadPlus, una de las leyes que nadie parece objetar es ...

mzero >>= f = mzero  -- Left zero

... que es precisamente la propiedad de la emptyque estábamos discutiendo algunos párrafos anteriores. La legalidad de mmapMaybesigue inmediatamente de la ley cero izquierda.

(Por cierto, Control.Monadproporcionamfilter :: MonadPlus m => (a -> Bool) -> m a -> m a , que coincide con el filterque podemos definir usando mmapMaybe).

En resumen:

Pero, ¿es esta implementación siempre legal? ¿A veces es legal (para alguna definición formal de "a veces")?

Sí, la implementación es legal. Esta conclusión depende del emptyhecho de que esté vacío, como debería, o de la mónada alternativa relevante que sigue la MonadPlusley de cero a la izquierda , que se reduce a casi lo mismo.

Vale la pena enfatizar que Filterableno está subsumido MonadPlus, como podemos ilustrar con los siguientes contraejemplos:

• ZipList: filtrable, pero no una mónada. La Filterableinstancia es la misma que para las listas, a pesar de Alternativeque es diferente.

• Map: filtrable, pero ni mónada ni aplicativo. De hecho, Mapni siquiera puede ser aplicativo porque no hay una implementación sensata de pure. Sin embargo, tiene el suyo empty.

• MaybeT f: mientras que sus instancias Monady deben ser una mónada, y una definición aislada necesitaría al menos , la instancia solo requiere (cualquier cosa se puede filtrar si desliza una capa en ella).AlternativefemptyApplicativeFilterableFunctor fMaybe

Tercera parte: vacía

En este punto, uno todavía podría preguntarse qué tan importante es un papel emptyo qué nilrealmente juega Filterable. No es un método de clase y, sin embargo, la mayoría de las instancias parecen tener una versión sensata del mismo.

De lo único que podemos estar seguros es que, si el tipo filtrable tiene habitantes, al menos uno de ellos será una estructura vacía, porque siempre podemos tomar a cualquier habitante y filtrar todo:

chop :: Filterable f => f a -> f Void
chop = mapMaybe (const Nothing)

La existencia de chop, sin embargo, no significa que habrá un solo nil valor vacío, o que chopsiempre dará el mismo resultado. Consideremos, por ejemplo, MaybeT IOcuyo Filterableejemplo podría ser considerado como una forma de censurar los resultados de IOlos cálculos. La instancia es perfectamente legal, aunque choppuede producir MaybeT IO Voidvalores distintos que conllevan IOefectos arbitrarios .

En una nota final, usted ha aludido a la posibilidad de trabajar con fuertes funtores monoidales, por lo que Alternativey Filterableestán vinculados al hacer union/ partitiony nil/ trivialisomorfismos. Tener uniony partitioncomo inversos mutuos es concebible pero bastante limitante, dado que union . partitiondescarta cierta información sobre la disposición de los elementos para una gran parte de las instancias. En cuanto al otro isomorfismo, trivial . niles trivial, pero nil . triviales interesante porque implica que solo hay un f Voidvalor único , algo que vale para una parte considerable de Filterableinstancias. Sucede que hay una MonadPlusversión de esta condición. Si exigimos eso, para cualquier u...

absurd <$> chop u = mzero

... y luego sustituimos la mmapMaybeparte dos, obtenemos:

absurd <$> chop u = mzero
absurd <$> mmapMaybe (const Nothing) u = mzero
mmapMaybe (fmap absurd . const Nothing) u = mzero
mmapMaybe (const Nothing) u = mzero
u >>= maybe mzero return . const Nothing = mzero
u >>= const mzero = mzero
u >> mzero = mzero

Esta propiedad se conoce como la ley de cero a la derecha MonadPlus, aunque hay buenas razones para impugnar su condición de ley de esa clase en particular.