如何在Agda中为外部函数定义返回值范围？

你遇到的问题很典型：外部导入的IO函数（比如这里的randomRIO）是黑盒，Agda没法直接知晓它的返回值满足什么性质，所以没法直接在类型里表达a ≤ 结果 ≤ b。不过我们可以通过包装外部函数+运行时验证+类型见证的方式来实现这个约束，下面是具体的方案：

1. 定义带范围约束的依赖类型 #

首先我们需要一个类型来明确表示“在[a,b]范围内的整数”，用依赖类型可以精准描述这个约束：

open import Agda.Builtin.Int
open import Prelude

data Between (a b : Int) : Set where
  mkBetween : (x : Int) → (a ≤ x) → (x ≤ b) → Between a b

这里Between a b类型的元素必须是一个整数x，同时携带两个证明：x大于等于a，且小于等于b，Agda的类型系统会确保这两个证明必须成立，才能构造出该类型的值。

2. 包装外部函数并添加验证逻辑 #

接下来我们要写一个包装函数，调用外部的randomRIO之后，对返回值做运行时检查，确认它在范围内后，生成带证明的Between a b类型值；如果不符合范围，可以选择抛出错误或者重试：

先保留你原代码中的postulate，再补充必要的辅助定义和包装函数：

postulate
  randomRIO : Int → Int → IO Int
  fail : String → IO {A : Set} A  -- 处理验证失败的辅助函数

{-# FOREIGN GHC import qualified System.Random as Random #-}
{-# FOREIGN GHC import Control.Monad (fail) #-}
{-# COMPILE GHC randomRIO = \a b -> Random.randomRIO (a, b) #-}
{-# COMPILE GHC fail = fail #-}

-- 辅助：整数比较的运行时检查和证明生成
postulate
  intLeq : Int → Int → Bool
  proveLeq : (x y : Int) → {auto : True (intLeq x y)} → x ≤ y

{-# FOREIGN GHC intLeq = (<=) #-}
{-# COMPILE GHC proveLeq = \x y -> Refl #-}

-- 带类型约束的包装函数
randomRIOBetween : (a b : Int) → IO (Between a b)
randomRIOBetween a b = do
  x ← randomRIO a b
  if intLeq a x ∧ intLeq x b then
    pure (mkBetween x (proveLeq a x) (proveLeq x b))
  else
    fail $ "randomRIO returned " ++ show x ++ " which is not between " ++ show a ++ " and " ++ show b

这个方案的核心逻辑是：

• 先调用外部的randomRIO获取随机数
• 用intLeq做运行时的范围检查
• 如果检查通过，用proveLeq生成Agda类型系统认可的证明（因为运行时已经确认了a ≤ x和x ≤ b，所以proveLeq可以安全返回Refl）
• 如果检查失败，用fail抛出错误（你也可以改成递归重试逻辑，直到得到符合范围的数）

3. 使用包装后的约束函数 #

现在你可以在main里使用randomRIOBetween，它的返回值类型明确保证了结果在[a,b]范围内：

main : IO Unit
main = do
  num ← randomRIOBetween 1 10
  case num of λ where
    (mkBetween x _ _) → putStrLn $ show x

通过模式匹配取出实际的整数x时，Agda的类型系统已经确保x一定满足1 ≤ x ≤ 10。

补充：跳过运行时检查的简化方案 #

如果你完全信任GHC的randomRIO实现（确定它一定会返回[a,b]之间的数），也可以直接postulate一个带约束的版本，跳过运行时验证，但这种方式相当于手动担保外部函数的正确性，风险更高：

postulate
  randomRIOBetween : (a b : Int) → IO (Between a b)

{-# COMPILE GHC randomRIOBetween = \a b -> mkBetween <$> Random.randomRIO (a,b) <*> pure Refl <*> pure Refl #-}

一旦外部函数的行为不符合预期（比如GHC的randomRIO出现bug），Agda的类型系统无法捕捉这类错误，所以更推荐第一种带验证的方案。

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