實例搜索限制

Question

實例參數機制在舊的paper和at the Agda wiki中描述。有沒有一些值得注意的事實，這些來源沒有提到？實例搜索有什麼限制？

Answer 1

刪除歧義

如果我們進行類型檢查這一點：

open import Category.Functor 
open import Category.Monad 
open RawFunctor 
open RawMonad 

和運行C-c C-w _<$>_（C-c C-w是 「解釋了爲什麼在範圍上具有特定名稱」），我們得到（一些清潔後）

_<$>_ is in scope as 
    * a record field Category.Functor.RawFunctor._<$>_ 
    * a record field Category.Monad.RawMonad._._<$>_ 

iee _<$>_是不明確的，因此在同一個模塊中使用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是應用程序，應用程序是函子，因此定義了_<$>_在monads上，因爲它是在仿函數上定義的。

實例字段

此刻的你can't申報記錄領域的實例：

record R : Set where 
    field 
    instance n : ℕ 

的解決方法是

record R : Set where 
    field 
    n : ℕ 

    instance 
    R->ℕ : ℕ 
    R->ℕ = n 

弱點

實例搜索不配合與metavariables決議。

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 

但如果從R定義ok'下面

ok' : z' ≡ 0 
ok' = refl 

實例不在範圍內，b無論如何，Agda都會選擇它。價值水平也是如此。即如果您導入模塊或打開記錄，則無論您打開哪個模塊，都可以使用下面的所有定義。

個人經歷

我是用實例論證戰鬥了兩個星期左右的時間，努力implement在阿格達一些基本範疇的理論，但例如搜索是不可預測的，因爲它的弱點 - 添加參數達到創紀錄的廢墟一切。也很難弄清楚爲什麼一切都是黃色的 - 是因爲你在做一些愚蠢的事情，還是因爲Agda拒絕解決一個微不足道的變量？如果您在六行和多個嵌套記錄上有類型簽名，則無論您是否找到解決實例搜索限制的方法，都是一個運氣問題。