N-Ary zip functions in Idris

GCurry.idr

module GCurry

import Data.HVect

GCurry : (ts : Vect n Type) -> (HVect ts -> Type) -> Type
GCurry [] T = T []
GCurry (t :: ts) T = (v : t) -> GCurry ts (T . (v ::))

gCurry :  {ts : Vect n Type}
       -> {T : HVect ts -> Type}
       -> ((vs : HVect ts) -> T vs)
       -> GCurry ts T
gCurry {ts=[]}          f = f []
gCurry {ts=t::ts} {T=T} f = \v => gCurry {ts=ts} {T = T . (v ::)} (\vs => f (v :: vs))

gUncurry :  {ts : Vect n Type}
         -> {T : HVect ts -> Type}
         -> GCurry ts T
         -> (vs : HVect ts)
         -> T vs
gUncurry {ts=[]}          f []        = f
gUncurry {ts=t::ts} {T=T} f (x :: xs) = gUncurry {ts=ts} {T = T . (x ::)} (f x) xs

ZipWithGeneric.idr

module ZipWithGeneric

import GCurry
import Data.HVect

zipWith : (f : a -> b -> c) -> List a -> List b -> List c
zipWith f []      _       = []
zipWith f _       []      = []
zipWith f (a::as) (b::bs) = f a b :: zipWith f as bs

zipWithUncurried :  {ts : Vect n Type}
                 -> (f : HVect ts -> r)
                 -> HVect (map List ts)
                 -> List r
zipWithUncurried {ts=[]}    f []      = [f []]
zipWithUncurried {ts=t::[]} f (l::[]) = map (f . (::[])) l
zipWithUncurried {ts=t::ts} f (l::ls) = zipWith ($) (zipWithUncurried (\vs => \v => f (v :: vs)) ls) l

zipWithN :  {ts : Vect n Type}
         -> (f : GCurry ts (const x))
         -> GCurry (map List ts) (const (List x))
zipWithN {n=n} {ts=ts} {x=x} f = gCurry {ts=map List ts} {T = const (List x)}
                                        (zipWithUncurried (gUncurry {ts=ts} {T=const x} f))

zipWith3 :  (f : a -> b -> c -> x)
         -> List a -> List b -> List c -> List x
zipWith3 {a} {b} {c} = zipWithN {ts=[a,b,c]}

zipWith4 :  (f : a -> b -> c -> d -> x)
         -> List a -> List b -> List c -> List d -> List x
zipWith4 {a} {b} {c} {d} = zipWithN {ts=[a,b,c,d]}

zipWith5 :  (f : a -> b -> c -> d -> e -> x)
         -> List a -> List b -> List c -> List d -> List e -> List x
zipWith5 {a} {b} {c} {d} {e} = zipWithN {ts=[a,b,c,d,e]}

zipWith6 :  (f : a -> b -> c -> d -> e -> f' -> x)
         -> List a -> List b -> List c -> List d -> List e -> List f' -> List x
zipWith6 {a} {b} {c} {d} {e} {f'} = zipWithN {ts=[a,b,c,d,e,f']}

zipWith7 :  (f : a -> b -> c -> d -> e -> f' -> g -> x)
         -> List a -> List b -> List c -> List d -> List e -> List f' -> List g -> List x
zipWith7 {a} {b} {c} {d} {e} {f'} {g} = zipWithN {ts=[a,b,c,d,e,f',g]}