Buenos ejemplos de No es Functor / Functor / Aplicativo / Mónada?

Al explicarle a alguien qué es un tipo de clase X, lucho por encontrar buenos ejemplos de estructuras de datos que sean exactamente X.

Entonces, solicito ejemplos para:

• Un constructor de tipos que no es un Functor.
• Un constructor de tipos que es un Functor, pero no Aplicativo.
• Un constructor de tipo que es un aplicativo, pero no es una mónada.
• Un constructor de tipo que es una mónada.

Creo que hay muchos ejemplos de Monad en todas partes, pero un buen ejemplo de Monad con alguna relación con ejemplos anteriores podría completar la imagen.

Busco ejemplos que serían similares entre sí, que difieren solo en aspectos importantes para pertenecer a la clase de tipo particular.

Si uno pudiera obtener un ejemplo de Arrow en algún lugar de esta jerarquía (¿es entre Applicative y Monad?), ¡Eso también sería genial!

Un constructor de tipos que no es un Functor:

newtype T a = T (a -> Int)

Puede hacer un functor contravariante, pero no un functor (covariante). Intenta escribir fmapy fracasarás. Tenga en cuenta que la versión del fundente contravariante se invierte:

fmap      :: Functor f       => (a -> b) -> f a -> f b
contramap :: Contravariant f => (a -> b) -> f b -> f a

Un constructor de tipos que es un functor, pero no Aplicativo:

No tengo un buen ejemplo. Hay Const, pero idealmente me gustaría un no monoide concreto y no puedo pensar en ninguno. Todos los tipos son básicamente numéricos, enumeraciones, productos, sumas o funciones cuando se llega al final. Puede ver a continuación el trabajador porcino y no estoy de acuerdo sobre si Data.Voides un Monoid;

instance Monoid Data.Void where
    mempty = undefined
    mappend _ _ = undefined
    mconcat _ = undefined

Dado que _|_es un valor legal en Haskell, y de hecho es el único valor legal de Data.Voideste, cumple con las reglas de Monoid. No estoy seguro de qué unsafeCoercetiene que ver con esto, porque su programa ya no garantiza que no violará la semántica de Haskell tan pronto como utilice cualquier unsafefunción.

Consulte la Wiki de Haskell para obtener un artículo sobre la parte inferior ( enlace ) o las funciones inseguras ( enlace ).

Me pregunto si es posible crear un constructor de este tipo utilizando un sistema de tipos más rico, como Agda o Haskell con varias extensiones.

Un constructor de tipos que es Aplicativo, pero no Mónada:

newtype T a = T {multidimensional array of a}

Puede hacer un aplicativo con algo como:

mkarray [(+10), (+100), id] <*> mkarray [1, 2]
  == mkarray [[11, 101, 1], [12, 102, 2]]

Pero si lo convierte en una mónada, podría obtener un desajuste de dimensión. Sospecho que ejemplos como este son raros en la práctica.

Un constructor de tipos que es una mónada:

[]

Acerca de las flechas:

Preguntar dónde se encuentra una flecha en esta jerarquía es como preguntar qué tipo de forma es "roja". Tenga en cuenta el tipo de desajuste:

Functor :: * -> *
Applicative :: * -> *
Monad :: * -> *

pero,

Arrow :: * -> * -> *

Mi estilo puede estar limitado por mi teléfono, pero aquí va.

newtype Not x = Kill {kill :: x -> Void}

No puede ser un Functor. Si fuera así, tendríamos

kill (fmap (const ()) (Kill id)) () :: Void

y la luna estaría hecha de queso verde.

mientras tanto

newtype Dead x = Oops {oops :: Void}

es un functor

instance Functor Dead where
  fmap f (Oops corpse) = Oops corpse

pero no puede ser aplicativo, o tendríamos

oops (pure ()) :: Void

y Green estaría hecho de queso Moon (que en realidad puede suceder, pero solo más tarde en la noche).

(Nota adicional: Voidcomo Data.Voides un tipo de datos vacío. Si intenta usarlo undefinedpara demostrar que es un Monoide, lo usaré unsafeCoercepara demostrar que no lo es).

Alegremente

newtype Boo x = Boo {boo :: Bool}

es aplicativo de muchas maneras, por ejemplo, como lo diría Dijkstra,

instance Applicative Boo where
  pure _ = Boo True
  Boo b1 <*> Boo b2 = Boo (b1 == b2)

pero no puede ser una mónada. Para ver por qué no, observe que el retorno debe ser constante Boo Trueo Boo False, y de ahí que

