Tous les conteneurs de taille fixe sont-ils des foncteurs monoïdaux solides et / ou vice versa?

La Applicativeclasse de types représente des foncteurs monoïdes laxistes qui préservent la structure monoïde cartésienne sur la catégorie des fonctions typées.

En d'autres termes, étant donné les isomorphismes canoniques témoins qui (,)forment une structure monoïdale:

-- 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 classe de types et ses lois peuvent être écrites de manière équivalente comme ceci:

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

On peut se demander à quoi pourrait ressembler un fonctor monoïde oplax par rapport à la même structure:

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 nous pensons aux types impliqués dans les définitions et les lois, la vérité décevante est révélée; OpApplicativen'est pas une contrainte plus spécifique que Functor:

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

Cependant, alors que chaque Applicativefoncteur (vraiment, n'importe lequel Functor) est trivialement OpApplicative, il n'y a pas nécessairement une bonne relation entre les Applicativelaxités et les OpApplicativeoplaxités. Nous pouvons donc rechercher de solides foncteurs monoïdaux par rapport à la structure monoïde cartésienne:

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

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

La première loi ci-dessus est triviale, car le seul habitant du type () -> ()est la fonction d'identité ().

Cependant, les trois lois restantes, et donc la sous-classe elle-même, ne sont pas triviales. Plus précisément, tous ne sont pas Applicativeune instance légale de cette classe.

Voici quelques Applicativefoncteurs pour lesquels nous pouvons déclarer des instances licites de StrongApplicative:

• Identity
• VoidF
• (->) r
• Monoid m => (,) m (voir les réponses)
• Vec (n :: Nat)
• Stream (infini)

Et voici quelques Applicatives pour lesquels nous ne pouvons pas:

• []
• Either e
• Maybe
• NonEmptyList

Le schéma suggère ici que la StrongApplicativeclasse est en quelque sorte la FixedSizeclasse, où "taille fixe" ^* signifie que la multiplicité ^** d'habitants d' aun habitant de f aest fixe.

Cela peut être défini comme deux conjectures:

• Chaque Applicativereprésentant un conteneur "de taille fixe" d'éléments de son argument type est une instance deStrongApplicative
• Aucun cas de StrongApplicativeexiste dans lequel le nombre d'occurrences de apeut varier

Quelqu'un peut-il penser à des contre-exemples qui réfutent ces conjectures, ou à un raisonnement convaincant qui démontre pourquoi elles sont vraies ou fausses?

* Je me rends compte que je n'ai pas correctement défini l'adjectif "taille fixe". Malheureusement, la tâche est un peu circulaire. Je ne connais aucune description formelle d'un conteneur de "taille fixe" et j'essaie d'en trouver un. StrongApplicativeest ma meilleure tentative jusqu'à présent.

Cependant, afin d'évaluer si c'est une bonne définition, j'ai besoin de quelque chose à comparer. Étant donné une définition formelle / informelle de ce que signifie pour un foncteur d'avoir une taille ou une multiplicité donnée par rapport aux habitants de son argument de type, la question est de savoir si l'existence d'une StrongApplicativeinstance distingue précisément les foncteurs de taille fixe et variable.

Ne connaissant pas une définition formelle existante, je fais appel à l'intuition dans mon utilisation du terme «taille fixe». Cependant, si quelqu'un connaît déjà un formalisme existant pour la taille d'un foncteur et peut le comparer StrongApplicative, tant mieux.

** Par "multiplicité", je me réfère au sens large à "combien" d'éléments arbitraires du type de paramètre du foncteur se produisent chez un habitant du type codomaine du foncteur. Ceci est sans égard au type spécifique auquel le foncteur est appliqué, et donc sans égard aux habitants spécifiques du type de paramètre.

Ne pas être précis à ce sujet a provoqué une certaine confusion dans les commentaires, voici donc quelques exemples de ce que je considérerais comme la taille / multiplicité de divers foncteurs:

• VoidF: fixe, 0
• Identity: fixe, 1
• Maybe: variable, minimum 0, maximum 1
• []: variable, minimum 0, maximum infini
• NonEmptyList: variable, minimum 1, maximum infini
• Stream: fixe, infini
• Monoid m => (,) m: fixe, 1
• data Pair a = Pair a a: fixe, 2
• Either x: variable, minimum 0, maximum 1
• data Strange a = L a | R a: fixe, 1

• Chaque Applicativereprésentant un conteneur "de taille fixe" d'éléments de son argument type est une instance deStrongApplicative
• Aucun cas de StrongApplicativeexiste dans lequel le nombre d'occurrences de apeut varier

Quelqu'un peut-il penser à des contre-exemples qui réfutent ces conjectures, ou à un raisonnement convaincant qui démontre pourquoi elles sont vraies ou fausses?

Je ne suis pas sûr de cette première conjecture, et d'après les discussions avec @AsadSaeeduddin, il sera probablement difficile à prouver, mais la deuxième conjecture est vraie. Pour voir pourquoi, considérez la StrongApplicativeloi husk . unhusk == id; qui est, pour tous x :: f (), husk (unhusk x) == x. Mais dans Haskell, unhusk == const (), de sorte que la loi équivaut à dire pour tous x :: f (), husk () == x. Mais cela implique à son tour qu'il ne peut exister qu'une seule valeur distincte de type f (): s'il y avait deux valeurs x, y :: f (), alors x == husk ()et husk () == y, alors x == y. Mais s'il n'y a qu'une seule f ()valeur possible , alors elle fdoit être de forme fixe. (par exemple pour data Pair a = Pair a a, il n'y a qu'une seule valeur de type Pair (), ceci étant Pair () (), mais il y a plusieurs valeurs de type Maybe ()ou [()].) Ainsihusk . unhusk == idimplique qu'il fdoit être de forme fixe.

Nous pouvons répondre à au moins une de ces questions par la négative:

Chaque Applicatif représentant un conteneur "de taille fixe" d'éléments de son argument type est une instance de StrongApplicative

En fait, l'un des exemples de licite StrongApplicativedans la question initiale est erroné. L'écrivain Monoid => (,) mn'est pas applicatif StrongApplicative, car par exemple husk $ unhusk $ ("foo", ()) == ("", ()) /= ("foo", ()).

De même, l'exemple d'un conteneur de taille fixe:

data Strange a = L a | R a

de multiplicité fixe 1, n'est pas un fort applicatif, car si l'on définit husk = Leftalors husk $ unhusk $ Right () /= Right (), et vice versa. Une façon équivalente de voir cela est que ce n'est que le rédacteur applicatif pour votre choix de monoïde Bool.

Il existe donc des applications "à taille fixe" qui ne le sont pas StrongApplicative. StrongApplicativeReste à savoir si tous les s sont de taille fixe.

Prenons les foncteurs représentables comme notre définition de "conteneur de taille fixe":

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

Le réel Representablea quelques lois et superclasses, mais pour les besoins de cette réponse, nous avons en fait besoin de seulement deux propriétés:

tabulate . index = id
index . tabulate = id

(D'accord, nous avons également besoin d'un respectueux des lois instance StrongApplicative ((->) r). Easy peasy, vous êtes déjà d'accord pour dire qu'il existe.)

Si nous prenons cette définition, je peux confirmer cette conjecture 1:

Chaque Applicativereprésentant un conteneur "de taille fixe" d'éléments de son argument type est une instance [respectueuse de la loi] deStrongApplicative

est vrai. Voici comment:

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

Il y a beaucoup de lois à prouver, mais je me concentrerai uniquement sur les quatre grands qui StrongApplicativeajoutent - vous croyez probablement déjà les premières pour Applicativeet OpApplicative, mais si vous ne le faites pas, leurs preuves ressemblent à celles ci-dessous ( qui à leur tour se ressemblent beaucoup). Pour plus de clarté, je vais utiliser zipf, huskfetc. pour l'instance de fonction, et zipr, huskretc. pour l'instance représentable, de sorte que vous pouvez garder une trace de ce qui est qui. (Et pour qu'il soit facile de vérifier que nous ne prenons pas la chose que nous essayons de prouver comme une hypothèse! C'est correct de l'utiliser unhuskf . huskf = idpour prouver unhuskr . huskr = id, mais ce serait une erreur de supposer unhuskr . huskr = iddans cette même preuve.)

La preuve de chaque loi procède essentiellement de la même manière: déroulez les définitions, supprimez l'isomorphisme qui Representablevous donne, puis utilisez la loi analogue pour les fonctions.

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)