Generalized Curry 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