我一直在尝试使用Chinese Remainder Theorem包针对两个方程的特定情况实现Data.Modular。我的想法是,我只能用一个模数(使用数字x = a (mod m)
的a (mod m)
)指定每个方程。这是我的实现。
{-# LANGUAGE DataKinds, ScopedTypeVariables, TypeOperators #-}
import GHC.TypeLits
import Data.Proxy (Proxy (..))
import Data.Modular
crt :: forall k1 k2 i. (KnownNat k1, KnownNat k2, Integral i) => i `Mod` k1 -> i `Mod` k2 -> i `Mod` (k1 * k2)
crt a1 a2 = toMod $ (unMod a1)*n2*(unMod n2') + (unMod a2)*n1*(unMod n1')
where n1 = getModulus a1 :: i
n2 = getModulus a2 :: i
n2' = inv $ (toMod n2 :: i `Mod` k1)
n1' = inv $ (toMod n1 :: i `Mod` k2)
getModulus :: forall n i j. (Integral i, Integral j, KnownNat n) => i `Mod` n -> j
getModulus x = fromInteger $ natVal (Proxy :: Proxy n)
我收到以下错误:
Could not deduce (KnownNat (k1 * k2)) arising from a use of ‘toMod’
。但是,GHC不能对KnownNat (k1 * k2)
进行算术运算吗?另外,出于某些奇怪的原因,如果我有一个Mod
类型的构造函数而不是toMod
函数,则一切正常。我也看不出那应该有什么不同...我正在寻找任何有助于此编译的修复程序,包括任何扩展名。但是,如果可能的话,我不想创建自己的Data.Modular版本。 (我认为我可以通过直接使用
Mod
构造函数来巧妙而笨拙地完成这项工作)。 最佳答案
进行此编译的便宜而俗气的方法是添加FlexibleContexts
,然后将KnownNat (k1 * k2)
添加到crt
的上下文中。一旦完成此操作,就可以在ghci中成功调用它:
> crt (3 :: Mod Integer 5) (5 :: Mod Integer 7)
33
玩弄如何将
Coprime k1 k2
表示为约束... ;-)关于haskell - 使用KnownNat算法使GHC接受类型签名,我们在Stack Overflow上找到一个类似的问题:https://stackoverflow.com/questions/30613542/