通过Nat-kind重叠实例

问题描述

这个问题实际上是由于尝试将几个数学组实现为类型而引起的.

This problem actually emerged from attempt to implement few mathematical groups as types.

循环组没有问题(在其他地方定义的Data.Group实例):

Cyclic groups have no problem (instance of Data.Group defined elsewhere):

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

但是对称组在定义某些实例时存在一些问题(通过阶乘数系统实现):

But symmetric groups have some problem on defining some instances (implementation via factorial number system):

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的错误消息(仅简短地):

Error message from ghci (only briefly):

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

那么GHC如何知道n-1是否等于1?我还想知道是否可以在不使用FlexibleInstances的情况下编写解决方案.

So how can GHC know whether n-1 equals to 1 or not? I'd also like to know whether the solution can be written without FlexibleInstances.

推荐答案

添加Bounded (Symmetric (n-1))和Enum (Symmetric (n-1))作为约束，因为要完全解决这些约束将需要知道n的确切值.

Add Bounded (Symmetric (n-1)) and Enum (Symmetric (n-1)) as constraints, because fully resolving those constraints would require knowing the exact value of 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是一个良性扩展)，请使用Peano数字data Nat = Z | S Nat代替GHC的原始表示形式.首先用Bounded (Symmetric (S (S n')))替换实例头Bounded (Symmetric n)(这扮演约束2 <= n的角色)，然后使用辅助类(可能更多)分解实例，以满足实例头的标准要求.可能看起来像这样:

---

To avoid FlexibleInstances (which is not worth it IMO, FlexibleInstances is a benign extension), use Peano numbers data Nat = Z | S Nat instead of GHC's primitive representation. First replace the instance head Bounded (Symmetric n) with Bounded (Symmetric (S (S n'))) (this plays the role of the constraint 2 <= n), and then break up the instance with an auxiliary class (possibly more) to satisfy the standard requirement on instance heads. It might look like this:

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

这篇关于通过Nat-kind重叠实例的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！