¿Son todos los contenedores de tamaño fijo fuertes functores monoidales y / o viceversa?

La Applicativeclase de tipos representa functores monoidales laxos que preservan la estructura monoidal cartesiana en la categoría de funciones escritas.

En otras palabras, dados los testigos de isomorfismos canónicos que (,)forman una estructura monoidal:

-- Implementations left to the motivated reader
assoc_fwd :: ((a, b), c) -> (a, (b, c))
assoc_bwd :: (a, (b, c)) -> ((a, b), c)

lunit_fwd :: ((), a) -> a
lunit_bwd :: a -> ((), a)

runit_fwd :: (a, ()) -> a
runit_bwd :: a -> (a, ())

La clase de tipos y sus leyes se pueden escribir de la misma manera:

class Functor f => Applicative f
  where
  zip :: (f a, f b) -> f (a, b)
  husk :: () -> f ()

-- Laws:

-- assoc_fwd >>> bimap id zip >>> zip
-- =
-- bimap zip id >>> zip >>> fmap assoc_fwd

-- lunit_fwd
-- =
-- bimap husk id >>> zip >>> fmap lunit_fwd

-- runit_fwd
-- =
-- bimap id husk >>> zip >>> fmap runit_fwd

Uno podría preguntarse cómo se vería un functor que es oplax monoidal con respecto a la misma estructura:

class Functor f => OpApplicative f
  where
  unzip :: f (a, b) -> (f a, f b)
  unhusk :: f () -> ()

-- Laws:

-- assoc_bwd <<< bimap id unzip <<< unzip
-- =
-- bimap unzip id <<< unzip <<< fmap assoc_bwd

-- lunit_bwd
-- =
-- bimap unhusk id <<< unzip <<< fmap lunit_bwd

-- runit_bwd
-- =
-- bimap id unhusk <<< unzip <<< fmap runit_bwd

Si pensamos en los tipos involucrados en las definiciones y leyes, se revela la verdad decepcionante; OpApplicativeNo es una restricción más específica que Functor:

instance Functor f => OpApplicative f
  where
  unzip fab = (fst <$> fab, snd <$> fab)
  unhusk = const ()

Sin embargo, aunque cada Applicativefunctor (realmente, cualquiera Functor) es trivial OpApplicative, no necesariamente hay una buena relación entre las Applicativelaxitudes y las OpApplicativeoplaxidades. Entonces podemos buscar functores monoidales fuertes con la estructura monoidal cartesiana:

class (Applicative f, OpApplicative f) => StrongApplicative f

-- Laws:
-- unhusk . husk = id
-- husk . unhusk = id
-- zip . unzip = id
-- unzip . zip = id

La primera ley anterior es trivial, ya que el único habitante del tipo () -> ()es la función de identidad ().

Sin embargo, las tres leyes restantes, y por lo tanto la propia subclase, no son triviales. Específicamente, no todos Applicativeson una instancia legal de esta clase.

Aquí hay algunos Applicativefunctores para los cuales podemos declarar instancias legales de StrongApplicative:

• Identity
• VoidF
• (->) r
• Monoid m => (,) m (ver respuestas)
• Vec (n :: Nat)
• Stream (infinito)

Y aquí hay algunos Applicatives para los que no podemos:

• []
• Either e
• Maybe
• NonEmptyList

El patrón aquí sugiere que la StrongApplicativeclase es en cierto sentido la FixedSizeclase, donde "tamaño fijo" ^* significa que la multiplicidad ^** de habitantes de aun habitante de f aes fija.

Esto se puede expresar como dos conjeturas:

• Cada Applicativerepresentación de un contenedor de "tamaño fijo" de elementos de su argumento tipo es una instancia deStrongApplicative
• No StrongApplicativeexiste ninguna instancia en la que el número de ocurrencias de apueda variar

¿Alguien puede pensar en contraejemplos que refuten estas conjeturas, o en algún razonamiento convincente que demuestre por qué son verdaderos o falsos?

