偶然地,我设法使实例搜索成功,但我不明白为什么。
在下面的代码中,为什么test2
成功但test1
失败(未解决的元和约束(?将 ⦃ isRelation ⦄
参数添加到IsSymmetric2
有何帮助?我认为它一定与解决某些元有关,因此允许实例搜索成功,但除此之外,我很模糊。
有人可以阐明这里工作的机制吗?
这里有一个涉及我的问题的答案("弱点"部分(,但没有解释解决方法的工作原理。我猜当前问题的答案将帮助我更好地理解该解决方法。
{-# 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
类型检查器为 test1
报告的错误和未解决的元数据是:
_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]
有问题的元变量是 _Q_41
,即 Q 参数symmetry1
。从约束[55]
中应该清楚地看出,_Q_41
没有唯一的解决方案(例如,R
和flip R
都是潜在的解决方案(。
当您添加 IsRelation Q
约束时,这将变成 test2
中的IsRelation {_A39 {.x} {.y}} (_Q_41 {.x} {.y})
。通常实例搜索不会触及这样的约束,因为主参数是一个元变量,但在这种情况下,元变量是受约束的(参见 [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