实例搜索限制
Instance search limitations
实例参数机制在旧 paper and at the Agda wiki 中有所描述。这些消息来源是否没有提及一些值得注意的事实？实例搜索的限制是什么？
消除歧义
如果我们打字检查：
open import Category.Functor
open import Category.Monad
open RawFunctor
open RawMonad
和运行C-c C-w _<$>_（C-c C-w是"explain why a particular name in scope"），我们得到（经过一些清理）
_<$>_ is in scope as
* a record field Category.Functor.RawFunctor._<$>_
* a record field Category.Monad.RawMonad._._<$>_
即_<$>_ 是不明确的，所以在同一个模块中使用不是 monad 的 monads 和仿函数很麻烦，因为你必须手动消除两个 _<$>_.
之间的歧义
这可以通过实例参数来解决。而不是在 Monad 的定义中打开 Functor（通过 Applicatve）：
record RawIMonad ... where
open RawIApplicative rawIApplicative public
我们可以提供一个实例，让实例搜索来完成工作（Applicative 和 Functor 的定义可以在 here 中找到）：
record Monad {α} (M : Set α -> Set α) : Set (suc α) where
infixl 1 _>>=_
field
return : ∀ {A} -> A -> M A
_>>=_ : ∀ {A B} -> M A -> (A -> M B) -> M B
instance
Monad<:Applicative : Applicative M
Monad<:Applicative = record { pure = return ; _<*>_ = λ mf mx -> mf >>= λ f -> mx >>= return ∘ f }
open Monad {{...}}
现在只有一个 _<$>_ — 在 Functor 的定义中，但是实例搜索发现，monad 是一个 applicative，而 applicative 是一个函子，所以 _<$>_是在 monads 上定义的，因为它是在仿函数上定义的。
实例字段
目前您can't将记录字段声明为实例：
record R : Set where
field
instance n : ℕ
解决方法是
record R : Set where
field
n : ℕ
instance
R->ℕ : ℕ
R->ℕ = n
弱点
实例搜索不配合元变量解析。
instance
fz : Fin 1
fz = zero
z : ∀ {n} {{_ : Fin n}} -> ℕ
z = 0
yellow : z ≡ 0
yellow = refl
ok : z {1} ≡ 0
ok = refl
在 yellow 实例搜索中找不到 fz 实例。我 was told，这是预期的行为，但它对我来说限制太多，我看不到任何好处。
一种解决方法是使用实例参数代替隐式参数：
instance
one : ℕ
one = 1
fz : Fin 1
fz = zero
z : ∀ {{n}} {{_ : Fin n}} -> ℕ
z = 0
now-ok : z ≡ 0
now-ok = refl
Instances are always imported
module M where
instance
z : ℕ
z = 0
z' : {{n : ℕ}} -> ℕ
z' {{n}} = n
ok : z' ≡ 0
ok = refl
M 模块未打开，但实例在范围内。如果你想隐藏实例，使用记录：
record R : Set where
instance
z : ℕ
z = 0
z' : {{n : ℕ}} -> ℕ
z' {{n}} = n
error : z' ≡ 0
error = refl
open R _
ok : z' ≡ 0
ok = refl
A nasty bug
我们可以将ok重写为
ok : let open R _ in z' ≡ 0
ok = refl
但是如果在下面定义ok'
ok' : z' ≡ 0
ok' = refl
来自 R 的实例不在范围内，但 Agda 还是选择了它。价值水平也是如此。 IE。如果您导入一个模块或打开一条记录，无论您在哪里打开它，它的实例都将可用于下面的所有定义。
个人经历
我与实例参数斗争了两周左右，试图 implement Agda 中的一些基本范畴理论，但实例搜索由于其弱点而无法预测——向记录添加参数会破坏一切。也很难理解为什么一切都是黄色的——是因为你在做一些愚蠢的事情还是因为 Agda 拒绝解析一个微不足道的元变量？当你有一个六行的类型签名和几个嵌套记录时，你是否会找到一种方法来克服实例搜索限制，那就是运气问题了。
实例参数机制在旧 paper and at the Agda wiki 中有所描述。这些消息来源是否没有提及一些值得注意的事实？实例搜索的限制是什么？
消除歧义
如果我们打字检查：
open import Category.Functor
open import Category.Monad
open RawFunctor
open RawMonad
和运行C-c C-w _<$>_（C-c C-w是"explain why a particular name in scope"），我们得到（经过一些清理）
_<$>_ is in scope as
* a record field Category.Functor.RawFunctor._<$>_
* a record field Category.Monad.RawMonad._._<$>_
即_<$>_ 是不明确的，所以在同一个模块中使用不是 monad 的 monads 和仿函数很麻烦，因为你必须手动消除两个 _<$>_.
这可以通过实例参数来解决。而不是在 Monad 的定义中打开 Functor（通过 Applicatve）：
record RawIMonad ... where
open RawIApplicative rawIApplicative public
我们可以提供一个实例，让实例搜索来完成工作（Applicative 和 Functor 的定义可以在 here 中找到）：
record Monad {α} (M : Set α -> Set α) : Set (suc α) where
infixl 1 _>>=_
field
return : ∀ {A} -> A -> M A
_>>=_ : ∀ {A B} -> M A -> (A -> M B) -> M B
instance
Monad<:Applicative : Applicative M
Monad<:Applicative = record { pure = return ; _<*>_ = λ mf mx -> mf >>= λ f -> mx >>= return ∘ f }
open Monad {{...}}
现在只有一个 _<$>_ — 在 Functor 的定义中，但是实例搜索发现，monad 是一个 applicative，而 applicative 是一个函子，所以 _<$>_是在 monads 上定义的，因为它是在仿函数上定义的。
实例字段
目前您can't将记录字段声明为实例：
record R : Set where
field
instance n : ℕ
解决方法是
record R : Set where
field
n : ℕ
instance
R->ℕ : ℕ
R->ℕ = n
弱点
实例搜索不配合元变量解析。
instance
fz : Fin 1
fz = zero
z : ∀ {n} {{_ : Fin n}} -> ℕ
z = 0
yellow : z ≡ 0
yellow = refl
ok : z {1} ≡ 0
ok = refl
在 yellow 实例搜索中找不到 fz 实例。我 was told，这是预期的行为，但它对我来说限制太多，我看不到任何好处。
一种解决方法是使用实例参数代替隐式参数：
instance
one : ℕ
one = 1
fz : Fin 1
fz = zero
z : ∀ {{n}} {{_ : Fin n}} -> ℕ
z = 0
now-ok : z ≡ 0
now-ok = refl
Instances are always imported
module M where
instance
z : ℕ
z = 0
z' : {{n : ℕ}} -> ℕ
z' {{n}} = n
ok : z' ≡ 0
ok = refl
M 模块未打开，但实例在范围内。如果你想隐藏实例，使用记录：
record R : Set where
instance
z : ℕ
z = 0
z' : {{n : ℕ}} -> ℕ
z' {{n}} = n
error : z' ≡ 0
error = refl
open R _
ok : z' ≡ 0
ok = refl
A nasty bug
我们可以将ok重写为
ok : let open R _ in z' ≡ 0
ok = refl
但是如果在下面定义ok'
ok' : z' ≡ 0
ok' = refl
来自 R 的实例不在范围内，但 Agda 还是选择了它。价值水平也是如此。 IE。如果您导入一个模块或打开一条记录，无论您在哪里打开它，它的实例都将可用于下面的所有定义。
个人经历
我与实例参数斗争了两周左右，试图 implement Agda 中的一些基本范畴理论，但实例搜索由于其弱点而无法预测——向记录添加参数会破坏一切。也很难理解为什么一切都是黄色的——是因为你在做一些愚蠢的事情还是因为 Agda 拒绝解析一个微不足道的元变量？当你有一个六行的类型签名和几个嵌套记录时，你是否会找到一种方法来克服实例搜索限制，那就是运气问题了。