Is it possible to define Zipp in Idris?

Question

This is a follow-up to this follow-up question. Zipp is a non-recursive, non-pattern-matching implementation of zip using folds. On the untyped lambda calculus, we have:

-- 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)

On Haskell, it is impossible to type this term, as proven by @András_Kovács, but Agda is able to do it, albeit a little complicated. Is it possible to define this program elegantly in Idris?

You can basically replicate the answer you were given in Idris. — gallais

Cactus Cactus · Accepted Answer · 2016-04-12T04:18:57

Here's a straight translation of 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

For simplicity's sake, I defined my own Ex2 and rewriteTy instead of wrestling with the standard library. Ex2 a b P can probably be expressed as DPair (a, b) (uncurry P).

Is it possible to define Zipp in Idris?

1 Answers