From e2ca6b24c2afb6ea17120c76e149b2aefe83ff6b Mon Sep 17 00:00:00 2001 From: Soham Chowdhury Date: Sun, 18 Jun 2017 18:17:05 +0530 Subject: [PATCH 1/5] Clean up Singletons module --- src/lib/Tisch/Internal/Singletons.hs | 242 ++++++++++++++------------- 1 file changed, 124 insertions(+), 118 deletions(-) diff --git a/src/lib/Tisch/Internal/Singletons.hs b/src/lib/Tisch/Internal/Singletons.hs index dc91b8a..5170d54 100644 --- a/src/lib/Tisch/Internal/Singletons.hs +++ b/src/lib/Tisch/Internal/Singletons.hs @@ -1,11 +1,11 @@ -- {-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} module Tisch.Internal.Singletons ( First @@ -25,123 +25,129 @@ module Tisch.Internal.Singletons , (:&&&$$$$) ) where -import Data.Singletons.TH -import Data.Kind - --------------------------------------------------------------------------------- - --- $(promoteOnly [d| --- -- Like 'Control.Arrow.first' for tuples. --- first :: (x -> x') -> (x, y) -> (x', y) --- first f (x, y) = (f x, y) --- --- -- Like 'Control.Arrow.second' for tuples. --- second :: (y -> y') -> (x, y) -> (x, y') --- second f (x, y) = (x, f y) --- --- infixr 3 &&& --- -- Like '(Control.Arrow.&&&)' for tuples. --- (&&&) :: (x -> y) -> (x -> z) -> x -> (y, z) --- (&&&) f g = \x -> (f x, g x) --- |]) --- --- ===> --- --- The ugly code below is generated by the ugly TH above. I expanded this --- using @-ddump-splices@ because otherwise I wasn't able to load this code --- into GHCi with profiling enabled. Not sure why. --- --- TODO: write these definitions by hand in a way that can be read. -type family Lambda_1627622444_aYtT f_aYtP g_aYtQ a_1627622439_aYtR t_aYtV where - Lambda_1627622444_aYtT f_aYtP g_aYtQ a_1627622439_aYtR x_aYtU = Apply (Apply Tuple2Sym0 (Apply f_aYtP x_aYtU)) (Apply g_aYtQ x_aYtU) -type Lambda_1627622444Sym4 t_aYtW t_aYtX t_aYtY t_aYtZ = Lambda_1627622444_aYtT t_aYtW t_aYtX t_aYtY t_aYtZ -instance SuppressUnusedWarnings Lambda_1627622444Sym3 where - suppressUnusedWarnings _ = snd ((,) Lambda_1627622444Sym3KindInference ()) -data Lambda_1627622444Sym3 l_aYua l_aYub l_aYuc l_aYu9 - = forall arg_aYud. KindOf (Apply (Lambda_1627622444Sym3 l_aYua l_aYub l_aYuc) arg_aYud) ~ KindOf (Lambda_1627622444Sym4 l_aYua l_aYub l_aYuc arg_aYud) => - Lambda_1627622444Sym3KindInference -type instance Apply (Lambda_1627622444Sym3 l_aYua l_aYub l_aYuc) l_aYu9 = Lambda_1627622444Sym4 l_aYua l_aYub l_aYuc l_aYu9 -instance SuppressUnusedWarnings Lambda_1627622444Sym2 where - suppressUnusedWarnings _ = snd ((,) Lambda_1627622444Sym2KindInference ()) -data Lambda_1627622444Sym2 l_aYu6 l_aYu7 l_aYu5 - = forall arg_aYu8. KindOf (Apply (Lambda_1627622444Sym2 l_aYu6 l_aYu7) arg_aYu8) ~ KindOf (Lambda_1627622444Sym3 l_aYu6 l_aYu7 arg_aYu8) => - Lambda_1627622444Sym2KindInference -type instance Apply (Lambda_1627622444Sym2 l_aYu6 l_aYu7) l_aYu5 = Lambda_1627622444Sym3 l_aYu6 l_aYu7 l_aYu5 -instance SuppressUnusedWarnings Lambda_1627622444Sym1 where - suppressUnusedWarnings _ = snd ((,) Lambda_1627622444Sym1KindInference ()) -data Lambda_1627622444Sym1 l_aYu3 l_aYu2 - = forall arg_aYu4. KindOf (Apply (Lambda_1627622444Sym1 l_aYu3) arg_aYu4) ~ KindOf (Lambda_1627622444Sym2 l_aYu3 arg_aYu4) => - Lambda_1627622444Sym1KindInference -type instance Apply (Lambda_1627622444Sym1 l_aYu3) l_aYu2 = Lambda_1627622444Sym2 l_aYu3 l_aYu2 -instance SuppressUnusedWarnings Lambda_1627622444Sym0 where - suppressUnusedWarnings _ = snd ((,) Lambda_1627622444Sym0KindInference ()) -data Lambda_1627622444Sym0 l_aYu0 - = forall arg_aYu1. KindOf (Apply Lambda_1627622444Sym0 arg_aYu1) ~ KindOf (Lambda_1627622444Sym1 arg_aYu1) => - Lambda_1627622444Sym0KindInference -type instance Apply Lambda_1627622444Sym0 l_aYu0 = Lambda_1627622444Sym1 l_aYu0 -type (:&&&$$$$) (t_aYty :: TyFun x1627622403 y1627622404 -> Type) - (t_aYtz :: TyFun x1627622403 z1627622405 -> Type) - (t_aYtA :: x1627622403) = (:&&&) t_aYty t_aYtz t_aYtA -instance SuppressUnusedWarnings (:&&&$$$) where - suppressUnusedWarnings _ = snd ((,) (:&&&$$$###) ()) -data (:&&&$$$) (l_aYtH :: TyFun x1627622403 y1627622404 -> Type) - (l_aYtI :: TyFun x1627622403 z1627622405 -> Type) - (l_aYtG :: TyFun x1627622403 (y1627622404, z1627622405)) - = forall arg_aYtJ. KindOf (Apply ((:&&&$$$) l_aYtH l_aYtI) arg_aYtJ) ~ KindOf ((:&&&$$$$) l_aYtH l_aYtI arg_aYtJ) => +import Data.Kind +import Data.Singletons.TH + +type Lambda1 p q r u = Apply (Apply Tuple2Sym0 (Apply p u)) (Apply q u) + +data LambdaSym3 a b c l = + forall d. KindOf (Apply (LambdaSym3 a b c) d) ~ KindOf (Lambda1 a b c d) => + LambdaSym3KindInference + +type instance Apply (LambdaSym3 a b c) l = Lambda1 a b c l + +data LambdaSym2 a b c + = forall z. KindOf (Apply (LambdaSym2 a b) z) ~ KindOf (LambdaSym3 a b z) => + LambdaSym2KindInference + +type instance Apply (LambdaSym2 a b) c = LambdaSym3 a b c + +data LambdaSym1 l k + = forall a. KindOf (Apply (LambdaSym1 l) a) ~ KindOf (LambdaSym2 l a) => + LambdaSym1KindInference + +type instance Apply (LambdaSym1 l) k = LambdaSym2 l k + +data LambdaSym0 l + = forall a1. KindOf (Apply LambdaSym0 a1) ~ KindOf (LambdaSym1 a1) => + LambdaSym0KindInference + +type instance Apply LambdaSym0 l = LambdaSym1 l + +type (:&&&$$$$) (y :: TyFun x y4 -> Type) + (z :: TyFun x z5 -> Type) + (a :: x3) = (:&&&) y z a + +data (:&&&$$$) (h :: TyFun x y -> Type) + (i :: TyFun x z -> Type) + (g :: TyFun x (y, z)) + = forall j. KindOf (Apply ((:&&&$$$) h i) j) ~ KindOf ((:&&&$$$$) h i j) => (:&&&$$$###) -type instance Apply ((:&&&$$$) l_aYtH l_aYtI) l_aYtG = (:&&&$$$$) l_aYtH l_aYtI l_aYtG -instance SuppressUnusedWarnings (:&&&$$) where - suppressUnusedWarnings _ = snd ((,) (:&&&$$###) ()) -data (:&&&$$) (l_aYtE :: TyFun x1627622403 y1627622404 -> Type) - (l_aYtD :: TyFun (TyFun x1627622403 z1627622405 -> Type) (TyFun x1627622403 (y1627622404, z1627622405) -> Type)) - = forall arg_aYtF. KindOf (Apply ((:&&&$$) l_aYtE) arg_aYtF) ~ KindOf ((:&&&$$$) l_aYtE arg_aYtF) => + +type instance Apply ((:&&&$$$) h i) g = (:&&&$$$$) h i g + +data (:&&&$$) (e :: TyFun x y -> Type) + (d :: TyFun (TyFun x z -> Type) (TyFun x (y, z) -> Type)) + = forall f. KindOf (Apply ((:&&&$$) e) f) ~ KindOf ((:&&&$$$) e f) => (:&&&$$###) -type instance Apply ((:&&&$$) l_aYtE) l_aYtD = (:&&&$$$) l_aYtE l_aYtD -instance SuppressUnusedWarnings (:&&&$) where - suppressUnusedWarnings _ = snd ((,) (:&&&$###) ()) -data (:&&&$) (l_aYtB :: TyFun (TyFun x1627622403 y1627622404 -> Type) (TyFun (TyFun x1627622403 z1627622405 -> Type) (TyFun x1627622403 (y1627622404, z1627622405) -> Type) -> Type)) - = forall arg_aYtC. KindOf (Apply (:&&&$) arg_aYtC) ~ KindOf ((:&&&$$) arg_aYtC) => + +type instance Apply ((:&&&$$) e) d = (:&&&$$$) e d + +data (:&&&$) + (b :: TyFun (TyFun x y -> Type) + (TyFun (TyFun x z -> Type) + (TyFun x (y, z) -> Type) -> Type)) + = forall a. KindOf (Apply (:&&&$) a) ~ KindOf ((:&&&$$) a) => (:&&&$###) -type instance Apply (:&&&$) l_aYtB = (:&&&$$) l_aYtB -type SecondSym2 (t_aYue :: TyFun y1627622406 y'1627622407 -> Type) - (t_aYuf :: (x1627622408, y1627622406)) = Second t_aYue t_aYuf -instance SuppressUnusedWarnings SecondSym1 where - suppressUnusedWarnings _ = snd ((,) SecondSym1KindInference ()) -data SecondSym1 (l_aYuj :: TyFun y1627622406 y'1627622407 -> Type) - (l_aYui :: TyFun (x1627622408, y1627622406) (x1627622408, y'1627622407)) - = forall arg_aYuk. KindOf (Apply (SecondSym1 l_aYuj) arg_aYuk) ~ KindOf (SecondSym2 l_aYuj arg_aYuk) => + +type instance Apply (:&&&$) b = (:&&&$$) b + +type SecondSym2 (e :: TyFun y6 y7 -> Type) + (f :: (x8, y6)) = Second e f +data SecondSym1 (j :: TyFun y6 y7 -> Type) + (i :: TyFun (x8, y6) (x8, y7)) + = forall k. KindOf (Apply (SecondSym1 j) k) ~ KindOf (SecondSym2 j k) => SecondSym1KindInference -type instance Apply (SecondSym1 l_aYuj) l_aYui = SecondSym2 l_aYuj l_aYui -instance SuppressUnusedWarnings SecondSym0 where - suppressUnusedWarnings _ = snd ((,) SecondSym0KindInference ()) -data SecondSym0 (l_aYug :: TyFun (TyFun y1627622406 y'1627622407 -> Type) (TyFun (x1627622408, y1627622406) (x1627622408, y'1627622407) -> Type)) - = forall arg_aYuh. KindOf (Apply SecondSym0 arg_aYuh) ~ KindOf (SecondSym1 arg_aYuh) => - SecondSym0KindInference -type instance Apply SecondSym0 l_aYug = SecondSym1 l_aYug -type FirstSym2 (t_aYuq :: TyFun x1627622409 x'1627622410 -> Type) - (t_aYur :: (x1627622409, y1627622411)) = First t_aYuq t_aYur -instance SuppressUnusedWarnings FirstSym1 where - suppressUnusedWarnings _ = snd ((,) FirstSym1KindInference ()) -data FirstSym1 (l_aYuv :: TyFun x1627622409 x'1627622410 -> Type) - (l_aYuu :: TyFun (x1627622409, y1627622411) (x'1627622410, y1627622411)) - = forall arg_aYuw. KindOf (Apply (FirstSym1 l_aYuv) arg_aYuw) ~ KindOf (FirstSym2 l_aYuv arg_aYuw) => + +type instance Apply (SecondSym1 j) i = SecondSym2 j i + +data SecondSym0 (g :: + TyFun (TyFun y6 y7 -> Type) (TyFun (x8, y6) (x8, y7) -> Type)) = + forall h. KindOf (Apply SecondSym0 h) ~ KindOf (SecondSym1 h) => + SecondSym0KindInference + +type instance Apply SecondSym0 g = SecondSym1 g + +type FirstSym2 (q :: TyFun x9 x10 -> Type) + (r :: (x9, y11)) = First q r + +data FirstSym1 (v :: TyFun x9 x10 -> Type) + (l :: TyFun (x9, y11) (x10, y11)) + = forall w. KindOf (Apply (FirstSym1 v) w) ~ KindOf (FirstSym2 v w) => FirstSym1KindInference -type instance Apply (FirstSym1 l_aYuv) l_aYuu = FirstSym2 l_aYuv l_aYuu -instance SuppressUnusedWarnings FirstSym0 where - suppressUnusedWarnings _ = snd ((,) FirstSym0KindInference ()) -data FirstSym0 (l_aYus :: TyFun (TyFun x1627622409 x'1627622410 -> Type) (TyFun (x1627622409, y1627622411) (x'1627622410, y1627622411) -> Type)) - = forall arg_aYut. KindOf (Apply FirstSym0 arg_aYut) ~ KindOf (FirstSym1 arg_aYut) => + +type instance Apply (FirstSym1 v) l = FirstSym2 v l + +data FirstSym0 (s :: TyFun (TyFun x9 x10 -> Type) (TyFun (x9, y11) (x10, y11) -> Type)) + = forall a. KindOf (Apply FirstSym0 a) ~ KindOf (FirstSym1 a) => FirstSym0KindInference -type instance Apply FirstSym0 l_aYus = FirstSym1 l_aYus -type family (:&&&) (a_aYtK :: TyFun x_aYtd y_aYte -> Type) - (a_aYtL :: TyFun x_aYtd z_aYtf -> Type) - (a_aYtM :: x_aYtd) :: (y_aYte, z_aYtf) where - (:&&&) f_aYtP g_aYtQ a_1627622439_aYtR = Apply (Apply (Apply (Apply Lambda_1627622444Sym0 f_aYtP) g_aYtQ) a_1627622439_aYtR) a_1627622439_aYtR -type family Second (a_aYul :: TyFun y_aYtg y'_aYth -> Type) - (a_aYum :: (x_aYti, y_aYtg)) :: (x_aYti, y'_aYth) where - Second f_aYun '(x_aYuo, y_aYup) = Apply (Apply Tuple2Sym0 x_aYuo) (Apply f_aYun y_aYup) -type family First (a_aYux :: TyFun x_aYtj x'_aYtk -> Type) - (a_aYuy :: (x_aYtj, y_aYtl)) :: (x'_aYtk, y_aYtl) where - First f_aYuz '(x_aYuA, y_aYuB) = Apply (Apply Tuple2Sym0 (Apply f_aYuz x_aYuA)) y_aYuB + +type instance Apply FirstSym0 s = FirstSym1 s + +type family (:&&&) (k :: TyFun d e -> Type) + (l :: TyFun d f -> Type) + (m :: d) :: (e, f) where + (:&&&) p q r = Apply (Apply (Apply (Apply LambdaSym0 p) q) r) r + +type family Second (l :: TyFun g h -> Type) + (m :: (i, g)) :: (i, h) where + Second n '(o, p) = Apply (Apply Tuple2Sym0 o) (Apply n p) + +type family First (x :: TyFun j k -> Type) + (y :: (j, l)) :: (k, l) where + First z '(a, b) = Apply (Apply Tuple2Sym0 (Apply z a)) b + infixr 3 :&&& +instance SuppressUnusedWarnings (:&&&$) where + suppressUnusedWarnings _ = snd ((,) (:&&&$###) ()) +instance SuppressUnusedWarnings (:&&&$$) where + suppressUnusedWarnings _ = snd ((,) (:&&&$$###) ()) +instance SuppressUnusedWarnings (:&&&$$$) where + suppressUnusedWarnings _ = snd ((,) (:&&&$$$###) ()) +instance SuppressUnusedWarnings FirstSym0 where + suppressUnusedWarnings _ = snd ((,) FirstSym0KindInference ()) +instance SuppressUnusedWarnings FirstSym1 where + suppressUnusedWarnings _ = snd ((,) FirstSym1KindInference ()) +instance SuppressUnusedWarnings SecondSym0 where + suppressUnusedWarnings _ = snd ((,) SecondSym0KindInference ()) +instance SuppressUnusedWarnings SecondSym1 where + suppressUnusedWarnings _ = snd ((,) SecondSym1KindInference ()) +instance SuppressUnusedWarnings LambdaSym0 where + suppressUnusedWarnings _ = snd ((,) LambdaSym0KindInference ()) +instance SuppressUnusedWarnings LambdaSym1 where + suppressUnusedWarnings _ = snd ((,) LambdaSym1KindInference ()) +instance SuppressUnusedWarnings LambdaSym2 where + suppressUnusedWarnings _ = snd ((,) LambdaSym2KindInference ()) +instance SuppressUnusedWarnings LambdaSym3 where + suppressUnusedWarnings _ = snd ((,) LambdaSym3KindInference ()) From 9edbe9cf80679f0a21c9bb04493085b186e9f7dc Mon Sep 17 00:00:00 2001 From: Soham Chowdhury Date: Sun, 18 Jun 2017 23:24:40 +0530 Subject: [PATCH 2/5] Remove useless "kind inference" constructors --- src/lib/Tisch/Internal/Singletons.hs | 49 ++-------------------------- 1 file changed, 2 insertions(+), 47 deletions(-) diff --git a/src/lib/Tisch/Internal/Singletons.hs b/src/lib/Tisch/Internal/Singletons.hs index 5170d54..fdf8960 100644 --- a/src/lib/Tisch/Internal/Singletons.hs +++ b/src/lib/Tisch/Internal/Singletons.hs @@ -30,27 +30,19 @@ import Data.Singletons.TH type Lambda1 p q r u = Apply (Apply Tuple2Sym0 (Apply p u)) (Apply q u) -data LambdaSym3 a b c l = - forall d. KindOf (Apply (LambdaSym3 a b c) d) ~ KindOf (Lambda1 a b c d) => - LambdaSym3KindInference +data LambdaSym3 a b c l type instance Apply (LambdaSym3 a b c) l = Lambda1 a b c l data LambdaSym2 a b c - = forall z. KindOf (Apply (LambdaSym2 a b) z) ~ KindOf (LambdaSym3 a b z) => - LambdaSym2KindInference type instance Apply (LambdaSym2 a b) c = LambdaSym3 a b c data LambdaSym1 l k - = forall a. KindOf (Apply (LambdaSym1 l) a) ~ KindOf (LambdaSym2 l a) => - LambdaSym1KindInference type instance Apply (LambdaSym1 l) k = LambdaSym2 l k data LambdaSym0 l - = forall a1. KindOf (Apply LambdaSym0 a1) ~ KindOf (LambdaSym1 a1) => - LambdaSym0KindInference type instance Apply LambdaSym0 l = LambdaSym1 l @@ -61,15 +53,11 @@ type (:&&&$$$$) (y :: TyFun x y4 -> Type) data (:&&&$$$) (h :: TyFun x y -> Type) (i :: TyFun x z -> Type) (g :: TyFun x (y, z)) - = forall j. KindOf (Apply ((:&&&$$$) h i) j) ~ KindOf ((:&&&$$$$) h i j) => - (:&&&$$$###) type instance Apply ((:&&&$$$) h i) g = (:&&&$$$$) h i g data (:&&&$$) (e :: TyFun x y -> Type) (d :: TyFun (TyFun x z -> Type) (TyFun x (y, z) -> Type)) - = forall f. KindOf (Apply ((:&&&$$) e) f) ~ KindOf ((:&&&$$$) e f) => - (:&&&$$###) type instance Apply ((:&&&$$) e) d = (:&&&$$$) e d @@ -77,8 +65,6 @@ data (:&&&$) (b :: TyFun (TyFun x y -> Type) (TyFun (TyFun x z -> Type) (TyFun x (y, z) -> Type) -> Type)) - = forall a. KindOf (Apply (:&&&$) a) ~ KindOf ((:&&&$$) a) => - (:&&&$###) type instance Apply (:&&&$) b = (:&&&$$) b @@ -86,15 +72,11 @@ type SecondSym2 (e :: TyFun y6 y7 -> Type) (f :: (x8, y6)) = Second e f data SecondSym1 (j :: TyFun y6 y7 -> Type) (i :: TyFun (x8, y6) (x8, y7)) - = forall k. KindOf (Apply (SecondSym1 j) k) ~ KindOf (SecondSym2 j k) => - SecondSym1KindInference type instance Apply (SecondSym1 j) i = SecondSym2 j i data SecondSym0 (g :: - TyFun (TyFun y6 y7 -> Type) (TyFun (x8, y6) (x8, y7) -> Type)) = - forall h. KindOf (Apply SecondSym0 h) ~ KindOf (SecondSym1 h) => - SecondSym0KindInference + TyFun (TyFun y6 y7 -> Type) (TyFun (x8, y6) (x8, y7) -> Type)) type instance Apply SecondSym0 g = SecondSym1 g @@ -103,14 +85,10 @@ type FirstSym2 (q :: TyFun x9 x10 -> Type) data FirstSym1 (v :: TyFun x9 x10 -> Type) (l :: TyFun (x9, y11) (x10, y11)) - = forall w. KindOf (Apply (FirstSym1 v) w) ~ KindOf (FirstSym2 v w) => - FirstSym1KindInference type instance Apply (FirstSym1 v) l = FirstSym2 v l data FirstSym0 (s :: TyFun (TyFun x9 x10 -> Type) (TyFun (x9, y11) (x10, y11) -> Type)) - = forall a. KindOf (Apply FirstSym0 a) ~ KindOf (FirstSym1 a) => - FirstSym0KindInference type instance Apply FirstSym0 s = FirstSym1 s @@ -128,26 +106,3 @@ type family First (x :: TyFun j k -> Type) First z '(a, b) = Apply (Apply Tuple2Sym0 (Apply z a)) b infixr 3 :&&& - -instance SuppressUnusedWarnings (:&&&$) where - suppressUnusedWarnings _ = snd ((,) (:&&&$###) ()) -instance SuppressUnusedWarnings (:&&&$$) where - suppressUnusedWarnings _ = snd ((,) (:&&&$$###) ()) -instance SuppressUnusedWarnings (:&&&$$$) where - suppressUnusedWarnings _ = snd ((,) (:&&&$$$###) ()) -instance SuppressUnusedWarnings FirstSym0 where - suppressUnusedWarnings _ = snd ((,) FirstSym0KindInference ()) -instance SuppressUnusedWarnings FirstSym1 where - suppressUnusedWarnings _ = snd ((,) FirstSym1KindInference ()) -instance SuppressUnusedWarnings SecondSym0 where - suppressUnusedWarnings _ = snd ((,) SecondSym0KindInference ()) -instance SuppressUnusedWarnings SecondSym1 where - suppressUnusedWarnings _ = snd ((,) SecondSym1KindInference ()) -instance SuppressUnusedWarnings LambdaSym0 where - suppressUnusedWarnings _ = snd ((,) LambdaSym0KindInference ()) -instance SuppressUnusedWarnings LambdaSym1 where - suppressUnusedWarnings _ = snd ((,) LambdaSym1KindInference ()) -instance SuppressUnusedWarnings LambdaSym2 where - suppressUnusedWarnings _ = snd ((,) LambdaSym2KindInference ()) -instance SuppressUnusedWarnings LambdaSym3 where - suppressUnusedWarnings _ = snd ((,) LambdaSym3KindInference ()) From 85d7a6e3fd8704676a4c9eed5d9014c3dd011aeb Mon Sep 17 00:00:00 2001 From: Soham Chowdhury Date: Sun, 18 Jun 2017 23:39:35 +0530 Subject: [PATCH 3/5] Remove most of the Singletons module --- src/lib/Tisch/Internal/Singletons.hs | 71 +--------------------------- 1 file changed, 2 insertions(+), 69 deletions(-) diff --git a/src/lib/Tisch/Internal/Singletons.hs b/src/lib/Tisch/Internal/Singletons.hs index fdf8960..3e6001a 100644 --- a/src/lib/Tisch/Internal/Singletons.hs +++ b/src/lib/Tisch/Internal/Singletons.hs @@ -1,4 +1,3 @@ --- {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE PolyKinds #-} @@ -8,17 +7,7 @@ {-# LANGUAGE UndecidableInstances #-} module Tisch.Internal.Singletons - ( First - , FirstSym0 - , FirstSym1 - , FirstSym2 - - , Second - , SecondSym0 - , SecondSym1 - , SecondSym2 - - , (:&&&) + ( (:&&&) , (:&&&$) , (:&&&$$) , (:&&&$$$) @@ -28,24 +17,6 @@ module Tisch.Internal.Singletons import Data.Kind import Data.Singletons.TH -type Lambda1 p q r u = Apply (Apply Tuple2Sym0 (Apply p u)) (Apply q u) - -data LambdaSym3 a b c l - -type instance Apply (LambdaSym3 a b c) l = Lambda1 a b c l - -data LambdaSym2 a b c - -type instance Apply (LambdaSym2 a b) c = LambdaSym3 a b c - -data LambdaSym1 l k - -type instance Apply (LambdaSym1 l) k = LambdaSym2 l k - -data LambdaSym0 l - -type instance Apply LambdaSym0 l = LambdaSym1 l - type (:&&&$$$$) (y :: TyFun x y4 -> Type) (z :: TyFun x z5 -> Type) (a :: x3) = (:&&&) y z a @@ -54,55 +25,17 @@ data (:&&&$$$) (h :: TyFun x y -> Type) (i :: TyFun x z -> Type) (g :: TyFun x (y, z)) -type instance Apply ((:&&&$$$) h i) g = (:&&&$$$$) h i g - data (:&&&$$) (e :: TyFun x y -> Type) (d :: TyFun (TyFun x z -> Type) (TyFun x (y, z) -> Type)) -type instance Apply ((:&&&$$) e) d = (:&&&$$$) e d - data (:&&&$) (b :: TyFun (TyFun x y -> Type) (TyFun (TyFun x z -> Type) (TyFun x (y, z) -> Type) -> Type)) -type instance Apply (:&&&$) b = (:&&&$$) b - -type SecondSym2 (e :: TyFun y6 y7 -> Type) - (f :: (x8, y6)) = Second e f -data SecondSym1 (j :: TyFun y6 y7 -> Type) - (i :: TyFun (x8, y6) (x8, y7)) - -type instance Apply (SecondSym1 j) i = SecondSym2 j i - -data SecondSym0 (g :: - TyFun (TyFun y6 y7 -> Type) (TyFun (x8, y6) (x8, y7) -> Type)) - -type instance Apply SecondSym0 g = SecondSym1 g - -type FirstSym2 (q :: TyFun x9 x10 -> Type) - (r :: (x9, y11)) = First q r - -data FirstSym1 (v :: TyFun x9 x10 -> Type) - (l :: TyFun (x9, y11) (x10, y11)) - -type instance Apply (FirstSym1 v) l = FirstSym2 v l - -data FirstSym0 (s :: TyFun (TyFun x9 x10 -> Type) (TyFun (x9, y11) (x10, y11) -> Type)) - -type instance Apply FirstSym0 s = FirstSym1 s - type family (:&&&) (k :: TyFun d e -> Type) (l :: TyFun d f -> Type) (m :: d) :: (e, f) where - (:&&&) p q r = Apply (Apply (Apply (Apply LambdaSym0 p) q) r) r - -type family Second (l :: TyFun g h -> Type) - (m :: (i, g)) :: (i, h) where - Second n '(o, p) = Apply (Apply Tuple2Sym0 o) (Apply n p) - -type family First (x :: TyFun j k -> Type) - (y :: (j, l)) :: (k, l) where - First z '(a, b) = Apply (Apply Tuple2Sym0 (Apply z a)) b + (:&&&) p q r = Apply (Apply Tuple2Sym0 (Apply p r)) (Apply q r) infixr 3 :&&& From b9aeff860135990c0dd4c76d8a8653543b025573 Mon Sep 17 00:00:00 2001 From: Soham Chowdhury Date: Sun, 18 Jun 2017 23:42:45 +0530 Subject: [PATCH 4/5] De-align code to fit original style --- src/lib/Tisch/Internal/Singletons.hs | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/lib/Tisch/Internal/Singletons.hs b/src/lib/Tisch/Internal/Singletons.hs index 3e6001a..b36994a 100644 --- a/src/lib/Tisch/Internal/Singletons.hs +++ b/src/lib/Tisch/Internal/Singletons.hs @@ -1,10 +1,9 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} module Tisch.Internal.Singletons ( (:&&&) @@ -14,8 +13,8 @@ module Tisch.Internal.Singletons , (:&&&$$$$) ) where -import Data.Kind -import Data.Singletons.TH +import Data.Kind +import Data.Singletons.TH type (:&&&$$$$) (y :: TyFun x y4 -> Type) (z :: TyFun x z5 -> Type) From 501629d6b8f4840b3403893ddb0b25b3406ded88 Mon Sep 17 00:00:00 2001 From: Soham Chowdhury Date: Mon, 19 Jun 2017 08:19:57 +0530 Subject: [PATCH 5/5] Add in removed Apply instances to fix defunctionalization --- src/lib/Tisch/Internal/Singletons.hs | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/lib/Tisch/Internal/Singletons.hs b/src/lib/Tisch/Internal/Singletons.hs index b36994a..2966934 100644 --- a/src/lib/Tisch/Internal/Singletons.hs +++ b/src/lib/Tisch/Internal/Singletons.hs @@ -16,9 +16,9 @@ module Tisch.Internal.Singletons import Data.Kind import Data.Singletons.TH -type (:&&&$$$$) (y :: TyFun x y4 -> Type) - (z :: TyFun x z5 -> Type) - (a :: x3) = (:&&&) y z a +type (:&&&$$$$) (a :: TyFun x y -> Type) + (b :: TyFun x z -> Type) + (c :: x) = (:&&&) a b c data (:&&&$$$) (h :: TyFun x y -> Type) (i :: TyFun x z -> Type) @@ -32,6 +32,10 @@ data (:&&&$) (TyFun (TyFun x z -> Type) (TyFun x (y, z) -> Type) -> Type)) +type instance Apply (:&&&$) b = (:&&&$$) b +type instance Apply ((:&&&$$) a) b = (:&&&$$$) a b +type instance Apply ((:&&&$$$) a b) c = (:&&&$$$$) a b c + type family (:&&&) (k :: TyFun d e -> Type) (l :: TyFun d f -> Type) (m :: d) :: (e, f) where