Skip to content

Clean up Singletons module #31

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
mrkgnao wants to merge 5 commits into
base: master
Choose a base branch
from
Open

Clean up Singletons module #31

Changes from 1 commit
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
e2ca6b2
Clean up Singletons module
mrkgnao Jun 18, 2017
9edbe9c
Remove useless "kind inference" constructors
mrkgnao Jun 18, 2017
85d7a6e
Remove most of the Singletons module
mrkgnao Jun 18, 2017
b9aeff8
De-align code to fit original style
mrkgnao Jun 18, 2017
501629d
Add in removed Apply instances to fix defunctionalization
mrkgnao Jun 19, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
242 changes: 124 additions & 118 deletions src/lib/Tisch/Internal/Singletons.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 #-}

@k0001 k0001 Jun 18, 2017

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

FWIW, the reason why I don't align these things vertically is because of what we are seeing here: When one line changes and this change shortens or widens the largest language extension name, then one needs to change all of the lines so that #-} aligns vertically again. The same goes for imports and as, except in imports it's even worse because one also needs to worry about how to format things when the import takes more than one line, something that looks very ugly when things are vertically aligned.

It's a small detail, but it makes maintaining and reviewing code a much pleasurable experience.

@mrkgnao mrkgnao Jun 18, 2017 •
edited
Loading

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm sorry, this was from stylish-haskell running automatically on save. I understand the diff problems that aligning code brings. :)


module Tisch.Internal.Singletons
( First
Expand All @@ -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

@k0001 k0001 Jun 18, 2017

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think we need these SuppressUnusedWarnings things. Can we remove them or do we get some warning? Also, I think you can delete all of the constructors named *KindInference, I don't think we need those.

@mrkgnao mrkgnao Jun 18, 2017 •
edited
Loading

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Removing them triggers -Wunused-top-binds warnings, which can be disabled module-locally if you'd prefer that. I'll look at the KindInference constructors.

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 ())