安全型模块算术无注释

Question

有一些Haskell模块化算术模块，实现了类型安全的模块化算术与类型注解。是否可以将一个 可变的 的类型注释中？

例如在 模式 模块化工程如下

let x = 4 :: Mod 7
let y = 5 :: Mod 7
print x + y

有没有什么方法可以实现类似于下面的功能？

let base = 7
let x = 4 :: Mod base
let y = 5 :: Mod base
print x + y

我的问题是 base 不是一个类型。我不知道正确的处理这个问题的方法，还是我对函数式语言的思考方式不对。谢谢。

更新

在实践中基础会是一些我事先不知道的计算结果。

Answer 1

的参数化的一个值。base 是一个多态值。

import Data.Mod
import GHC.TypeNats (Nat)

nine :: KnownNat base => Mod base
nine =
  let x = 4
      y = 5
  in x + y   -- Let type inference do the work of deducing that x, y :: Mod base

要明确地注释这些表达式，使用 ScopedTypeVariables 能够参考 base 类型变量。这也要求 base 要明确量化。

{-# LANGUAGE ScopedTypeVariables #-}
import Data.Mod
import GHC.TypeNats (Nat)

nine :: forall base. KnownNat base => Mod base
nine =
  let x = 4 :: Mod base
      y = 5 :: Mod base
  in x + y

Answer 2

我发现一个类似的问题

我可以有一个未知的KnownNat吗？

在给定的例子中可以应用为

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
module Main where

import GHC.TypeLits
import Data.Proxy
import Data.Mod as M

f x = x + 2

main :: IO ()
main = do
    let y = f 5
    let Just someNat = someNatVal y
    case someNat of
        SomeNat (_ :: Proxy n) -> do
            let x = 4 :: M.Mod n
            let y = 5 :: M.Mod n
            print $ x + y