是否可以在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)。