4

私が関数を持っていると仮定します (それは実際に名前が言うことを行います):

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
4

4 に答える 4

3

これは uncurring に関する質問だと思います。標準ライブラリは、製品の uncurry 関数を提供します。 uncurryを参照してください。あなたの状況では、ヘッド関数は通常長さのインデックスを暗黙の引数として取るため、最初の引数が隠されている uncurry 関数を使用する方が有益です。そのような uncurry 関数を書くことができます:

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

これで、目的の関数は、上記で定義した最初の引数の暗黙的な非カリー化関数を使用して、多分ヘッド関数をアンカリー化するだけの問題です。

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
于 2012-03-14T10:14:45.370 に答える
1

しばらく遊んだ後、最初に欲しかった機能に似たソリューションを思いつきました。

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
  ...
于 2012-03-09T18:34:34.633 に答える
1

最良の方法は、おそらく最初に従属ペアを分解して、次のように書くことです。

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

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

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

または類似。PosN の定義は読者の課題として残しておきます。基本的に、これは Vitus の回答が既に行っていることですが、代わりに、より単純な述語を定義できます。

于 2012-03-09T21:31:01.620 に答える
0

これは の通常のhead機能とまったく同じですVec。

head' : ∀ {α} {A : Set α} → ∃ (λ n → Vec A (suc n)) → A
head' (_ , x ∷ _) = x
于 2014-07-09T19:17:16.740 に答える