Vérifier l'implémentation d'un monoïde (Haskell, Idris2)

Voir aussi : video youtube - code source

Dans l’article précédent, on a vu que Haskell permet d’implémenter des semigroupes et des monoïdes en instanciant les classes de type Semigroup et Monoid, mais que c’est au développeur de s’assurer que son implémentation respecte bien les lois correspondantes (associativité, neutralité à gauche et à droite).

Dans cet article, on va voir qu’avec Haskell et Idris, on peut vérifier automatiquement, et même prouver, que les lois sont respectées. Pour cela, on utilisera un exemple très simple : le monoïde des booléens pour l’opérateur conjonction.

En Haskell

Haskell permet de vérifier que les lois des semigroupes/monoïdes sont vérifiées, pour des valeurs données ou générées aléatoirement.

Implémentation du monoïde

On peut implémenter notre exemple avec le wrapper de type suivant (cette implémentation existe déjà dans la bibliothèque standard) :

newtype All = All Bool
  deriving (Eq, Show)

L’opérateur ne doit retourner “vrai” que si les deux termes sont “vrai”. L’élément neutre est la valeur “vrai” :

instance Semigroup All where
  All True <> y = y
  _ <> _ = All False

instance Monoid All where
  mempty = All True

Tests de propriétés

Pour vérifier qu’un type respecte les lois des semigroupes (associativité) et des monoïdes (identité par la gauche et par la droite), on peut implémenter des tests de propriétés correspondants :

semigroupAssoc :: (Eq m, Monoid m) => m -> m -> m -> Bool
semigroupAssoc a b c = (a <> (b <> c)) == ((a <> b) <> c)

monoidLeftId :: (Eq m, Monoid m) => m -> Bool
monoidLeftId a = (mempty <> a) == a

monoidRightId :: (Eq m, Monoid m) => m -> Bool
monoidRightId a = (a <> mempty) == a

Pour tester ces propriétés sur notre type All, il ne reste qu’à instancier la classe de type Arbitrary (pour pouvoir générer des valeurs automatiquement), et lancer les vérifications dans la fonction principale :

instance Arbitrary All where
  arbitrary = All <$> arbitrary

main :: IO ()
main = do
  quickCheck (semigroupAssoc :: All -> All -> All -> Bool)
  quickCheck (monoidLeftId :: All -> Bool)
  quickCheck (monoidRightId :: All -> Bool)

Il faut ensuite exécuter le code pour effectuer les vérifications :

$ runghc all1.hs

+++ OK, passed 100 tests.
+++ OK, passed 100 tests.
+++ OK, passed 100 tests.

Si les lois n’étaient pas respectées dans l’implémentation, on aurait une erreur à l’exécution des tests de propriétés. Par exemple, si on écrit _ <> y = y au lieu de _ <> y = All False, des tests de monoidRightId vont échouer à l’eécution :

$ runghc all1.hs 

+++ OK, passed 100 tests.
+++ OK, passed 100 tests.
*** Failed! Falsified (after 3 tests):  
All False

A noter qu’on aurait pu se contenter ici de tests unitaires, étant donné que le type All n’a qu’un petit nombre de valeurs possibles.

Tests de propriétés prédéfinis

La bibliothèque checkers implémente des tests de propriétés classiques, dont ceux pour les lois des semigroupes et des monoïdes.

Ainsi pour notre monoïde d’exemple, si on a écrit le type et les instances de Semigroup et de Monoid, on peut vérifier les lois en instanciant Arbitrary et EqProp, et en lançant le test monoid :

instance Arbitrary All where
  arbitrary = All <$> arbitrary

instance EqProp All where 
  (=-=) = eq

main :: IO ()
main = quickBatch (monoid $ All True)

A l’exécution, les propriétés des monoïdes sont vérifiées, ainsi que les propriétés des semigroupes (puisque qu’un monoïde doit aussi être un semigroupe) :

$ runghc all2.hs 

monoid:
  left  identity: +++ OK, passed 500 tests.
  right identity: +++ OK, passed 500 tests.
  associativity:  +++ OK, passed 500 tests.
  mappend = (<>): +++ OK, passed 500 tests.
  mconcat:        +++ OK, passed 500 tests.

