@@ -0,0 +1,148 @@
1+{-# language AllowAmbiguousTypes #-}
2+{-# language DataKinds #-}
3+{-# language FlexibleInstances #-}
4+{-# language MultiParamTypeClasses #-}
5+{-# language PolyKinds #-}
6+{-# language ScopedTypeVariables #-}
7+{-# language StandaloneKindSignatures #-}
8+{-# language TypeApplications #-}
9+{-# language TypeFamilies #-}
10+{-# language TypeOperators #-}
11+{-# language UndecidableInstances #-}
12+
13+module Rel8.Generic.Record
14+ ( Record(..)
15+ )
16+where
17+
18+-- base
19+import Data.Kind ( Constraint, Type )
20+import GHC.Generics
21+import GHC.TypeLits
22+import Prelude hiding ( Show )
23+
24+
25+type Recordize :: (Type -> Type) -> Type -> Type
26+type family Recordize rep where
27+ Recordize (M1 D meta rep) = M1 D meta (Recordize rep)
28+ Recordize (l :+: r) = Recordize l :+: Recordize r
29+ Recordize (M1 C ('MetaCons name fixity 'False) rep) =
30+ M1 C ('MetaCons name fixity 'True) (Snd (Count 0 rep))
31+ Recordize rep = rep
32+
33+
34+type Count :: Nat -> (Type -> Type) -> (Nat, Type -> Type)
35+type family Count n rep where
36+ Count n (M1 S ('MetaSel _selector su ss ds) rep) =
37+ '(n + 1, M1 S ('MetaSel ('Just (Show (n + 1))) su ss ds) rep)
38+ Count n (a :*: b) = CountHelper1 (Count n a) b
39+ Count n rep = '(n, rep)
40+
41+
42+type CountHelper1 :: (Nat, Type -> Type) -> (Type -> Type) -> (Nat, Type -> Type)
43+type family CountHelper1 tuple b where
44+ CountHelper1 '(n, a) b = CountHelper2 a (Count n b)
45+
46+
47+type CountHelper2 :: (Type -> Type) -> (Nat, Type -> Type) -> (Nat, Type -> Type)
48+type family CountHelper2 a tuple where
49+ CountHelper2 a '(n, b) = '(n, a :*: b)
50+
51+
52+type Show :: Nat -> Symbol
53+type Show n =
54+ AppendSymbol "_" (AppendSymbol (Show' (Div n 10)) (ShowDigit (Mod n 10)))
55+
56+
57+type Show' :: Nat -> Symbol
58+type family Show' n where
59+ Show' 0 = ""
60+ Show' n = AppendSymbol (Show' (Div n 10)) (ShowDigit (Mod n 10))
61+
62+
63+type ShowDigit :: Nat -> Symbol
64+type family ShowDigit n where
65+ ShowDigit 0 = "0"
66+ ShowDigit 1 = "1"
67+ ShowDigit 2 = "2"
68+ ShowDigit 3 = "3"
69+ ShowDigit 4 = "4"
70+ ShowDigit 5 = "5"
71+ ShowDigit 6 = "6"
72+ ShowDigit 7 = "7"
73+ ShowDigit 8 = "8"
74+ ShowDigit 9 = "9"
75+
76+
77+type Snd :: (a, b) -> b
78+type family Snd tuple where
79+ Snd '(_a, b) = b
80+
81+
82+type Recordizable :: (Type -> Type) -> Constraint
83+class Recordizable rep where
84+ recordize :: rep x -> Recordize rep x
85+ unrecordize :: Recordize rep x -> rep x
86+
87+
88+instance Recordizable rep => Recordizable (M1 D meta rep) where
89+ recordize (M1 a) = M1 (recordize a)
90+ unrecordize (M1 a) = M1 (unrecordize a)
91+
92+
93+instance (Recordizable l, Recordizable r) => Recordizable (l :+: r) where
94+ recordize (L1 a) = L1 (recordize a)
95+ recordize (R1 a) = R1 (recordize a)
96+ unrecordize (L1 a) = L1 (unrecordize a)
97+ unrecordize (R1 a) = R1 (unrecordize a)
98+
99+
100+instance Countable 0 rep =>
101+ Recordizable (M1 C ('MetaCons name fixity 'False) rep)
102+ where
103+ recordize (M1 a) = M1 (count @0 a)
104+ unrecordize (M1 a) = M1 (uncount @0 a)
105+
106+
107+instance {-# OVERLAPPABLE #-} Recordize rep ~ rep => Recordizable rep where
108+ recordize = id
109+ unrecordize = id
110+
111+
112+type Countable :: Nat -> (Type -> Type) -> Constraint
113+class Countable n rep where
114+ count :: rep x -> Snd (Count n rep) x
115+ uncount :: Snd (Count n rep) x -> rep x
116+
117+
118+instance Countable n (M1 S ('MetaSel selector su ss ds) rep) where
119+ count (M1 a) = M1 a
120+ uncount (M1 a) = M1 a
121+
122+
123+instance
124+ ( Countable n a, Countable n' b
125+ , '(n', a') ~ Count n a
126+ , Snd (CountHelper2 a' (Count n' b)) ~ (a' :*: Snd (Count n' b))
127+ )
128+ => Countable n (a :*: b)
129+ where
130+ count (a :*: b) = count @n a :*: count @n' b
131+ uncount (a :*: b) = uncount @n a :*: uncount @n' b
132+
133+
134+instance {-# OVERLAPPABLE #-} Snd (Count n rep) ~ rep => Countable n rep where
135+ count = id
136+ uncount = id
137+
138+
139+newtype Record a = Record
140+ { unrecord :: a
141+ }
142+
143+
144+instance (Generic a, Recordizable (Rep a)) => Generic (Record a) where
145+ type Rep (Record a) = Recordize (Rep a)
146+
147+ from (Record a) = recordize (from a)
148+ to = Record . to . unrecordize