Re: Solution à base de types variants en ADA

J'ai pas trop de souci avec la verbosité d'ADA (Que je découvre en lisant ton code). Je suis plus embêté par le concept de devoir fournir un cas par défaut pour un type comme tu le laisse supposer en commentaire. Cela veut dire qu'ADA, si tu n'initialise pas explicitement ta valeur, va prendre le choix par défaut ? Je n'aime pas ;)

On a droit également à une exception si on tente d'accéder ou de modifier un champ alors que le discriminant n'est pas le bon :

MaPolitique := (Politique => CasParticulier);
MaPolitique.NombreThread := 5;—CONSTRAINT_ERROR : discriminant check failed

Il n'y a pas de garantie statique sur ce genre de chose ? Ça c'est dommage.

Les range, c'est sympa que le langage propose cela de façon native, mais au final cela s'émule assez bien dans n'importe quel autre langage avec un peu de typage dépendant.

Par exemple, en Haskell :

{-# LANGUAGE KindSignatures, DataKinds, TypeApplications, ScopedTypeVariables #-}
import GHC.TypeLits
import Control.Exception (assert)
import Data.Proxy
newtype Range (a :: Nat) (b :: Nat) = RangeVal Integer deriving (Show)
newValInRange :: forall a b. (KnownNat a, KnownNat b) => Integer -> Range a b
newValInRange i = assert (i >= bMin && i <= bMax) (RangeVal i)
 where bMin = natVal @a Proxy
 bMax = natVal @b Proxy

C'est assez verbeux et incompréhensible pour l’œil non habitué, donc en gros, si on passe les import et LANGUAGE nécessaires. On a une définition de type Range, paramétrée par deux types "phantoms", bMin et bMax qui représentent les borne du range, mais ces valeurs sont stockées au niveau du type. Cependant la valeur stockée ne peut pas être contrainte, donc on stock un Integer dedans.

Tous le problème se résume maintenant à empêcher la création d'un Range sans passer par une procédure de vérification. Pour cela on n'exportera pas le constructeur RangeVal, à la place, on va exporter la fonction newValInRange. Son type est assez barbare, newValInRange :: forall a b. (KnownNat a, KnownNat b) => Integer -> Range a b, mais en gros elle prend un Integer et renvoie un Range a b. Le truc c'est que on va se servir du a et b attendus (au niveau du type) pour déduire la vérification au niveau valeur.

La ligne assert (i >= bMin && i <= bMax) (RangeVal i) se contente de renvoyer notre Integer bien encapsulé dans un RangeVal, mais après avoir testé qu'il est bien dans les bornes, en se servant de bMin = natVal @a Proxy pour transformer le type a, Integer au niveau du type, vers la valeur bMin, integer au niveau valeur.

Après cela s'utilise comme cela. Imaginons la fonction suivante qui accepte un Range 0 10 :

launchMissile :: Range 0 10 -> IO ()
launchMissile r = case getValInRange r of
 0 -> putStrLn "Paix et harmonie"
 n -> putStrLn (unwords (replicate (fromInteger n) "EXTERMINATE!"))

qui se sert entre autre de la fonction utilitaire getValInRange (RangeVal i) = i qui permet d'extraire l'Integer du range.

Alors, nous obtenons :

*Main GHC.TypeLits> launchMissile (newValInRange 0)
Paix et harmonie
*Main GHC.TypeLits> launchMissile (newValInRange 10)
EXTERMINATE! EXTERMINATE! EXTERMINATE! EXTERMINATE! EXTERMINATE! EXTERMINATE! EXTERMINATE! EXTERMINATE! EXTERMINATE! EXTERMINATE!
*Main GHC.TypeLits> launchMissile (newValInRange 11)
*** Exception: Assertion failed
CallStack (from HasCallStack):
 assert, called at range.hs:9:19 in main:Main

On note que l’inférence de type fait son boulot et déduit tout seul que le résultat de newValInRange doit être un Range 0 10.

Mais bon, c'est une usine à gaz de typage dépendant pour au final avoir une erreur au runtime, donc c'est assez inutile, on pourrait remplacer la même chose par un bête check dans la fonction launchMissile.

Ce qui est par contre intéressant c'est quand on peut faire tout ce processus à la compilation. Par exemple, une fonction launchMissile qui connait son nombre de missile à la compilation et peut faire des vérifications statiques dessus :

launchMissile' :: forall (n :: Nat). (KnownNat n, 0 <= n, n <= 10) => IO ()
launchMissile' = case natVal @n Proxy of
 0 -> putStrLn "Paix et harmonie"
 n -> putStrLn (unwords (replicate (fromInteger n) "EXTERMINATE!"))

(Cette solution demande les extensions TypeOperators, ConstraintKinds, TypeFamilies, AllowAmbiguousTypes, rien que ça, et aussi le package typelits-witnesses et l'import de 'GHC.TypeLits.CompareetData.Type.Bool.) IcilaunchMissile'est une fonction qui est paramétrée parnà la compilation, donc c'est à la compilation que l'erreur surn` pétera.

Bon, çà c'est vachement plus simple en C++, qui gère super bien le typage dépendant sur les entiers et vivent les constexpr :

template<int n>
void launchMissile2()
{
 static_assert(n >= 0 && n <= 10, "WTF!");
 if(n == 0)
 std::cout << "Paix et harmonie\n" << std::endl;
 else
 for(auto i = 0u; i < n; ++i)
 {
 std::cout << "EXTERMINATE!\n";
 }
}
constexpr int fact(const int n)
{
 int res = 1;
 for(int i = 1; i <= n; i++)
 {
 res *= i;
 }
 return res;
}
int main()
{
 launchMissile2<fact(3)>(); // lance 3! == 6 missiles
}

(Bon, le c++ c'est bon des fois, constexpr déchire très souvent, jusqu'à ce que tu veuilles créer des valeurs plus poussées au niveau du type. ;)

Aller, dodo.