2

私は Agda プロジェクトに数週間取り組んできましたが、レベルのポリモーフィズムを可能な限り無視しています。残念なことに (またはおそらく幸いなことに)、私はそれを理解し始める必要があるところまで来ているようです。

これまで、レベル変数は、 の 2 番目の引数Rel(または の 3 番目の引数REL) として必要な場合にのみ使用してきました。Setそれ以外の場合は、直接使用するだけで省略しました。現在、レベルを明示的に数量化し、いくつかのタイプのフォームを既存のコードにa渡そうとするクライアント コードがいくつかあります。Set a以下の例でquibbleは、 はクライアント コードを表し、_[_]×[_]_と≈-Listは、 を使用するだけの既存のコードの典型ですSet。

module Temp where

open import Data.List
open import Data.Product
open import Level
open import Relation.Binary

-- Direct product of binary relations.
_[_]×[_]_ : {ℓ₁ ℓ₂ : Level} {A B C D : Set} → A × B → REL A C ℓ₁ → REL B D ℓ₂ → C × D → Set (ℓ₁ ⊔ ℓ₂)
(a , b) [ _R_ ]×[ _S_ ] (c , d) = a R c × b S d

-- Extend a setoid (A, ≈) to List A.
data ≈-List {ℓ : Level} {A : Set} (_≈_ : Rel A ℓ) : Rel (List A) ℓ where
   [] : ≈-List _≈_ [] []
   _∷_ : {x y : A} {xs ys : List A} → (x≈y : x ≈ y) → (xs≈ys : ≈-List _≈_ xs ys) → ≈-List _≈_ (x ∷ xs) (y ∷ ys)

quibble : {a ℓ : Level} {A : Set a} → Rel A ℓ → Rel (List (A × A)) ℓ
quibble _≈_ = ≈-List (λ x y → x [ _≈_ ]×[ _≈_ ] y)

≈-Listここで、追加の level パラメータを使用しての帰納的定義を拡張してa、 type の型引数を取ることができますSet aが、入力と出力の関係のユニバースがどのように変化するかについては不明です。そして、問題はより複雑な定義にまで波及します。たとえば、_[_]×[_]_どのように進めたらよいかわからない場合などです。

与えられた例の署名を一般化してquibbleコンパイルするにはどうすればよいですか? 私が従うことができる一般的なルールはありますか? 私はこれを読みました。

4

1 に答える 1