Auto implicit 没有解决，即使它应该是封闭条件下的直接函数应用

Question

我有以下 Agda 代码：

open import Data.Maybe
open import Data.Product

data Addressing : Set where
  PC++ SP++ SP-- : Addressing

combine : Maybe Addressing → Maybe Addressing → Maybe Addressing
combine nothing y = y
combine (just x) nothing = just x
combine (just PC++) (just PC++) = just PC++
combine (just SP++) (just SP++) = just SP++
combine (just SP--) (just SP--) = just SP--
combine (just _) (just _) = nothing

record Ends : Set where
  constructor _⇝_
  field
    before : Maybe Addressing
    after : Maybe Addressing
open Ends

Compatible : Ends → Maybe Ends → Set
Compatible this that = Is-just (combine (after this) (that >>= before))

open import Data.Maybe.Relation.Unary.Any

append : (this : Ends) → (that : Maybe Ends) → Compatible this that → Ends
append ends nothing _ = ends
append (start ⇝ _) (just (_ ⇝ end)) _ = start ⇝ end

data Transfer : Set where
  Load Store : Transfer

data Microcode (Step : Ends → Set) : Maybe Ends → Set where
  [] : Microcode Step nothing
  _∷_ : ∀ {this rest} → Step this → Microcode Step rest → {auto match : Compatible this rest} → Microcode Step (just (append this rest match))

infixr 20 _∷_

如您所见，combine 是一个带有两个数据类型参数的总函数。如果 this 和 rest 是封闭条款，我希望 auto match : Compatible this rest 很容易解决。

然而，当我尝试这样使用它时：

data Step : Ends → Set where
  Load : (addr : Addressing) → Step (just addr ⇝ nothing)
  Store : (addr : Addressing) → Step (nothing ⇝ just addr)
  ALU : Step (nothing ⇝ nothing)

microcode : Microcode Step (just (just PC++ ⇝ just SP++))
microcode = Load PC++ ∷ Store SP++ ∷ []

然后我在每个缺点步骤都得到未解决的元数据：

_auto_56 : Compatible (nothing ⇝ just SP++) nothing
_match_57 : Compatible (nothing ⇝ just SP++) nothing 
_auto_58 : Compatible (just PC++ ⇝ nothing) (just (nothing ⇝ just SP++))
_match_59 : Compatible (just PC++ ⇝ nothing) (just (nothing ⇝ just SP++))

这是怎么回事？如果我把例如一个洞里的第一个，求值，它的正常形式是：

Any (λ _ → Agda.Builtin.Unit.⊤) (just SP++)

这对我来说表明 Agda 能够计算它，那么为什么不使用它来解决那些 auto 隐式？

Answer 1

Agda 没有 auto 关键字。 {auto match : Compatible this rest} 引入了两个参数，称为 auto 和 match。

对于所需的行为，一种解决方案是仅使用隐式参数和谓词计算 ⊤ 或 ⊥。如果谓词计算为 ⊤，则根据 eta 法则推断其见证为 tt。

Compatible : Ends → Maybe Ends → Set
Compatible this that = T (is-just (combine (after this) (that >>= before)))

_∷_ : ... {match : Compatible this rest} ...

另一个更接近 Idris auto 的解决方案是实例参数：

data Is-just' {A : Set} : Maybe A → Set where
  instance is-just' : ∀ {x} → Is-just' (just x)

Compatible this that = Is-just' (combine (after this) (that >>= before))

_∷_ : ... {{match : Compatible this rest}} ...

Auto implicit 没有解决，即使它应该是封闭条件下的直接函数应用

Auto implicit not solved, even though it should be straightforward function application on closed terms

implicit

unification

reduction

agda