* Me doy cuenta de que no he definido correctamente el adjetivo "tamaño fijo". Lamentablemente, la tarea es un poco circular. No conozco ninguna descripción formal de un contenedor de "tamaño fijo", y estoy tratando de encontrar uno. StrongApplicativeEs mi mejor intento hasta ahora.

Sin embargo, para evaluar si esta es una buena definición, necesito algo para compararla. Dada alguna definición formal / informal de lo que significa para un functor tener un tamaño o multiplicidad dada con respecto a los habitantes de su argumento tipo, la pregunta es si la existencia de una StrongApplicativeinstancia distingue con precisión los functores de tamaño fijo y variable.

Al no tener conocimiento de una definición formal existente, hago un llamamiento a la intuición en mi uso del término "tamaño fijo". Sin embargo, si alguien ya conoce un formalismo existente para el tamaño de un functor y puede compararlo StrongApplicative, mucho mejor.

** Por "multiplicidad" me refiero en un sentido laxo a "cuántos" elementos arbitrarios del tipo de parámetro del functor ocurren en un habitante del tipo de codominio del functor. Esto es sin tener en cuenta el tipo específico al que se aplica el functor y, por lo tanto, sin tener en cuenta los habitantes específicos del tipo de parámetro.

No ser preciso sobre esto ha causado cierta confusión en los comentarios, así que aquí hay algunos ejemplos de lo que consideraría el tamaño / multiplicidad de varios functores:

• VoidF: fijo, 0
• Identity: fijo, 1
• Maybe: variable, mínimo 0, máximo 1
• []: variable, mínimo 0, máximo infinito
• NonEmptyList: variable, mínimo 1, máximo infinito
• Stream: fijo, infinito
• Monoid m => (,) m: fijo, 1
• data Pair a = Pair a a: fijo, 2
• Either x: variable, mínimo 0, máximo 1
• data Strange a = L a | R a: fijo, 1

• Cada Applicativerepresentación de un contenedor de "tamaño fijo" de elementos de su argumento tipo es una instancia deStrongApplicative
• No StrongApplicativeexiste ninguna instancia en la que el número de ocurrencias de apueda variar

¿Alguien puede pensar en contraejemplos que refuten estas conjeturas, o en algún razonamiento convincente que demuestre por qué son verdaderos o falsos?

No estoy seguro de esa primera conjetura, y según las discusiones con @AsadSaeeduddin es probable que sea difícil de probar, pero la segunda conjetura es cierta. Para ver por qué, considere la StrongApplicativeley husk . unhusk == id; es decir, para todos x :: f (), husk (unhusk x) == x. Pero en Haskell, unhusk == const ()para que la ley es equivalente a decir para todos x :: f (), husk () == x. Pero esto a su vez implica que solo puede existir un valor de tipo distinto f (): si hubiera dos valores x, y :: f (), entonces x == husk ()y husk () == y, entonces x == y. Pero si solo hay un f ()valor posible , fdebe ser de forma fija. (por ejemplo data Pair a = Pair a a, para , solo hay un valor de tipo Pair (), este es Pair () (), pero hay múltiples valores de tipo Maybe ()o [()]).husk . unhusk == idimplica que fdebe ser de forma fija.

Podemos responder al menos una de estas preguntas en forma negativa:

Cada aplicativo que representa un contenedor de "tamaño fijo" de elementos de su argumento de tipo es una instancia de StrongApplicative

De hecho, uno de los ejemplos de un legal StrongApplicativeen la pregunta original es incorrecto. El escritor aplicativo Monoid => (,) mno lo es StrongApplicative, porque por ejemplo husk $ unhusk $ ("foo", ()) == ("", ()) /= ("foo", ()).

Del mismo modo, el ejemplo de un contenedor de tamaño fijo:

data Strange a = L a | R a

de multiplicidad fija 1, no es un aplicativo fuerte, porque si definimos husk = Leftentonces husk $ unhusk $ Right () /= Right (), y viceversa. Una forma equivalente de ver esto es que este es solo el aplicativo de escritor para su elección de monoide Bool.

