Перекрывающиеся экземпляры через Nat-kind - PullRequest
Новая
       64

Перекрывающиеся экземпляры через Nat-kind

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

Эта проблема фактически возникла при попытке реализовать несколько математических групп как типы.

У циклических групп нет проблем (экземпляр Data.Group определен в другом месте): 

newtype Cyclic (n :: Nat) = Cyclic {cIndex :: Integer} deriving (Eq, Ord)

cyclic :: forall n. KnownNat n => Integer -> Cyclic n
cyclic x = Cyclic $ x `mod` toInteger (natVal (Proxy :: Proxy n))

Но симметричные группывозникли проблемы с определением некоторых экземпляров (реализация через систему факторных чисел): 

infixr 6 :.

data Symmetric (n :: Nat) where
    S1 :: Symmetric 1
    (:.) :: (KnownNat n, 2 <= n) => Cyclic n -> Symmetric (n-1) -> Symmetric n

instance {-# OVERLAPPING #-} Enum (Symmetric 1) where
    toEnum _ = S1
    fromEnum S1 = 0

instance (KnownNat n, 2 <= n) => Enum (Symmetric n) where
    toEnum n = let
        (q,r) = divMod n (1 + fromEnum (maxBound :: Symmetric (n-1)))
        in toEnum q :. toEnum r
    fromEnum (x :. y) = fromInteger (cIndex x) * (1 + fromEnum (maxBound `asTypeOf` y)) + fromEnum y

instance {-# OVERLAPPING #-} Bounded (Symmetric 1) where
    minBound = S1
    maxBound = S1

instance (KnownNat n, 2 <= n) => Bounded (Symmetric n) where
    minBound = minBound :. minBound
    maxBound = maxBound :. maxBound

Сообщение об ошибке от ghci (только кратко): 

Overlapping instances for Enum (Symmetric (n - 1))
Overlapping instances for Bounded (Symmetric (n - 1))

Так как GHC может узнать, n-1 равно 1 или нет?Я также хотел бы знать, можно ли написать решение без FlexibleInstances.

1 Ответ

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

Добавьте Bounded (Symmetric (n-1)) и Enum (Symmetric (n-1)) в качестве ограничений, поскольку полное разрешение этих ограничений потребует знания точного значения n. 

instance (KnownNat n, 2 <= n, Bounded (Symmetric (n-1)), Enum (Symmetric (n-1))) =>
  Enum (Symmetric n) where
  ...

instance (KnownNat n, 2 <= n, Bounded (Symmetric (n-1))) =>
  Bounded (Symmetric n) where
  ...

Чтобы избежать FlexibleInstances (что не стоитэто IMO, FlexibleInstances - доброкачественное расширение), используйте числа Пеано data Nat = Z | S Nat вместо примитивного представления GHC.Сначала замените заголовок экземпляра Bounded (Symmetric n) на Bounded (Symmetric (S (S n'))) (это играет роль ограничения 2 <= n), а затем разбейте экземпляр на вспомогательный класс (возможно, больше), чтобы удовлетворить стандартное требование к заголовкам экземпляров.Это может выглядеть так: 

instance Bounded_Symmetric n => Bounded (Symmetric n) where ...
instance Bounded_Symmetric O where ...
instance Bounded_Symmetric n => Bounded_Symmetric (S n) where ...
...