爲什麼基於相關對的過濾器？

在Idris Tutorial中，用於過濾矢量的函數是基於相關對的。爲什麼基於相關對的過濾器？

filter : (a -> Bool) -> Vect n a -> (p ** Vect p a) 
filter f [] = (_ ** []) 
filter f (x :: xs) with (filter f xs) 
    | (_ ** xs') = if (f x) then (_ ** x :: xs') else (_ ** xs')

但是，爲什麼有必要把它放在依賴對而不是更直接的東西上？

filter' : (a -> Bool) -> Vect n a -> Vect p a

在這兩種情況下的p類型必須確定，但我認爲替代上市p兩倍的冗餘消除。

我天真地試圖實施filter'失敗，所以我想知道是否有一個根本的原因，它不能實現？或者可以執行filter'，或許filter僅僅是一個糟糕的例子來展示Idris中的相關對？但是，如果是這種情況，那麼在哪些情況下依賴對是有用的？

謝謝！

來源

2017-08-14 trevor cook

金史貝爾的answer是正確的錢。讓我注意，這是在伊德里斯郵件列表上回在2012年已經討論（!!）：

filter for vector, a question - Idris Programming Language

raichoo貼有什麼可以幫助澄清它，我認爲;您filter'的真正簽名

filter' : {p : Nat} -> {n: Nat} -> {a: Type} -> (a -> Bool) -> Vect a n -> Vect a p

從它應該是顯而易見的，這是不什麼過濾器應該（或者甚至可能）做的; p實際上取決於對謂詞和你正在過濾的向量，你可以（實際上需要）用一個從屬對來表達這個。請注意，在(p ** Vect p a)，p（並因此Vect p a）對中隱含地依賴於在其簽名之前出現的（未命名的）謂詞和向量。

在此擴展，爲什麼依賴對？你想返回一個向量，但是沒有「Vector未知長度」類型;您需要長度爲的值以獲得Vector類型。但是，你可以認爲「好的，我將返回一個Nat連同一個長度的向量」。毫不奇怪，這一對的類型是一個從屬對的例子。更詳細地，從屬對DPair a P是

A型建立了一種類型a
函數P: a -> Type

該類型DPair a P的值是值

的對

x: a
y: P a

在這一點上，我認爲這只是語法可能會誤導你。類型p ** Vect p a是DPair Nat (\p => Vect p a); p沒有過濾器或類似的任何參數。所有這些一開始可能有點混亂;如果是這樣，也許這有助於將p ** Vect p a作爲「長度未知」的「Vector」類型的替代。

來源

2017-08-14 15:39:26

我現在明白爲什麼'filter''不能，謝謝。但我不認爲它已經在這裏（或在郵件列表中）涵蓋了爲什麼原始定義不會與我的選擇相同。也就是說，爲什麼在原始定義中不存在隱含的「{p：Nat}」，允許調用者指定返回長度？我想你在最後一句話中已經談到了，但我不太明白，你能否詳細說明一下？ –

當然，增加了一個更詳細的解釋，爲什麼你需要從屬配對。 –

filter和filter'之間的區別是存在性和普遍量化之間。如果(a -> Bool) -> Vect n a -> Vect p a是filter的正確類型，那將意味着filter返回一個長度爲p的Vector，並且調用者可以指定p應該是什麼。

來源

2017-08-14 14:58:16

很明顯，我們不能爲*任意*類型生成任意*長度的向量。讓我們考慮以下情況：輸入向量是[]，而'a'是無人居住的類型，但這意味着我們不能爲*非零*'p'生成向量，因爲我們必須提供至少一個元素'x'的類型'a'，並且輸入不會*提供給我們。所以，實際上，'filter''不能在這個通用設置中實現。 –

謝謝Kim，但是DPair如何防止這種行爲？ –

一個從屬對就像是說「有ap，這樣......」，但是調用者不能指定p是什麼 –

爲什麼基於相關對的過濾器？

回答

相關問題