join . return == id

no puede sostenerse.

Oh si, casi me olvido

newtype Thud x = The {only :: ()}

es una mónada Ruede el suyo.

Avión para atrapar ...

Creo que las otras respuestas omitieron algunos ejemplos simples y comunes:

Un constructor de tipos que es un Functor pero no un Aplicativo. Un ejemplo simple es un par:

instance Functor ((,) r) where
    fmap f (x,y) = (x, f y)

Pero no hay forma de definir su Applicativeinstancia sin imponer restricciones adicionales r. En particular, no hay forma de definir pure :: a -> (r, a)un arbitrario r.

Un constructor de tipo que es un aplicativo, pero no es una mónada. Un ejemplo bien conocido es ZipList . (Es una newtypeenvoltura de listas y proporciona una Applicativeinstancia diferente para ellos).

fmapse define de la manera habitual. Pero purey <*>se definen como

pure x                    = ZipList (repeat x)
ZipList fs <*> ZipList xs = ZipList (zipWith id fs xs)

por lo que purecrea una lista infinita repitiendo el valor dado y <*>cremalleras una lista de funciones con una lista de valores - se aplica i función -ésimo al i -ésimo elemento. (El estándar <*>en []produce todas las combinaciones posibles de aplicar la función i - ésima al elemento j -ésimo). Pero no hay una manera sensata de cómo definir una mónada (ver esta publicación ).

¿Cómo encajan las flechas en la jerarquía de fundador / aplicativo / mónada? Ver modismos son ajenos, las flechas son meticulosas, las mónadas son promiscuas por Sam Lindley, Philip Wadler, Jeremy Yallop. MSFP 2008. (Ellos llaman modismos de los ficticios aplicativos ). El resumen:

Revisamos la conexión entre tres nociones de cómputo: las mónadas de Moggi, las flechas de Hughes y las expresiones idiomáticas de McBride y Paterson (también llamadas fundores aplicativos). Mostramos que los modismos son equivalentes a flechas que satisfacen el tipo de isomorfismo A ~> B = 1 ~> (A -> B) y que las mónadas son equivalentes a flechas que satisfacen el tipo de isomorfismo A ~> B = A -> (1 ~ > B). Además, los modismos se integran en flechas y las flechas se integran en mónadas.

Un buen ejemplo para un constructor de tipos que no es un functor es Set: No puede implementar fmap :: (a -> b) -> f a -> f b, porque sin una restricción adicional Ord bno puede construir f b.

Me gustaría proponer un enfoque más sistemático para responder esta pregunta, y también mostrar ejemplos que no usen ningún truco especial como los valores "inferiores" o los tipos de datos infinitos o algo así.

¿Cuándo los constructores de tipos no tienen instancias de clase de tipo?

En general, hay dos razones por las que un constructor de tipos podría no tener una instancia de una clase de tipo determinada:

1. No se pueden implementar las firmas de tipo de los métodos necesarios de la clase de tipo.
2. Puede implementar las firmas de tipo pero no puede cumplir con las leyes requeridas.

Los ejemplos del primer tipo son más fáciles que los del segundo tipo porque para el primer tipo, solo necesitamos verificar si uno puede implementar una función con una firma de tipo dada, mientras que para el segundo tipo, debemos demostrar que no hay implementación posiblemente podría satisfacer las leyes.

Ejemplos específicos

• Un constructor de tipos que no puede tener una instancia de functor porque el tipo no se puede implementar:

  data F z a = F (a -> z)

Este es un contrafunctor, no un functor, con respecto al parámetro tipo a, porque está aen una posición contravariante. Es imposible implementar una función con firma de tipo (a -> b) -> F z a -> F z b.

• Un constructor de tipos que no es un functor legal aunque fmapse pueda implementar la firma de tipo de :

  data Q a = Q(a -> Int, a)
  fmap :: (a -> b) -> Q a -> Q b
  fmap f (Q(g, x)) = Q(\_ -> g x, f x)  -- this fails the functor laws!

El aspecto curioso de este ejemplo es que podemos poner en práctica fmapdel tipo correcto a pesar de que Fno es posible que sea un funtor, ya que utiliza aen una posición contravariante. Por lo tanto, esta implementación que se fmapmuestra arriba es engañosa, a pesar de que tiene la firma de tipo correcta (creo que esta es la única implementación posible de esa firma de tipo), las leyes de functor no están satisfechas. Por ejemplo, fmap id≠ id, porque let (Q(f,_)) = fmap id (Q(read,"123")) in f "456"es 123, pero let (Q(f,_)) = id (Q(read,"123")) in f "456"es 456.

