haskell - 让 GHC 接受带有 KnownNat 算术的类型签名

Question

我一直在尝试实现 Chinese Remainder Theorem ，对于只有两个方程的特定情况，使用Data.Modular包裹。我的想法是，我可以仅用一个模数指定每个方程(使用数字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)

我收到以下错误:无法推断因使用“toMod”而产生的 (KnownNat (k1 * k2))。但是，GHC 不应该能够对 KnownNat (k1 * k2) 进行算术吗？另外，由于某些奇怪的原因，看起来如果我有一个 Mod 类型的构造函数而不是 toMod 函数，一切都会正常。我也不明白这会产生什么影响......

我正在寻找任何修复程序来帮助编译，包括任何扩展。然而，如果可能的话，我希望不必制作我自己的 Data.Modular 版本。 (我认为直接使用 Mod 构造函数可以让这项工作变得不优雅且笨拙)。

Answer 1

进行此编译的廉价、简单的方法是添加 FlexibleContexts，然后将 KnownNat (k1 * k2) 添加到 crt 的上下文>。一旦我这样做了，我就可以在 ghci 中成功调用它:

> crt (3 :: Mod Integer 5) (5 :: Mod Integer 7)
33

祝您玩得开心，了解如何将 Coprime k1 k2 表达为约束...;-)