如何在Agda中生成替换指定参数返回值的新函数

要实现一个函数replace_f，输入函数f : A → B、参数a : A和值b : B，返回一个新函数——该函数与f行为一致，仅当传入a时返回b。以下是问题分析和正确实现：

你的尝试问题分析 #

1. Lambda模式匹配的变量冲突
   你写的代码：

   replace_f : ∀ {A B} (f : A → B) (a : A) (b : B) → (A → B)
   replace_f f a b = \ { a -> b ; attr -> f attr }
   

   这里lambda中的a是新绑定的局部变量，会匹配任意输入值，导致所有调用都返回b，完全覆盖了原函数f的逻辑，并非你想要的“仅匹配传入的参数a”。

2. 可判定相等性的用法错误
   你尝试的代码：

   replace_f f a b var = if ⌊ Dec (var ≡ a) ⌋ then b else (f var)
   

   报错的原因是Dec是类型构造器，不是函数，无法直接生成Dec (var ≡ a)类型的实例。正确做法是使用对应类型的可判定相等性函数（如_≟_）来生成判定结果。

正确实现方式 #

方法1：基于可判定相等性（通用场景） #

如果类型A支持可判定相等性，可通过with语句匹配判定结果：

open import Relation.Binary.PropositionalEquality using (_≡_)
open import Relation.Nullary
open import Relation.Nullary.Decidable

-- 要求类型A具有可判定相等性
replace_f : ∀ {A B} {{_ : Decidable (_≡_ {A = A})}} (f : A → B) (a : A) (b : B) → A → B
replace_f f a b var with var ≟ a
... | yes _ = b  -- 匹配到var ≡ a，返回b
... | no _  = f var  -- 未匹配，返回原函数结果

解释：

• {{_ : Decidable (_≡_ {A = A})}}是隐式参数，要求类型A提供可判定相等性的实现
• var ≟ a返回Dec (var ≡ a)，即要么yes p（p是var ≡ a的证明），要么no ¬p（¬p是var ≢ a的证明）
• 分支中忽略具体证明（用_），只关注判定结果

方法2：针对具体类型（如自然数） #

如果是处理内置类型（比如ℕ），可直接导入对应类型的_≟_：

open import Data.Nat using (ℕ; _≟_)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Relation.Nullary
open import Relation.Nullary.Decidable

replace_f : ∀ {B} (f : ℕ → B) (a : ℕ) (b : B) → ℕ → B
replace_f f a b var with var ≟ a
... | yes _ = b
... | no _ = f var

方法3：依赖模式匹配（无需可判定相等性） #

如果不想依赖可判定相等性，可通过inspect来获取等式证明：

open import Relation.Binary.PropositionalEquality using (_≡_; refl; inspect)

replace_f : ∀ {A B} (f : A → B) (a : A) (b : B) → A → B
replace_f f a b var with var ≡ a | inspect (_≡_ var) a
... | refl | _ = b
... | _ | _ = f var

这种方式需要调用者在运行时能提供var ≡ a的证明，适合依赖类型编程场景。

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