实例搜索限制

Question

实例论证机制在旧论文和Agda维基中描述.这些消息来源没有提到一些值得注意的事实吗？实例搜索有哪些限制？

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._._<$>_

即_<$>_不明确,因此在同一模块中使用monad和functor(不是monad)是很麻烦的,因为你必须手动消除两者之间的歧义_<$>_.

这可以通过实例参数来解决.而不是Functor在Monad(via Applicatve)的定义中打开:

record RawIMonad ... where

  open RawIApplicative rawIApplicative public

我们可以提供一个实例,让实例搜索完成工作(这里可以找到Applicative和的定义):Functor

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是一个functor,所以_<$>_在monad上定义,因为它是在functor上定义的.

实例字段

目前您无法将记录字段声明为实例:

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实例.有人告诉我,这是预期的行为,但它对我来说太过限制,我看不出任何好处.

一种解决方法是使用实​​例参数代替隐式参数:

instance
  one : ?
  one = 1

  fz : Fin 1
  fz = zero

  z : ? {{n}} {{_ : Fin n}} -> ?
  z = 0

  now-ok : z ? 0
  now-ok = refl

实例始终是导入的

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

一个讨厌的bug

我们可以重写ok为

ok : let open R _ in z' ? 0
ok = refl

但如果定义ok'如下

ok' : z' ? 0
ok' = refl

来自实例R不在范围内,但无论如何Agda都会选择它.价值水平也是如此.即,如果您导入模块或打开记录,则无论您在何处打开它,下面的所有定义都可以使用它的实例.

个人经验

我正在与实例论证争夺两周左右,试图在Agda中实现一些基本类别理论,但实例搜索由于其弱点而无法预测 - 在记录中添加参数会破坏一切.也很难理解为什么一切都是黄色的 - 是因为你做的事情愚蠢还是因为Agda拒绝解决一个微不足道的元变量？当你有六行和几个嵌套记录的类型签名时,这是一个运气问题,你是否会找到克服实例搜索限制的方法.