Skip to content

Instantly share code, notes, and snippets.

@timjb

timjb/GCurry.idr

Last active Oct 26, 2017
Embed
What would you like to do?
Generalized Curry in Idris
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment