我如何使用依賴於對

假設有一個函數（它確實什麼名字說）：我如何使用依賴於對

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;但是失敗了，因爲當我在IsTrue中使用它時，n超出了範圍。

謝謝你的時間！

IsTrue是一樣的東西：

data IsTrue : Bool → Set where 
    check : IsTrue true

來源

2012-03-08 Vitus

我覺得這是一個關於uncurrying問題。標準庫爲產品提供了不安全的函數，請參閱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

現在你需要的功能僅僅是一個上面定義與第一參數隱-uncurrying 功能uncurrying的也許頭功能的物質：

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

結論：相關產品喜歡咖喱和uncurry像他們的非依賴版本。

Uncurrying一旁，你想用的類型簽名

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-14 10:14:45 danr

很好，雖然我認爲你的意思是IsTrue（proj 1 p≥succ zero）'。 – Vitus 2012-03-14 15:59:43

謝謝，編輯！ – danr 2012-03-14 16:01:43

與它玩了一段時間後，我想出瞭解決方案，類似於我最想要的功能：

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-09 18:34:34 Vitus

最好的辦法可能是先解構依賴對，這樣就可以只寫：

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

然而，如果你真的想保持函數簽名中的從屬對完整，你可以編寫一個謂詞PosN來檢查對的第一個元素並檢查它是肯定的：

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

或相似。我將PosN的定義作爲練習給讀者。基本上這就是Vitus的答案已經做到的，但是可以定義一個更簡單的謂詞。

來源

2012-03-09 21:31:01

這就像平時head功能Vec。

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

來源

2014-07-09 19:17:16 user3237465

我如何使用依賴於對

回答

相關問題