Рекурсия по нат-видам

Question

Этот вопрос является продолжением следующего вопроса. Сначала обратитесь к нему: перекрывающиеся экземпляры через Nat-kind

Теперь пришло время сделать пример Group Symmetric, После некоторой дикой математики я подошел к примеру, который работает в принципе, но на самом деле это не так:

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

go функция внутри Semigroup экземпляр должен строить результат, имея рекурсию, хотя Symmetric n, Symmetric (n-1)и так до Symmetric 1, Но GHC не знает, как это сделать, и выдает следующее сообщение об ошибке:

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

Итак, каким будет обходной путь? Возможно ли это для go чтобы иметь возможность вернуть любой экземпляр Symmetric m (m от 1 до n)?

Answer 1

Небольшое изменение go а также f решил проблему:

instance KnownNat n => Semigroup (Symmetric n) where
    x <> y = go x [] 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 x (sIndex y (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

Основная идея заключается в том, чтобы ввести фиктивный параметр. Также обратите внимание, что Cyclic был использован вместо cyclic,

К сожалению, получается, что я немного ошибся в математике. Это должно быть исправлено.

РЕДАКТИРОВАТЬ: Вот исправлено sIndex, который завершает экземпляр:

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

Я также заметил, что x а также y поменялись местами в определении <>, который затем исправляется выше.