From b9f249a9ff1e548ed979a8d802eaec9c81a8ddf0 Mon Sep 17 00:00:00 2001
From: rnhmjoj <micheleguerinirocco@me.com>
Date: Sun, 27 Nov 2016 20:16:23 +0100
Subject: [PATCH] raise Data.Function to the type levels

---
 src/Data/Function.hs | 40 +++++++++++++++++++++++++---------------
 1 file changed, 25 insertions(+), 15 deletions(-)

diff --git a/src/Data/Function.hs b/src/Data/Function.hs
index c66b896..8b65cc4 100644
--- a/src/Data/Function.hs
+++ b/src/Data/Function.hs
@@ -14,26 +14,36 @@
 -- | Defines commonly used functions and combinators
 module Data.Function where
 
--- | Identity Function
-id ∷ ∀ (a ∷ ★). a → a
-id x = x
+import Data.Singletons.TH
 
--- | Constant function
-const ∷ ∀ (a ∷ ★) (b ∷ ★). a → b → a
-const k _ = k
+singletons [d|
 
--- | Undefined
-(⊥) ∷ ∀ a. a
-(⊥) = (⊥)
+  -- | Identity function
+  id ∷ ∀ a. a → a
+  id x = x
+
+  -- | Constant function
+  const ∷ ∀ a b. a → b → a
+  const k _ = k
+
+  -- | Flip the arguments of a function
+  flip ∷ ∀ a b c. (a → b → c) → (b → a → c)
+  flip f x y = f y x
+
+  -- | Undefined
+  (⊥) ∷ ∀ a. a
+  (⊥) = (⊥)
+
+  infixr 9 ∘
+
+  -- | Function composition operator
+  (∘) :: ∀ a b c. (b → c) → (a → b) → a → c
+  f ∘ g = \x → f (g x)
+
+  |]
 
 infixr 0 $
-infixr 9 ∘
 
 -- | Function application operator
 ($) ∷ ∀ a b. (a → b) → a → b
 f $ x = f x
-
--- | Function composition operator
-(∘) :: ∀ a b c. (b → c) → (a → b) → a → c
-f ∘ g = \x → f (g x)
-