Impossible de montrer en raison de type ambigu lors de l'utilisation Data.Reflection dans Haskell

Question

Je suis très nouveau à Haskell et j'essaie de créer un type qui représentera toute instance d'Integral sur un module. J'ai trouvé some example code online et je travaille avec cela, donc ma définition de type ressemble à ceci:

data Zn n a = Zn !a !a 

La plupart des choses fonctionnent comme je voudrais; Je peux montrer, ajouter, soustraire, etc.

instance (Integral a, Show a) => Show (Zn n a) where 
    show (Zn n x) = printf "(%s mod %s)" (show (mod x n)) (show n) 

instance (Integral a, Reifies n a) => Num (Zn n a) where 
    Zn n x + Zn _ y = Zn n (mod (x + y) n) 
    Zn n x - Zn _ y = Zn n (mod (x - y) n) 
    Zn n x * Zn _ y = Zn n (mod (x * y) n) 
    negate (Zn n x) = Zn n (n - x) 
    abs = id 
    signum x@(Zn _ 0) = x 
    signum (Zn n _) = Zn n 1 
    fromInteger x = Zn n (mod (fromInteger x) n) 
    where n = reflect (Proxy :: Proxy n) 


znToIntegral :: Integral a => Zn n a -> a 
znToIntegral (Zn n x) = fromIntegral x 

Cependant, je ne peux pas montrer les résultats des opérations arithmétiques sur ces types. Par exemple, dans GHCi:

*Main> let x = Zn 5 3 
*Main> x 
(3 mod 5) 
*Main> let y = Zn 5 7 
(2 mod 5) 
*Main> let z = x + y 
*Main> z 
<interactive>:6:1: 
    No instance for (Integral a0) arising from a use of ‘print’ 
    The type variable ‘a0’ is ambiguous 
    Note: there are several potential instances: 
     instance Integral GHC.Int.Int16 -- Defined in ‘GHC.Int’ 
     instance Integral GHC.Int.Int32 -- Defined in ‘GHC.Int’ 
     instance Integral GHC.Int.Int64 -- Defined in ‘GHC.Int’ 
     ...plus 9 others 
    In a stmt of an interactive GHCi command: print it 

J'ai trouvé cette question a été soulevée dans un certain nombre d'autres moyens que j'ai essayé de mettre en œuvre ces chiffres, et de comprendre comment fonctionne le paquet Data.Reflection me donne quelques problèmes. Je serais également curieux de connaître d'autres implémentations qui semblent plus naturelles aux autres. J'avais initialement essayé de faire quelque chose comme

newtype Zn n a = Zn a 

et allumé parce que je pensais que ce serait simplifier les choses, qu'il n'a pas en particulier. À votre santé!

Answer 1

Dans cet exemple particulier, Zn est un détail d'implémentation interne et ne doit pas être utilisé pour la construction de nombres. Idéalement, Zn ne devrait même pas être exporté d'une bibliothèque. Au lieu de cela, nous sommes supposés construire en utilisant fromInteger et les littéraux numériques.

Le module est introduit dans fromInteger par la réflexion, et nous hébergerons que dans Zn pour éviter une utilisation ultérieure de reflect, pour des raisons de performance (même si je crois reflect n'a pas beaucoup de frais généraux par défaut, donc nous ne pourrions pas gagner beaucoup par ce schéma). Si nous n'utilisons que fromInteger pour créer de nouveaux Zn -s, les modules seront uniformes sur l'ensemble du calcul avec la contrainte Reifies. D'un autre côté, si nous introduisons manuellement le module dans Zn, alors ce morceau de Zn aura toujours ce module, et reify (la façon dont nous fournissons la configuration implicite) ne l'affectera pas du tout. En d'autres termes, cela gâche notre supposé invariant.

Exemple d'utilisation:

foo :: (Integral a, Reifies s a) => Zn s a -> Zn s a -> Zn s a 
foo a b = e where 
    c = 123 
    d = a * b - 3 
    e = negate (d + c) 

showAFooResult = reify 12 (\(Proxy :: Proxy s) -> show (foo 3 4 :: Zn s Int)) 
-- fooResult == "(0 mod 12)" 

A l'intérieur du corps de foo tout aura 12 comme module après nous l'avons installé à l'aide reify.

Si nous louchons un peu, foo est juste une fonction qui attend un argument supplémentaire Integral qu'il utilise en interne comme module. Nous pouvons utiliser reify pour fournir l'argument, en utilisant l'index s dans Proxy.

Si nous ne fournissons aucune valeur pour brancher le trou Reifies, alors nous ne pouvons pas en extraire une valeur. Et bien sûr, nous ne pouvons pas l'imprimer, tout comme nous ne pouvons pas imprimer une fonction.

Nous pouvons imprimer Zn 5 5 parce qu'il a le type Num a => Zn n a, donc nous n'avons aucun trou à remplir.D'autre part, Zn 5 5 + Zn 5 5 a le type (Integral a, Reifies n a) => Zn n a, parce que nous avons spécifié la contrainte Reifies n a dans l'instance Num, et bien sûr l'utilisation de + exige une instance Num. Ici, nous devons utiliser reify (ou une autre fonction d'aide qui l'appelle) pour tirer un résultat.

Answer 2

À titre de comparaison, voici une implémentation qui ne stocke pas le module et utilise toujours reflect:

{-# LANGUAGE FlexibleContexts #-} 
{-# LANGUAGE ScopedTypeVariables #-} 
{-# LANGUAGE RankNTypes #-} 

import Data.Reflection 
import Data.Proxy 
import Text.Printf 

newtype Zn a s = Zn { getZ :: a } 

instance (Integral a, Show a, Reifies s a) => Show (Zn a s) where 
     show x = 
      let 
       p = reflect (Proxy::Proxy s)   
      in 
       printf "(%s mod %s)" (show (mod (getZ x) p)) (show p) 

instance (Integral a, Reifies s a) => Num (Zn a s) where 
     Zn x + Zn y = Zn (mod (x + y) (reflect (Proxy::Proxy s))) 
     Zn x - Zn y = Zn (mod (x - y) (reflect (Proxy::Proxy s))) 
     Zn x * Zn y = Zn (mod (x * y) (reflect (Proxy::Proxy s))) 
     negate (Zn x) = Zn ((reflect (Proxy::Proxy s)) - x) 
     abs = id 
     signum x@(Zn 0) = x 
     signum _ = Zn 1 
     fromInteger x = Zn (mod (fromInteger x) p) 
      where p = reflect (Proxy :: Proxy s) 

Certaines fonctions auxiliaires:

znToIntegral :: Integral a => Zn a s -> a 
znToIntegral (Zn x) = fromIntegral x 

-- Convince the compiler that the phantom type in the proxy 
-- is the same as the one in the Zn 
likeProxy :: Proxy s -> Zn a s -> Zn a s 
likeProxy _ = id 

withZn :: Integral a => a -> (forall s. Reifies s a => Zn a s) -> a 
withZn p z = reify p $ \proxy -> znToIntegral . likeProxy proxy $ z 

Un exemple d'utilisation:

main :: IO() 
main = print $ withZn (7::Int) (Zn 3 + Zn 5) 

withZn fonctionne également à partir de ghci.