Así que existen solicitantes de "tamaño fijo" que no lo son StrongApplicative. Queda por ver si todos los StrongApplicatives son de tamaño fijo.

Tomemos los functores representables como nuestra definición de "contenedor de tamaño fijo":

class Representable f where
    type Rep f
    tabulate :: (Rep f -> a) -> f a
    index :: f a -> Rep f -> a

El real Representabletiene algunas leyes y superclases, pero a los efectos de esta respuesta, en realidad solo necesitamos dos propiedades:

tabulate . index = id
index . tabulate = id

(De acuerdo, también necesitamos una ley respetuosa instance StrongApplicative ((->) r). Fácil, fácil, ya está de acuerdo en que existe).

Si tomamos esa definición, entonces puedo confirmar esa conjetura 1:

Cada Applicativerepresentación de un contenedor de "tamaño fijo" de elementos de su argumento tipo es una instancia [respetuosa de la ley] deStrongApplicative

es verdad. Así es cómo:

instance Representable f => Applicative f where
    zip (fa, fb) = tabulate (zip (index fa, index fb))
    husk = tabulate . husk

instance Representable f => OpApplicative f where
    unzip fab = let (fa, fb) = unzip (index fab) in (tabulate fa, tabulate fb)
    unhusk = unhusk . index

instance Representable f => StrongApplicative f

Hay muchas leyes que demostrar, pero me centraré solo en los Cuatro Grandes que se StrongApplicativesuman: probablemente ya creas en los que están por delante Applicativey OpApplicative, pero si no lo haces, sus pruebas se parecen a las siguientes ( que a su vez se parecen mucho). Para mayor claridad, voy a utilizar zipf, huskfetc. para la instancia de la función, y zipr, huskr, etc., para la instancia representable, para que pueda realizar un seguimiento de cuál es cuál. (¡Y para que sea fácil verificar que no tomamos lo que estamos tratando de probar como una suposición! Está bien usarlo unhuskf . huskf = idal probar unhuskr . huskr = id, pero sería un error asumirlo unhuskr . huskr = iden esa misma prueba).

La prueba de cada ley procede básicamente de la misma manera: desenrolla las definiciones, descarta el isomorfismo que Representablete da, luego usa la ley análoga para las funciones.

unhuskr . huskr
= { def. of unhuskr and huskr }
(unhuskf . index) . (tabulate . huskf)
= { index . tabulate = id }
unhuskf . huskf
= { unhuskf . huskf = id }
id

huskr . unhuskr
= { def. of huskr and unhuskr }
(tabulate . huskf) . (unhuskf . index)
= { huskf . unhuskf = id }
tabulate . index
= { tabulate . index = id }
id

zipr (unzipr fab)
= { def. of unzipr }
zipr (let (fa, fb) = unzipf (index fab) in (tabulate fa, tabulate fb))
= { def. of zipr }
let (fa, fb) = unzipf (index fab) in tabulate (zipf (index (tabulate fa), index (tabulate fb)))
= { index . tabulate = id }
let (fa, fb) = unzipf (index fab) in tabulate (zipf (fa, fb))
= { def. of (fa, fb) }
tabulate (zipf (unzipf (index fab)))
= { zipf . unzipf = id }
tabulate (index fab)
= { tabulate . index = id }
fab

unzipr (zipr (fa, fb))
= { def. of zipr }
unzipr (tabulate (zipf (index fa, index fb)))
= { def. of unzipr }
let (fa', fb') = unzipf (index (tabulate (zipf (index fa, index fb))))
in (tabulate fa', tabulate fb')
= { index . tabulate = id }
let (fa', fb') = unzipf (zipf (index fa, index fb))
in (tabulate fa', tabulate fb')
= { unzipf . zipf = id }
let (fa', fb') = (index fa, index fb)
in (tabulate fa', tabulate fb')
= { def. of fa' and fb' }
(tabulate (index fa), tabulate (index fb))
= { tabulate . index = id }
(fa, fb)