De hecho, Fes solo un profunctor, no es ni un functor ni un contrafunctor.

• Un functor legal que no es aplicativo porque la firma de tipo de pureno se puede implementar: tome la mónada Writer (a, w)y elimine la restricción que wdebería ser un monoide. Entonces es imposible construir un valor de tipo a (a, w)partir de a.

• Un funtor aplicativo que no es porque el tipo de firma <*>no pueden ser implementadas: data F a = Either (Int -> a) (String -> a).

• Un functor que no es legalmente aplicativo a pesar de que se pueden implementar los métodos de clase de tipo:

  data P a = P ((a -> Int) -> Maybe a)

El constructor de tipos Pes un functor porque asolo se usa en posiciones covariantes.

instance Functor P where
   fmap :: (a -> b) -> P a -> P b
   fmap fab (P pa) = P (\q -> fmap fab $ pa (q . fab))

La única implementación posible de la firma de tipo de <*>es una función que siempre devuelve Nothing:

 (<*>) :: P (a -> b) -> P a -> P b
 (P pfab) <*> (P pa) = \_ -> Nothing  -- fails the laws!

Pero esta implementación no satisface la ley de identidad para los actores aplicativos.

• Un functor que es Applicativepero no unMonad porque la firma de tipo de bindno se puede implementar.

¡No conozco ninguno de esos ejemplos!

• Un functor que es Applicativepero noMonad porque las leyes no se pueden cumplir a pesar de que bindse puede implementar la firma de tipo .

Este ejemplo ha generado bastante discusión, por lo que es seguro decir que demostrar que este ejemplo es correcto no es fácil. Pero varias personas han verificado esto independientemente por diferentes métodos. Ver Es `datos PoE a = Vacío | Par aa` una mónada? para discusión adicional.

 data B a = Maybe (a, a)
   deriving Functor

 instance Applicative B where
   pure x = Just (x, x)
   b1 <*> b2 = case (b1, b2) of
     (Just (x1, y1), Just (x2, y2)) -> Just((x1, x2), (y1, y2))
     _ -> Nothing

Es algo engorroso demostrar que no hay una Monadinstancia legal . La razón del comportamiento no monádico es que no hay una forma natural de implementar bindcuándo una función f :: a -> B bpodría regresar Nothingo Justpara diferentes valores de a.

Quizás sea más claro considerarlo Maybe (a, a, a), que tampoco es una mónada, y tratar de implementarlo join. Uno encontrará que no hay una forma intuitiva razonable de implementación join.

 join :: Maybe (Maybe (a, a, a), Maybe (a, a, a), Maybe (a, a, a)) -> Maybe (a, a, a)
 join Nothing = Nothing
 join Just (Nothing, Just (x1,x2,x3), Just (y1,y2,y3)) = ???
 join Just (Just (x1,x2,x3), Nothing, Just (y1,y2,y3)) = ???
 -- etc.

En los casos indicados por ???, parece claro que no podemos producir Just (z1, z2, z3)de manera razonable y simétrica a partir de seis valores diferentes de tipo a. Ciertamente podríamos elegir algún subconjunto arbitrario de estos seis valores, por ejemplo, siempre tomar el primer no vacío Maybe, pero esto no satisfaría las leyes de la mónada. Regresar Nothingtampoco satisfará las leyes.

• Una estructura de datos en forma de árbol que no es una mónada a pesar de que tiene asociatividad bind, pero no cumple con las leyes de identidad.

La mónada usual en forma de árbol (o "un árbol con ramas en forma de functor") se define como

 data Tr f a = Leaf a | Branch (f (Tr f a))

Esta es una mónada gratis sobre el functor f. La forma de los datos es un árbol donde cada punto de ramificación es un "functor-ful" de subárboles. El árbol binario estándar se obtendría con type f a = (a, a).

Si modificamos esta estructura de datos haciendo también las hojas en forma de functor f, obtenemos lo que yo llamo una "semimonada", bindque cumple con las leyes de naturalidad y asociatividad, pero su puremétodo falla una de las leyes de identidad. "Los semimonads son semigrupos en la categoría de endofunctores, ¿cuál es el problema?" Esta es la clase de tipo Bind.

