如何在Morte中輸入zipWith？

這是一個幾乎有效zipWith定義莫提：如何在Morte中輸入zipWith？

zipWith 
    = λ (u : *) 
    -> λ (f : (u -> u -> u)) 
    -> λ (a : (#List u)) 
    -> λ (b : (#List u)) 
    -> λ (List : *) 
    -> λ (cons : (u -> List -> List)) 
    -> λ (nil : List) 
    -> ((λ (A:*) -> λ (B:*) -> 
    (a (B -> List) 
    (λ (h:u) -> λ (t : (B -> List) -> λ k : B -> (k h t))) 
    (λ (k:B) -> nil) 
    (b (u -> A -> List) 
     (λ (h:u) -> λ (t:(u -> A -> List)) -> λ (H:u) -> λ (k:A) -> (cons (f h H) (k t))) 
     (λ (H:u) -> λ (k:A) -> nil))) 
) (fix A . ((u -> A -> List) -> List)) 
    (fix B . (u -> (B -> List) -> List)))

它實際上並沒有分型由於使用的fix，這莫提缺乏。去年有András posted this clever Agda solution without fix。儘管如此，它對Morte的翻譯並不明顯，因爲它也缺乏歸納類型。如何解決這個問題？

編輯：好像我的zipWith與fix不正確。但是，This one似乎檢查。

來源

2016-11-17 MaiaVictor

爲了簡單起見，我將使用常規的Haskell列表。首先，讓我們使用foldr定義zipWith：

zipWith' :: (a -> b -> c) -> [a] -> [b] -> [c] 
zipWith' f xs ys = foldr step (const []) xs ys where 
    step x r [] = [] 
    step x r (y:ys) = f x y : r ys

在這裏，我們摺疊xs，通過ys作爲參數，並在每次迭代拆呢。問題是我們想模仿Church編碼的列表，但它們不能在模式上匹配。然而，有可能在來定義split

split :: [a] -> Maybe (a, [a]) 
split [] = Nothing 
split (x:xs) = Just (x, xs)

的foldr：

czipWith :: (a -> b -> c) -> [a] -> [b] -> [c] 
czipWith f xs ys = foldr step (const []) xs ys where 
    step x r = maybe [] (\(y, ys) -> f x y : r ys) . split

但是同時split遍歷列表懶洋洋地：

split :: [a] -> Maybe (a, [a]) 
split = snd . foldr (\x ~(r, _) -> (x : r, Just (x, r))) ([], Nothing)

現在我們只用正確的褶皺可以定義zipWith （所以split [1..] ≡ Just (1, [2..])），它仍然解構和重建整個列表，因此每個split引入了O（n）開銷，其中n是被分割的列表的長度。由於ys在每次迭代時被分割，所以該算法的總複雜度爲O（n^2）。

所以是的，你可以只使用非遞歸類型鍵入zipWith，但它會是O（n^2）。

此外，除水都依賴paramorphisms和paramorphisms給你做模式匹配，所以如果你有消除器，它的straightforward定義爲O（n）zipWith，它不必像在安德拉什爲複雜'回答你的鏈接。

一些閱讀：

在類型化的設置教會編碼被稱爲Boehm-Berarducci編碼。
How to zip folds。
How to take a TAIL of a functional stream。
split根據foldr的定義，我正在使用的是TAPL中的某處。

來源

2016-11-17 08:21:42 user3237465

的zipWith聰明的定義（來自Launchbury et al.，我相信）不莫提工作，因爲沒有負遞歸類型（其中莫提沒有鍵入它，並暗示fix，在看到我的mentioned以前的答案）需要至少在自然數上進行歸納。 Here's Launcbury定義的一個簡單的Agda版本沒有教會編碼;爲了在Morte中重現這一點，我們需要函數的返回類型取決於自然數（輸入列表的長度）。

沒有歸納法，我們能做的最好的是O(N^2)定義，它在列表上使用O(N)模式匹配，即一個List A -> Maybe (A, List A)函數。它是O(N)，因爲我們只能從最後重建列表的尾部。

在兼容莫特阿格達（獲得莫提，我們需要desugar let樣式定義應用程序和功能定義以註釋lambda表達式）：

Pair : Set → Set → Set 
Pair A B = ∀ P → (A → B → P) → P 

pair : ∀ A B → A → B → Pair A B 
pair A B a b P p = p a b 

List : Set → Set 
List = λ A → ∀ L → (A → L → L) → L → L 

Maybe : Set → Set 
Maybe A = ∀ M → (A → M) → M → M 

just : ∀ A → A → Maybe A 
just A a M j n = j a 

nothing : ∀ A → Maybe A 
nothing A M j n = n 

nil : ∀ A → List A 
nil A L c n = n 

cons : ∀ A → A → List A → List A 
cons A a as L c n = c a (as L c n) 

match : ∀ A → List A → Maybe (Pair A (List A)) 
match A as = 
    as 
    (Maybe (Pair A (List A))) 
    (λ a m M j n → 
     m M 
     (λ p → p M (λ a' as → j (pair A (List A) a (cons A a' as)))) 
     (j (pair A (List A) a (nil A)))) 
    (nothing (Pair A (List A))) 

zipWith : ∀ A B C → (A → B → C) → List A → List B → List C 
zipWith A B C f as = 
    as 
    (List B → List C) 
    (λ a hyp bs → match B bs (List C) 
     (λ p → p (List C) (λ b bs' → cons C (f a b) (hyp bs'))) 
     (nil C)) 
    (λ _ → nil C)

來源

2016-11-17 08:35:03

如何在Morte中輸入zipWith？

回答

相關問題