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

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

0 голосов
/ 03 января 2019

Этот вопрос является продолжением следующего вопроса. Сначала обратитесь к нему: Перекрывающиеся экземпляры через 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)?

1 Ответ

0 голосов
/ 03 января 2019

Небольшое изменение 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 поменялись местами в определении <>, которое затем исправляется выше.

...