是否可以在 Idris 中定义 Zipp？

Question

这是this follow-up question 的后续行动。 Zipp 是使用折叠的非递归、非模式匹配的 zip 实现。在无类型 lambda 演算中，我们有：

-- 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 所证明的那样，但 Agda 能够做到，尽管有点复杂。是否可以在 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)。