添加實例參數如何幫助實例搜索？

不小心，我設法讓實例搜索成功，但我不明白爲什麼。添加實例參數如何幫助實例搜索？

在下面的代碼中，爲什麼test2成功，但test1失敗（未解決的metas &約束）？ ⦃ isRelation ⦄參數的添加如何幫助IsSymmetric2？我認爲它必須與某些metas得到解決，因此允許實例搜索成功，但除此之外，我很霧。

有人可以闡明這裏的工作機制嗎？

有一個答案here觸及我的問題（「弱點」部分），但沒有解釋如何解決方法的機制工作。我猜測對這個問題的回答將幫助我更好地理解這個解決方法。

{-# OPTIONS --show-implicit #-} 

record IsSymmetric1 {A : Set} (F : A → A → A) (Q : A → A → Set) : Set where 
    field 
    symmetry1 : ∀ {x y} → Q (F x y) (F y x) 

open IsSymmetric1 ⦃ … ⦄ 

record IsRelation {A : Set} (Q : A → A → Set) : Set where 
    no-eta-equality 

record IsSymmetric2 {A : Set} (F : A → A → A) (Q : A → A → Set) ⦃ isRelation : IsRelation Q ⦄ : Set where 
    field 
    symmetry2 : ∀ {x y} → Q (F x y) (F y x) 

open IsSymmetric2 ⦃ … ⦄ 

postulate 
    B : Set 
    G : B → B → B 
    R : B → B → Set 
    instance I-IsSymmetric1 : IsSymmetric1 {B} G R 
    instance I-IsRelation : IsRelation R 
    instance I-IsSymmetric2 : IsSymmetric2 {B} G R 

test1 : ∀ {x y} → R (G x y) (G y x) 
test1 = symmetry1 -- yellow unless {F = G} or {Q = R} is specified 


test2 : ∀ {x y} → R (G x y) (G y x) 
test2 = symmetry2

錯誤和由typechecker爲test1報道未解METAS是：

_A_39 : Set [ at ….agda:29,9-18 ] 
_F_40 : _A_39 {.x} {.y} → _A_39 {.x} {.y} → _A_39 {.x} {.y} [ at ….agda:29,9-18 ] 
_Q_41 : _A_39 {.x} {.y} → _A_39 {.x} {.y} → Set [ at ….agda:29,9-18 ] 
_r_42 : IsSymmetric1 {_A_39 {.x} {.y}} (_F_40 {.x} {.y}) (_Q_41 {.x} {.y}) [ at ….agda:29,9-18 ] 
_x_43 : _A_39 {.x} {.y} [ at ….agda:29,9-18 ] 
_y_44 : _A_39 {.x} {.y} [ at ….agda:29,9-18 ] 
_45 : R (G .x .y) (G .y .x) [ at ….agda:29,9-18 ] 
_46 : R (G .x .y) (G .y .x) [ at ….agda:29,9-18 ] 

———— Errors ———————————————————————————————————————————————— 
Failed to solve the following constraints: 
    Resolve instance argument 
    _42 : 
     {.x .y : B} → 
     IsSymmetric1 {_A_39 {.x} {.y}} (_F_40 {.x} {.y}) (_Q_41 {.x} {.y}) 
    Candidates I-IsSymmetric1 : IsSymmetric1 {B} G R 
    [55] _Q_41 {.x} {.y} 
     (_F_40 {.x} {.y} (_x_43 {.x} {.y}) (_y_44 {.x} {.y})) 
     (_F_40 {.x} {.y} (_y_44 {.x} {.y}) (_x_43 {.x} {.y})) 
     =< R (G .x .y) (G .y .x) 
     : Set 
    _45 := 
    λ {.x} {.y} → 
     IsSymmetric1.symmetry1 (_r_42 {.x} {.y}) {_x_43 {.x} {.y}} 
     {_y_44 {.x} {.y}} 
    [blocked on problem 55]

來源

2017-04-03 m0davis

有問題的metavariable是_Q_41，即q自變量到symmetry1。從約束[55]應該清楚，_Q_41沒有唯一的解決方案（例如，R和flip R都是潛在的解決方案）。

當您添加IsRelation Q約束條件時，將變爲IsRelation {_A39 {.x} {.y}} (_Q_41 {.x} {.y})的test2。通常情況下，實例搜索不會觸及這樣的約束，因爲主要參數是一個元變量，但在這種情況下，元變量是約束（請參閱[1]），因此將繼續實例搜索。唯一可用的實例是IsRelation R，並選擇此解決方案強制_Q_41爲R。

如果您要添加一個實例IsRelation (flip R)的例子將不再經過，因爲例如搜索不能兩個IsRelation實例之間的選擇不知道更多關於_Q_41。

[1] http://agda.readthedocs.io/en/latest/language/instance-arguments.html#instance-resolution

來源

2017-04-04 09:42:51 ulfnorell

添加實例參數如何幫助實例搜索？

回答

相關問題