Initial version

1 files changed, 51 insertions, 0 deletions

diff --git a/src/Data/Fun/Nary.idr b/src/Data/Fun/Nary.idr
new file mode 100644
index 0000000..21a684b
--- /dev/null
+++ b/src/Data/Fun/Nary.idr
@@ -0,0 +1,51 @@
+module Data.Fun.Nary
+
+import Data.Vect
+
+%default total
+
+public export
+data Visibility = Visible | Hidden | Auto
+
+public export
+Pi : Visibility -> (a : Type) -> (a -> Type) -> Type
+Pi Visible a b = (x : a) -> b x
+Pi Hidden  a b = {x : a} -> b x
+Pi Auto    a b = {auto x : a} -> b x
+
+public export
+lam : (vis : Visibility) -> (0 b : a -> Type) ->
+      ((x : a) -> b x) -> Pi vis a b
+lam Visible b f = f
+lam Hidden  b f = f _
+lam Auto    b f = f %search
+
+public export
+app : (vis : Visibility) -> (0 b : a -> Type) ->
+      Pi vis a b -> ((x : a) -> b x)
+app Visible b f x = f x
+app Hidden  b f x = f
+app Auto    b f x = f
+
+public export
+PI : (n : Nat) -> Visibility -> (a : Type) -> (Vect n a -> Type) -> Type
+PI Z     vis a b = b []
+PI (S n) vis a b = Pi vis a (\ x => PI n vis a (b . (x ::)))
+
+public export
+curry : (n : Nat) -> (vis : Visibility) ->
+        (0 b : Vect n a -> Type) ->
+        ((as : Vect n a) -> b as) ->
+        PI n vis a b
+curry 0 vis b f = f []
+curry (S n) vis b f
+  = lam vis _ $ \ x => curry n vis (b . (x ::)) (\ xs => f (x :: xs))
+
+public export
+uncurry : (n : Nat) -> (vis : Visibility) ->
+          (0 b : Vect n a -> Type) ->
+          PI n vis a b ->
+          (as : Vect n a) -> b as
+uncurry 0 vis b f [] = f
+uncurry (S n) vis b f (x :: xs)
+  = uncurry n vis (b . (x ::)) (app vis _ f x) xs