haskell - 类型安全的模块化算术无注释

Question

有许多 Haskell 模块化算术模块可以使用类型注释实现类型安全的模块化算术。是否可以在类型注释中传入一个变量？

例如，在 mod 模块中，以下工作

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 不是类型。我不确定解决这个问题的正确方法，或者我是否以错误的方式考虑函数式语言。谢谢。

更新

在实践中，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