依存ペアの使用方法

Question

関数があるとします (実際には名前のとおりの動作をします)。

filter : ∀ {A n} → (A → Bool) → Vec A n → ∃ (λ m → Vec A m)

ここで、返した依存ペアを何らかの方法で操作したいと思います。簡単に書きました head 関数：

head :: ∀ {A} → ∃ (λ n → Vec A n) → Maybe A
head (zero   , _ )       = nothing
head (succ _ , (x :: _)) = just x

もちろんこれは完璧に機能します。しかし、私は次のように疑問に思いました。関数が次の場合にのみ呼び出せることを確認する方法はありますか? n ≥ 1?

理想的には機能を作りたいです head : ∀ {A} → ∃ (λ n → Vec A n) → IsTrue (n ≥ succ zero) → A;しかしそれは失敗します。 n で使用する場合は範囲​​外です IsTrue.

御時間ありがとうございます！

---

IsTrue は次のようなものです:

data IsTrue : Bool → Set where
  check : IsTrue true

Answer 1

これはアンカリー化についての質問だと思います。標準ライブラリは、製品の不自然な機能を提供します。 アンカレー。あなたの状況では、ヘッド関数は通常、長さのインデックスを暗黙の引数として取得するため、最初の引数が隠されている場合、不正な機能を持つことがより有益です。次のようなアンカリー関数を書くことができます。

uncurryʰ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : (a : A) → B a → Set c} →
           ({x : A} → (y : B x) → C x y) →
           ((p : Σ A B) → uncurry C p)
uncurryʰ f (x , y) = f {x} y

ベクトルがある場合にベクトルの頭を返す関数は、標準ライブラリに存在しないように見えるので、次のことを書きます。

maybe-head : ∀ {a n} {A : Set a} → Vec A n → Maybe A
maybe-head []       = nothing
maybe-head (x ∷ xs) = just x

これで、あなたの希望する関数は、上記の最初のargplicit-Implicit-uncurrying関数を使用して、おそらく頭の関数をアンカリーすることの問題です。

maybe-filter-head : ∀ {A : Set} {n} → (A → Bool) → Vec A n → Maybe A
maybe-filter-head p = uncurryʰ maybe-head ∘ filter p

結論：依存製品は、非依存バージョンと同様に、喜んでカリー化またはアンカリー化します。

アンカリーはさておき、型シグネチャを使って書きたい関数

head : ∀ {A} → ∃ (λ n → Vec A n) → IsTrue (n ≥ succ zero) → A

次のように記述できます。

head : ∀ {A} → (p : ∃ (λ n → Vec A n)) → IsTrue (proj₁ p ≥ succ zero) → A

Answer 2

おそらく最良の方法は、最初に依存ペアを構造化して、次のように記述することです。

head :: ∀ {A n} → Vec A (S n) → A

ただし、依存ペアを関数シグネチャ内でそのまま保持したい場合は、ペアの最初の要素を検査し、それが正であることを確認する述語 PosN を作成できます。

head :: ∀ {A p} → PosN p -> A

または類似。PosN の定義は演習として読者に任せます。基本的にこれは Vitus の答えがすでに行っていることですが、代わりにより単純な述語を定義できます。

Answer 3

しばらく試した後、最初に欲しかった機能に似た解決策を思いつきました。

data ∃-non-empty (A : Set) : ∃ (λ n → Vec A n) → Set where
  ∃-non-empty-intro : ∀ {n} → {x : Vec A (succ n)} → ∃-non-empty A (succ n , x)

head : ∀ {A} → (e : ∃ (λ n → Vec A n)) → ∃-non-empty A e → A
head (zero   , [])       ()
head (succ _ , (x :: _)) ∃-non-empty-intro = x

誰かがより良い（またはより一般的な）解決策を思いついた場合は、喜んでその答えを受け入れます。コメントも大歓迎です。

---

私が思いついたより一般的な述語は次のとおりです。

data ∃-succ {A : Nat → Set} : ∃ A → Set where
  ∃-succ-intro : ∀ {n} → {x : A (succ n)} → ∃-succ (succ n , x)

-- or equivalently
data ∃-succ {A : Nat → Set} : ∃ (λ n → A n) → Set where
  ...

Answer 4

これはいつもと同じです head のための関数 Vec.

head' : ∀ {α} {A : Set α} → ∃ (λ n → Vec A (suc n)) → A
head' (_ , x ∷ _) = x