2

假设您要定义一系列二元运算符（例如，由集合索引），其中参数的类型取决于索引的值，并且索引是显式传递的。此外，假设您希望家庭成员可以使用中缀表示法：

x <[A] y

A 这里是索引；括号 [-] 应该表明 A 应该被读作下标。为与此语法兼容的此类操作提供类型签名很困难，因为 x 的类型取决于值A，因此A : Set必须出现x : A在 的定义的左侧_<[_]_。

我已经根据syntax声明尝试了以下技巧（hack？）：

cmp : (A : Set) → A → A → Set
cmp = {!!}

syntax cmp A x y = x <[ A ] y

postulate C : Set
postulate c : C

x = c <[ C ] c

这似乎有效，除非您的二进制操作使用隐式实例。如果我尝试将表单{{x}}的参数添加到syntax声明中，Agda 会抱怨。（也许不是不合理的。）

似乎可以通过引入一个cmp显式地采用隐式实例的版本来适应这个习惯用法，然后定义一个调用该版本的语法变体：

postulate B : Set

-- Now expects an ambient B.
cmp : (A : Set) {{b : B}} → A → A → Set
cmp = {!!}

-- Version of cmp that makes implicit instance explicit.
cmp-explicit : (A : Set) (b : B) → A → A → Set
cmp-explicit A b = cmp A {{b}}

syntax cmp A x y = x <[ A ] y
syntax cmp-explicit A b x y = x <[ A at b ] y

postulate C : Set
postulate c : C
postulate b : B

x = c <[ C ] c       -- pick up ambient B
y = c <[ C at b ] c  -- pass B explicitly

（由于syntax似乎不支持{{x}}参数，所以不能只内联cmp到cmp-explicit，而不放弃完全拾取环境 B 的能力。）

这是黑客吗？当 y 的类型取决于 x 的值并且 x 被显式传递时，是否还有另一种方法来翻转参数 x 和 y？

自然地，定义

_<′[_]_ = λ x A y → cmp A x y

导致 Agda 在类型检查时抱怨x。

4

1 回答 1

3

您不能以.A : Set之后的方式真正翻转论点x : A。

您已经提到syntax过，我认为这是最好的解决方案。这是可行的，因为 Agda 将转换x <[ A ] y为cmp A x y类型检查器，这很好。

这是另一种（相当丑陋和hacky）的方法。假设我们有：

_<[_]_ : {A : Set} → A → ? → A → Set

在这里我们可以稍微利用一下统一性：通过使用漏洞中提到A的东西?，我们可以强制类型检查器填充A前面的隐式。但据我所知，没有简单的类型可以用来代替?，因此我们可以得到所需的x <[ A ] y。但要完成这个想法，这里有一件事有效：

data Is : Set → Set₁ where
  is : (A : Set) → Is A

_<[_]_ : {A : Set} → A → Is A → A → Set
x <[ is A ] y = cmp A x y

是的，这相当丑陋，我建议不要这样做。

但回到你的问题syntax：我不会syntax以任何方式认为是黑客。事实上，标准库syntax在一个地方使用大致相同的方式（Data.Plus准确地说）：

syntax Plus R x y = x [ R ]⁺ y

即使有cmp-explicit周围也是有用的。我什至会建议您制作两个额外的版本：

cmp-syntax          =         cmp
cmp-explicit-syntax = λ A b → cmp A {{b}}

syntax cmp-syntax          A   x y = x <[ A      ] y
syntax cmp-explicit-syntax A b x y = x <[ A at b ] y

如果您的模块的用户不想使用语法快捷方式（例如，他导入了另一个_<[_]_定义cmp.

同样，标准库使用Σ. 该快捷方式允许您编写：

open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality

x : Σ[ n ∈ ℕ ] n + 2 ≡ 4
x = 2 , refl

如果您不想要它，那么您只需：

open import Data.Product
  hiding (Σ-syntax)
于 2014-01-15T17:20:39.293 回答