Skip to content

Instantly share code, notes, and snippets.

@pelotom

pelotom/curry.idr

Last active August 29, 2015 14:09
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save pelotom/741bf7542bd55a37ecf6 to your computer and use it in GitHub Desktop.
Save pelotom/741bf7542bd55a37ecf6 to your computer and use it in GitHub Desktop.
Download ZIP
A dependent curry and uncurry.
Raw
curry.idr
curry : {A : Type}
-> {B : A -> Type}
-> {C : Sigma A B -> Type}
-> ((p : Sigma A B) -> C p)
-> (x : A) -> (y : B x) -> C (x ** y)
curry f x y = f (x ** y)
-- Dependent uncurry is just the induction principle for sigma types
uncurry : {A : Type}
-> {B : A -> Type}
-> {C : Sigma A B -> Type}
-> ((x : A) -> (y : B x) -> C (x ** y))
-> (p : Sigma A B) -> C p
uncurry f (x ** y) = f x y
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment