1

This question is a sequel to the following question. Refer to it first: Overlapping instances via Nat-kind

Now it's time to make the instance of Group Symmetric. After some savage math, I've come up to an instance that works in principle, but actually doesn't:

sIndex :: forall n. KnownNat n => Symmetric n -> Integer -> Integer
sIndex xs m = sIndex_ xs (m `mod` n)
  where
    n = toInteger (natVal (Proxy :: Proxy n))
    sIndex_ :: Symmetric m -> Integer -> Integer
    sIndex_ S1 _ = 0
    sIndex_ (x :. _) 0 = cIndex x
    sIndex_ (x :. xs) m = let
        i = cIndex x + sIndex_ xs (m-1)
        in if i < n then i else i - n

instance KnownNat n => Semigroup (Symmetric n) where
    x <> y = go [] n where
        n = toInteger (natVal (Proxy :: Proxy n))
        go :: forall m. [(Integer,Integer)] -> Integer -> Symmetric m
        go j m
            | 0 == m = S1
            | otherwise = let
                i = sIndex y (sIndex x (n-m))
                ix = foldr f i j
                in cyclic ix :. go ((ix,m) :j) (m-1)
        f (j,m) i = (i - j) `mod` m - 1

The go function inside the Semigroup instance should build the result by having recursion though Symmetric n, Symmetric (n-1), and so on until Symmetric 1. But GHC doesn't know how to do it and outputs the following error message:

Group_Symmetric.hs:89:24: error:
    • Couldn't match type ‘m’ with ‘1’
      ‘m’ is a rigid type variable bound by
        the type signature for:
          go :: forall (m :: Nat).
                [(Integer, Integer)] -> Integer -> Symmetric m
        at Group_Symmetric.hs:87:9-69
      Expected type: Symmetric m
        Actual type: Symmetric 1

So what would the workaround be? Is it possible for go to be able to return any instantation of Symmetric m (m from 1 to n)?

Dannyu NDos
  • 2,458
  • 13
  • 32

1 Answers1

1

A slight change of go and f solved the problem:

instance KnownNat n => Semigroup (Symmetric n) where
    x <> y = go y [] n where
        n = toInteger (natVal (Proxy :: Proxy n))
        go :: forall m. Symmetric m -> [(Integer,Integer)] -> Integer -> Symmetric m
        go S1 _ _ = S1
        go (_ :. xs) j m = let
            i = sIndex y (sIndex x (n-m))
            ix = foldr f i j
            in Cyclic ix :. go xs ((ix,m) :j) (m-1)
        f (j,m) i = let
            ix = (i - j) `mod` m - 1
            in if 0 <= ix then ix else ix + m

The key idea is to introduce a dummy parameter. Also note that Cyclic was used instead of cyclic.

Unfortunately, it turns out that I did some math wrong. It is to be corrected.

EDIT: Here is the corrected sIndex, which completes the instance:

sIndex :: forall n. KnownNat n => Symmetric n -> Integer -> Integer
sIndex xs m = let
    n = toInteger (natVal (Proxy :: Proxy n))
    in sIndex_ xs (m `mod` n) n
  where
    sIndex_ :: Symmetric m -> Integer -> Integer -> Integer
    sIndex_ S1 _ _ = 0
    sIndex_ (x :. _) 0 _ = cIndex x
    sIndex_ (x :. xs) m n = let
        i = cIndex x + sIndex_ xs (m-1) (n-1) + 1
        in if n <= i then i - n else i
Dannyu NDos
  • 2,458
  • 13
  • 32