如何以变量为参数创建Mod类型？Haskell编译错误求助

问题代码 #

以下是用于搜索最大乘法阶数的部分Haskell实现：

{-# LANGUAGE DataKinds #-}
module Cryptography.WringTwistree.Mix3
  ( mix
  , fiboPair
  , searchDir
  ) where

import Data.Bits
import Data.Word
import qualified Data.Sequence as Seq
import Data.Sequence ((><), (<|), (|>), Seq((:<|)), Seq((:|>)))
import Math.NumberTheory.ArithmeticFunctions
import GHC.TypeLits (Nat)
import Data.Mod
import Math.NumberTheory.Primes

mix :: (Num t,Bits t) => t -> t -> t -> t
mix a b c = xor a mask
  where mask = (a .|. b .|. c) - (a .&. b .&. c)

fibonacci = 0 : 1 : zipWith (+) fibonacci (tail fibonacci)

fiboPair :: Integer -> [Integer]
fiboPair n = take 2 $ dropWhile (<= n) fibonacci

searchDir :: Integer -> (Integer,Int)
-- fst=n/φ rounded to nearest. snd=+1 or -1, indicating search direction.
-- e.g. if n=89, returns (55,1). Search 55,56,54,57,53...
-- if n=144, returns (89,(-1)). Search 89,88,90,87,91...
searchDir n
  | r*2 < den = (q,1)
  | otherwise = (q+1,(-1))
  where [num,den] = fiboPair (2*n)
        (q,r) = (n*num) `divMod` den

isMaxOrder :: Integral a => Nat -> a -> [a] -> a -> Bool
-- isMaxOrder modl car fac n
-- where modl is the modulus, car is its Carmichael function,
-- fac is the set of prime factors of car (without multiplicities),
-- and n is the number being tested.
-- Returns true if n has maximum order, which implies it's a primitive root
-- if modulus has any primitive roots.
isMaxOrder modl car fac n = (modln ^% car) == modl1 && allnot1
  where modln = (fromIntegral n) :: Mod modl
        modl1 = 1 :: Mod modl
        powns = map ((modln ^%) . (car `div`)) fac
        allnot1 = foldl (&&) True (map (/= modl1) powns)

编译错误信息 #

编译时出现以下错误：

/home/phma/src/wring-twistree/src/Cryptography/WringTwistree/Mix3.hs:43:36: error:
    • Could not deduce (GHC.TypeNats.KnownNat m0)
        arising from a use of ‘^%’
      from the context: Integral a
        bound by the type signature for:
                   isMaxOrder :: forall a. Integral a => Nat -> a -> [a] -> a -> Bool
        at /home/phma/src/wring-twistree/src/Cryptography/WringTwistree/Mix3.hs:36:1-56
      The type variable ‘m0’ is ambiguous
    • In the first argument of ‘(==)’, namely ‘(modln ^% car)’
      In the first argument of ‘(&&)’, namely ‘(modln ^% car) == modl1’
      In the expression: (modln ^% car) == modl1 && allnot1
   |
43 | isMaxOrder modl car fac n = (modln ^% car) == modl1 && allnot1
   |                                    ^^

/home/phma/src/wring-twistree/src/Cryptography/WringTwistree/Mix3.hs:44:18: error:
    • Could not deduce (GHC.TypeNats.KnownNat modl1)
        arising from a use of ‘fromIntegral’
      from the context: Integral a
        bound by the type signature for:
                   isMaxOrder :: forall a. Integral a => Nat -> a -> [a] -> a -> Bool
        at /home/phma/src/wring-twistree/src/Cryptography/WringTwistree/Mix3.hs:36:1-56
      Possible fix:
        add (GHC.TypeNats.KnownNat modl1) to the context of
          an expression type signature:
            forall (modl1 :: Nat). Mod modl1
    • In the expression: (fromIntegral n) :: Mod modl
      In an equation for ‘modln’: modln = (fromIntegral n) :: Mod modl
      In an equation for ‘isMaxOrder’:
          isMaxOrder modl car fac n
            = (modln ^% car) == modl1 && allnot1
            where
                modln = (fromIntegral n) :: Mod modl
                modl1 = 1 :: Mod modl
                powns = map ((modln ^%) . (car `div`)) fac
                allnot1 = foldl (&&) True (map (/= modl1) powns)
   |
44 |   where modln = (fromIntegral n) :: Mod modl
   |                  ^^^^^^^^^^^^

/home/phma/src/wring-twistree/src/Cryptography/WringTwistree/Mix3.hs:45:17: error:
    • Could not deduce (GHC.TypeNats.KnownNat modl1)
        arising from a use of ‘1’
      from the context: Integral a
        bound by the type signature for:
                   isMaxOrder :: forall a. Integral a => Nat -> a -> [a] -> a -> Bool
        at /home/phma/src/wring-twistree/src/Cryptography/WringTwistree/Mix3.hs:36:1-56
      Possible fix:
        add (GHC.TypeNats.KnownNat modl1) to the context of
          an expression type signature:
            forall (modl1 :: Nat). Mod modl1
    • In the expression: 1 :: Mod modl
      In an equation for ‘modl1’: modl1 = 1 :: Mod modl
      In an equation for ‘isMaxOrder’:
          isMaxOrder modl car fac n
            = (modln ^% car) == modl1 && allnot1
            where
                modln = (fromIntegral n) :: Mod modl
                modl1 = 1 :: Mod modl
                powns = map ((modln ^%) . (car `div`)) fac
                allnot1 = foldl (&&) True (map (/= modl1) powns)
   |
45 |         modl1 = 1 :: Mod modl
   |                 ^

/home/phma/src/wring-twistree/src/Cryptography/WringTwistree/Mix3.hs:46:29: error:
    • Could not deduce (GHC.TypeNats.KnownNat m1)
        arising from a use of ‘^%’
      from the context: Integral a
        bound by the type signature for:
                   isMaxOrder :: forall a. Integral a => Nat -> a -> [a] -> a -> Bool
        at /home/phma/src/wring-twistree/src/Cryptography/WringTwistree/Mix3.hs:36:1-56
      The type variable ‘m1’ is ambiguous
      Relevant bindings include
        powns :: [Mod m1]
          (bound at /home/phma/src/wring-twistree/src/Cryptography/WringTwistree/Mix3.hs:46:9)
    • In the first argument of ‘(.)’, namely ‘(modln ^%)’
      In the first argument of ‘map’, namely ‘((modln ^%) . (car `div`))’
      In the expression: map ((modln ^%) . (car `div`)) fac
   |
46 |         powns = map ((modln ^%) . (car `div`)) fac
   |                             ^^

问题描述 #

isMaxOrder的参数均为正整数及正整数列表。最初将modl设为a类型，之后尝试改为Nat类型（但直接导入GHC.TypeLits会引发mod冲突）。可以成功编写1 :: Mod 89，但1 :: Mod (fromIntegral 89)会报错，需要解决编译错误。

解决方案 #

错误根源 #

问题核心是混淆了类型级别和值级别的概念：

• Nat是GHC的类型级别自然数，不能作为值参数传递给函数
• Data.Mod的Mod m类型要求m是已知的类型级别Nat（即带有KnownNat m约束），但原代码的类型签名缺少该约束
• 若模数是运行时动态确定的值，无法直接用Mod m，需要通过SomeNat将值级别整数转换为类型级别Nat

方案1：编译时已知模数（类型参数） #

如果模数是编译时固定的，将modl改为类型参数，并添加KnownNat约束：

{-# LANGUAGE DataKinds, ScopedTypeVariables #-}
-- 导入必要模块
import GHC.TypeLits (KnownNat, Nat)
import Data.Mod

-- 修改类型签名，将modl作为类型参数
isMaxOrder :: forall m a. (KnownNat m, Integral a) => a -> [a] -> a -> Bool
isMaxOrder car fac n = (modln ^% car) == modl1 && allnot1
  where
    modln = fromIntegral n :: Mod m
    modl1 = 1 :: Mod m
    -- 简化allnot1的写法
    allnot1 = all (/= modl1) $ map ((modln ^%) . (car `div`)) fac

调用时需指定类型参数，比如：

-- 检查89模数下n是否有最大阶数
isMaxOrder @89 carFac carFactors n

方案2：运行时动态模数（值参数） #

如果模数是运行时动态确定的，使用someNatVal将值级别整数转换为带KnownNat约束的类型级别Nat：

{-# LANGUAGE DataKinds, ScopedTypeVariables #-}
-- 新增导入
import GHC.TypeLits (KnownNat, Nat, SomeNat(..), someNatVal)
import Data.Proxy (Proxy(..))
import Data.Mod

-- 修改类型签名，modl为值参数
isMaxOrder :: Integral a => a -> a -> [a] -> a -> Bool
isMaxOrder modl car fac n = case someNatVal (fromIntegral modl) of
    -- 处理模数<=0的非法情况
    Nothing -> False
    Just (SomeNat (_ :: Proxy m)) -> 
        let modln = fromIntegral n :: Mod m
            modl1 = 1 :: Mod m
            allnot1 = all (/= modl1) $ map ((modln ^%) . (car `div`)) fac
        in (modln ^% car) == modl1 && allnot1

额外注意 #

• 若导入GHC.TypeLits时出现mod名称冲突，可使用限定导入：

  import qualified GHC.TypeLits as TL (Nat, KnownNat, SomeNat(..), someNatVal)
  

  然后用TL.Nat、TL.KnownNat等指代相关类型/函数。

内容的提问来源于stack exchange，提问作者Pierre Abbat