haskell - 通过 Nat-kind 重叠实例
问题描述
这个问题实际上是由于尝试将几个数学组实现为类型而出现的。
循环组没有问题(在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
.
解决方案
添加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
是一个良性扩展),请使用 Peano 数字data Nat = Z | S Nat
而不是 GHC 的原始表示。先将instance head替换为Bounded (Symmetric n)
(Bounded (Symmetric (S (S n')))
这起到了约束的作用2 <= n
),然后将instance分解为一个辅助类(可能更多)以满足对instance head的标准要求。它可能看起来像这样:
instance Bounded_Symmetric n => Bounded (Symmetric n) where ...
instance Bounded_Symmetric O where ...
instance Bounded_Symmetric n => Bounded_Symmetric (S n) where ...
推荐阅读
- javascript - 分组条形图d3js中的文本标签错误
- python - 在python中执行.sh文件
- angular - AWS Amplify Cognito TOTP 设置的更短的手动设置代码
- javascript - 如何使用javascript中的动态数组将更多数据添加到csv文件中
- git - Magit:如何在选定的差异大块中禁用突出显示
- excel - 单元格分配导致 For Next 循环不退出
- c - 为什么while循环在这段代码中不起作用?
- kotlin - 如何禁用编辑 EditText 中的部分文本?
- vba - 在vba中执行直到循环
- google-cloud-platform - ssh 到谷歌云计算引擎中新添加的用户时权限被拒绝错误