Search code examples
haskellreflectiontypesalgebrareification

Can't show due to ambiguous type while using Data.Reflection in Haskell


I'm very new to Haskell and am trying to create a type that will represent any instance of Integral over some modulus. I found some example code online and am working with that, so my type definition looks like this:

data Zn n a = Zn !a !a

Most things are working as I'd like; I can show, add, subtract, 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

However, I can't show the results of arithmetic operations on these types. For example, in 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

I've found this issue has come up in a number of other ways that I've tried to implement these numbers, and understanding how the Data.Reflection package works is giving me some troubles. I'd also be curious about any other implementations that seem more natural to others. I had originally tried doing something like

newtype Zn n a = Zn a

and switched because I thought that it would simplify things, which it hasn't in particular. Cheers!


Solution

  • In this particular example, Zn is an internal implementation detail and it shouldn't be used for constructing numbers. Ideally, Zn shouldn't be even exported from a library. Instead, we're supposed to construct using fromInteger and numeric literals.

    The modulus is introduced in fromInteger by reflection, and we only store it in Zn to avoid further use of reflect, for performance reasons (although I believe reflect doesn't have much overhead by default, so we might not gain much by this scheme). If we only use fromInteger to create new Zn-s, the moduli will be uniform over the whole computation with the Reifies constraint. On the other hand, if we manually plug in the modulus into Zn, then that piece of Zn will always have that modulus, and reify (the way by which we supply implicit configuration) won't affect it at all. In other words, it messes up our supposed invariant.

    Example use:

    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)"
    

    Inside the body of foo everything will have 12 as modulus after we plugged it in using reify.

    If we squint a bit, foo is just a function that expects an extra Integral argument which it uses internally as modulus. We can use reify to supply the argument, using the the s index in Proxy.

    If we don't supply any value to plug in the Reifies hole, then we can't pull out a value. And of course we can't print it, much like we can't print a function.

    We can print Zn 5 5 because it has type Num a => Zn n a, so we have no hole to fill. On the other hand, Zn 5 5 + Zn 5 5 has type (Integral a, Reifies n a) => Zn n a, because we specified the Reifies n a constraint in the Num instance, and of course the use of + demands a Num instance. Here we must use reify (or some other helper function that calls it) to pull out a result.