Por simplicidad, defino el joinmétodo en lugar de bind:

 data Trs f a = Leaf (f a) | Branch (f (Trs f a))
 join :: Trs f (Trs f a) -> Trs f a
 join (Leaf ftrs) = Branch ftrs
 join (Branch ftrstrs) = Branch (fmap @f join ftrstrs)

El injerto de rama es estándar, pero el injerto de hoja no es estándar y produce a Branch. Esto no es un problema para la ley de asociatividad, pero rompe una de las leyes de identidad.

¿Cuándo los tipos polinómicos tienen instancias de mónada?

Ninguno de los funtores Maybe (a, a)y Maybe (a, a, a)se puede dar un legítimo Monadejemplo, a pesar de que son obviamente Applicative.

Estos functores no tienen trucos, Voidni en bottomningún lado, ni pereza / rigidez engañosas, ni estructuras infinitas, ni restricciones de clase de tipo. La Applicativeinstancia es completamente estándar. Las funciones returny bindse pueden implementar para estos functores pero no satisfarán las leyes de la mónada. En otras palabras, estos functores no son mónadas porque falta una estructura específica (pero no es fácil entender qué es exactamente lo que falta). Como ejemplo, un pequeño cambio en el functor puede convertirlo en una mónada: data Maybe a = Nothing | Just aes una mónada. Otro functor similar data P12 a = Either a (a, a)es también una mónada.

Construcciones para mónadas polinómicas

En general, aquí hay algunas construcciones que producen Monads legales a partir de tipos polinomiales. En todas estas construcciones, Mes una mónada:

1. type M a = Either c (w, a)donde whay un monoide
2. type M a = m (Either c (w, a))donde mhay alguna mónada y wes cualquier monoide
3. type M a = (m1 a, m2 a)donde m1y m2son mónadas
4. type M a = Either a (m a)¿Dónde mestá alguna mónada?

La primera construcción es WriterT w (Either c), la segunda construcción es WriterT w (EitherT c m). La tercera construcción es un producto de mónadas pure @Mpor componentes : se define como el producto por componentes de pure @m1y pure @m2, y join @Mse define omitiendo datos de productos cruzados (por ejemplo, m1 (m1 a, m2 a)se asigna m1 (m1 a)omitiendo la segunda parte de la tupla):

 join :: (m1 (m1 a, m2 a), m2 (m1 a, m2 a)) -> (m1 a, m2 a)
 join (m1x, m2x) = (join @m1 (fmap fst m1x), join @m2 (fmap snd m2x))

La cuarta construcción se define como

 data M m a = Either a (m a)
 instance Monad m => Monad M m where
    pure x = Left x
    join :: Either (M m a) (m (M m a)) -> M m a
    join (Left mma) = mma
    join (Right me) = Right $ join @m $ fmap @m squash me where
      squash :: M m a -> m a
      squash (Left x) = pure @m x
      squash (Right ma) = ma

He comprobado que las cuatro construcciones producen mónadas legales.

Yo conjeturo que no hay otras construcciones para mónadas polinómicas. Por ejemplo, el functor Maybe (Either (a, a) (a, a, a, a))no se obtiene a través de ninguna de estas construcciones y, por lo tanto, no es monádico. Sin embargo, Either (a, a) (a, a, a)es monádica porque es isomorfo al producto de tres mónadas a, a, y Maybe a. Además, Either (a,a) (a,a,a,a)es monádico porque es isomorfo al producto de ay Either a (a, a, a).

Las cuatro construcciones mostradas arriba nos permitirán obtener cualquier suma de cualquier número de productos de cualquier número de a's, por ejemplo, Either (Either (a, a) (a, a, a, a)) (a, a, a, a, a))etc. Todos los constructores de tipo tendrán (al menos una) Monadinstancia.

Queda por ver, por supuesto, qué casos de uso podrían existir para tales mónadas. Otro problema es que las Monadinstancias derivadas a través de las construcciones 1-4 en general no son únicas. Por ejemplo, al constructor de tipos type F a = Either a (a, a)se le puede dar una Monadinstancia de dos maneras: mediante la construcción 4 con la mónada (a, a)y mediante la construcción 3 con el isomorfismo de tipo Either a (a, a) = (a, Maybe a). Nuevamente, encontrar casos de uso para estas implementaciones no es inmediatamente obvio.

Queda una pregunta: dado un tipo de datos polinómico arbitrario, cómo reconocer si tiene una Monadinstancia. No sé cómo demostrar que no hay otras construcciones para mónadas polinómicas. No creo que exista ninguna teoría hasta ahora para responder a esta pregunta.