Re: Intérêt de refineTH ?

Très bonne question ! Il faut bien comprendre que le compilateur GHC n'a AUCUNE notion de type raffinés. Pour lui, un Integer reste un Integer, i.e. un entier de taille infinie.

La librairie refined propose simplement un type Refined qui, de manière simpliste, peut être vue comme un objet ne contenant qu'un seul membre privé de type Integer. Comme il n'y a pas de conversion implicite en Haskell, un Integer (comme 5) ne peut pas être vu comme un Refined, il faut le convertir.

On ne peut pas obtenir d'erreur à l’exécution : soit on utilise refineTH lors de la compilation (et l'erreur sera le cas échéant à la compilation), soit on utilise refine à l’exécution et on est forcé de tester le résultat de la conversion.

Ce type Refined est très limité, il n'accepte pas d'autres opérations (comme l'addition, la soustraction, ...) Ainsi il ne peut être vraiment pratique que pour des valeurs constante. On peut imaginer trois exemples de fonction division :

• Celle qui ne gère pas l'erreur et qui va planter à l’exécution :

myDiv :: Integer -> Integer -> Integer
myDiv a b = div a b

• Celle qui gère l'erreur et renvoie une valeur représentant la réussite ou l'échec, ce qui force l'appelant de la fonction à gérer le cas sur le résultat:

myDiv :: Integer -> Integer -> Maybe Integer
myDiv _ 0 = Nothing
myDiv a b = Just (div a b)
-- plus tard
case myDiv a b of
 Just res -> putStrLn ("C'est bon: " ++ show res)
 Nothing -> putStrLn "Erreur"

• L'approche qui ne peut pas échouer, mais force l'appelant à fournir le bon type "raffiné" :

myDiv :: Integer -> Refined (Or (LessThan 0) (GreaterThan 0)) Integer -> Integer
myDiv a b = div a b
-- plus tard
case refine b of
 Left erreur -> putStrLn "Erreur"
 Just bRefined -> putStrLn ("C'est bon" ++ show (myDiv a bRefined))

Dans ce dernier cas que je préfère, le type de la fonction est bien plus informatif, et le code de la fonction est plus simple. Et si tu possède déjà un type raffiné, tu peux t'affranchir des tests et ainsi il n'y a pas de coût à l’exécution :

normalizeByTen :: Integer -> Integer
normalizeByTen v = myDiv v $$(refineTH 10)

Qui n'aura pas plus de coût à l’exécution que l'appel à la fonction div.

On pourrait cependant imaginer une libraire d'un peu plus haut niveau capable d'opérations arithmétiques entre les types. C'est le cas par exemple de Liquid Haskell qui est un analyseur statique de code Haskell. Par exemple, il peut prouver que div x (abs x + 1) est correct car :

• quelque que soit x, abs x >= 0
• abs x + 1 >= 1
• div x (abs x + 1) est défini (car point précédant) et différent de 0.

Cet exemple est assez simple et on pourrait facilement réaliser un type Haskell qui permet ces opérations. Cependant des cas plus complexes ne sont pas possible à exprimer dans le système de type et demandent donc un outil externe, comme Liquid Haskell.