是否可以在Idris中定義Zipp？

Question

這是this follow-up question的後續行動。 Zipp是使用摺疊的非遞歸，非模式匹配的zip實現。在無類型演算，我們有：

-- foldr for church encoded lists (that is, folds) 
foldr cons nil list = list cons nil 

zipp_left = foldr (λ x xs cont -> (cont x xs)) (const []) 
zipp_right = foldr (λ y ys x cont -> (cons (pair x y) (cont ys))) (const (const [])) 
zipp  = λ a b -> (zipp_left a) (zipp_right b) 

在Haskell中，它是不能輸入這個詞，它見證了@András_Kovács，但阿格達是能夠做到這一點，雖然有點複雜。可以在Idris中優雅地定義這個程序嗎？

Answer 1

這裏是András's answer直翻譯：

%default total 

foldr : {a : Type} -> (F : List a -> Type) -> 
     (f : {xs : List a} -> (x : a) -> F xs -> F (x :: xs)) -> 
     F [] -> (xs : List a) -> F xs 
foldr F f z [] = z 
foldr F f z (x :: xs) = f x (foldr F f z xs) 

Zip1 : Type -> Type -> Type -> Nat -> Type 
Zip1 A B C Z = C -> List (A, B) 
Zip1 A B C (S n) = (A -> Zip1 A B C n -> List (A, B)) -> List (A, B) 

Zip2 : Type -> Type -> Type -> Nat -> Type 
Zip2 A B C Z = A -> C -> List (A, B) 
Zip2 A B C (S n) = A -> (Zip2 A B C n -> List (A, B)) -> List (A, B) 

data Ex2 : (a : Type) -> (b : Type) -> (p : a -> b -> Type) -> Type where 
    MkEx2 : (x : a) -> (y : b) -> p x y -> Ex2 a b p 

unifyZip : (A : Type) -> (B : Type) -> (n : Nat) -> (m : Nat) -> Ex2 Type Type (\C1 => \C2 => Zip1 A B C1 n = (Zip2 A B C2 m -> List (A, B))) 
unifyZip A B Z  m = MkEx2 (Zip2 A B Void m) Void Refl 
unifyZip A B (S n) Z = MkEx2 Void (Zip1 A B Void n) Refl 
unifyZip A B (S n) (S m) with (unifyZip A B n m) 
    | MkEx2 C1 C2 p = MkEx2 C1 C2 (cong {f = \t => (A -> t -> List (A, B)) -> List (A, B)} p) 

zip1 : (A : Type) -> (B : Type) -> (C : Type) -> (xs : List A) -> Zip1 A B C (length xs) 
zip1 A B C = foldr (Zip1 A B C . length) (\x => \r => \k => k x r) (const []) 

zip2 : (A : Type) -> (B : Type) -> (C : Type) -> (ys : List B) -> Zip2 A B C (length ys) 
zip2 A B C = foldr (Zip2 A B C . length) (\y => \k => \x => \r => (x, y) :: r k) (const . const $ []) 

rewriteTy : a = b -> a -> b 
rewriteTy Refl x = x 

zipp : {A : Type} -> {B : Type} -> List A -> List B -> List (A, B) 
zipp {A} {B} xs ys with (unifyZip A B (length xs) (length ys)) 
    | MkEx2 C1 C2 p with (zip1 A B C1 xs) 
    | zxs with (zip2 A B C2 ys) 
     | zys = rewriteTy p zxs zys 

爲了簡便起見，我定義我自己Ex2和rewriteTy，而不是摔跤的標準庫。 Ex2 a b P大概可以表示爲DPair (a, b) (uncurry P)。