2

引数の型がインデックスの値に依存し、インデックスが明示的に渡される二項演算子のファミリ (たとえば、セットによってインデックス付けされる) を定義するとします。さらに、ファミリーのメンバーを中置記法で使用できるようにしたいとします。

x <[A] y

ここにインデックスがあります。角かっこ [-] は、A を下付き文字として読み取る必要があることを示すと想定されています。x の型は値A に依存し、の定義でA : Setの左側に出現する必要があるため、このような演算にこの構文と互換性のある型シグネチャを与えることは困難です。x : A_<[_]_

syntax宣言に基づいて、次のトリック (ハック?) を試しました。

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}}、syntaxAgda が文句を言います。(不合理ではないかもしれません。)

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をサポートしていないように見えるため、アンビエント B を完全に取得する機能をあきらめずに、 に{{x}}インラインcmp化することはできません。)cmp-explicit

これはハックですか？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し、タイプ チェッカーでは問題ありません。

これは別の（かなり醜くてハックな）アプローチです。私たちが持っているとしましょう：

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

ここで、統一を少し利用することができます: 穴にメンションするものを使用することでA、型チェッカーに暗黙の前?を埋めさせることができます。Aしかし、私の知る限り?、必要な を取得するために の代わりに使用できる単純な型はありませんx <[ A ] y。しかし、考えを終わらせるために、ここで機能することが1つあります。

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実際、標準ライブラリはsyntax1 つの場所でほぼ同じ方法で使用しData.Plusます (正確には):

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

持っcmp-explicitていても重宝します。2 つの追加バージョンを作成することをお勧めします。

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 に答える