En Idris2

Les tests de propriétés apportent déjà un certain niveau de confiance dans l’implémentation de notre monoïde, mais cela reste des vérifications a posteriori, sur des valeurs ponctuelles. Idris permet d’apporter un niveau de confiance supplémentaire, via l’écrire de preuves.

Implémentation du monoïde

L’implémentation de notre type All en Idris est très proche de l’implémentation en Haskell :

data All = MkAll Bool

Semigroup All where
  MkAll True <+> y = y
  _ <+> y = MkAll False

Monoid All where
  neutral = MkAll True

Par rapport à Haskell, on notera qu’on doit utiliser un nom différent pour la valeur (MkAll) que pour le type (All), qu’on n’a pas besoin du mot-clé instance et que le nom de l’opérateur (<+>) et de l’élément neutre (neutral) sont différents.

Preuves

Idris utilise les types dépendants, c’est-à-dire qu’on peut manipuler des valeurs au niveau du type lui-même. Ceci permet de définir des propriétés et d’implémenter des preuves validées par le compilateur lui-même (voir la correspondance de Curry-Howard).

Par exemple, on peut écrire une propriété allIsAssociative dont le type décrit que le type All respecte l’associativité :

allIsAssociative : (x, y, z : All) -> x <+> (y <+> z) = (x <+> y) <+> z

On peut alors écrire la preuve dans l’implémentation de allIsAssociative :

allIsAssociative (MkAll True)  _ _ = Refl
allIsAssociative (MkAll False)  _ _ = Refl

De même, on peut écrire des preuves pour les lois des monoïdes :

allIsNeutralL : (x : All) -> x <+> MkAll True = x
allIsNeutralL (MkAll False) = Refl
allIsNeutralL (MkAll True) = Refl

allIsNeutralR : (x : All) -> MkAll True <+> x = x
allIsNeutralR (MkAll False) = Refl
allIsNeutralR (MkAll True) = Refl

Ce code n’a pas vocation à être exécuté mais uniquement à être compilé. En effet, le compilateur vérifiera que les types sont cohérents, et donc que la démonstration est correcte.

Par exemple, si on écrit _ <+> y = y au lieu de _ <+> y = MkAll False, le compilateur va détecter un problème de type et donc que la preuve allIsNeutralL n’est pas valide :

$ idris2 all1.idr
...
Error: While processing right hand side of allIsNeutralL. When unifying:
    MkAll False = MkAll False
and:
    MkAll False <+> MkAll True = MkAll False
Mismatch between: False and True.

all1:21:31--21:35
 17 | allIsAssociative (MkAll True)  _ _ = Refl
 18 | allIsAssociative (MkAll False)  _ _ = Refl
 19 | 
 20 | allIsNeutralL : (x : All) -> x <+> MkAll True = x
 21 | allIsNeutralL (MkAll False) = Refl

Preuves prédéfinies

Le module Control.Algebra du package contrib implémente déjà les lois des semigroupes/monoïdes (voir Idris2Doc). Pour cela, il suffit d’instancier les interfaces SemigroupV et MonoidV, en y écrivant nos preuves :

SemigroupV All where
  semigroupOpIsAssociative (MkAll True) _ _ = Refl
  semigroupOpIsAssociative (MkAll False) _ _ = Refl

MonoidV All where
  monoidNeutralIsNeutralL (MkAll True) = Refl
  monoidNeutralIsNeutralL (MkAll False) = Refl

  monoidNeutralIsNeutralR (MkAll True) = Refl
  monoidNeutralIsNeutralR (MkAll False) = Refl

Conclusion

Certaines structures algébriques comme les semigroupes/monoïdes sont définies mathématiquement mais peuvent être intéressantes à utiliser pour programmer. Haskell et Idris en proposent des implémentations via les classes de types Semigroup/Monoid et les utilisent couramment dans leurs bibliothèques.

Cependant, certaines propriétés doivent être vérifiées, ce qu’on peut faire facilement avec les tests de propriétés (Haskell, Idris) ou, plus rigoureusement, avec des preuves (Idris).