git.iko.soy/rel8
on c8341c1 help sign in
rel8/src/Rel8/Generic/Record.hs
152 lines 4.0 kB history raw
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 #-}
13module Rel8.Generic.Record
14 ( Record(..)
15 )
16where
18-- base
19import Data.Kind ( Constraint, Type )
20import GHC.Generics
21 ( Generic, Rep, from, to
22 , (:+:)( L1, R1 ), (:*:)( (:*:) ), M1( M1 )
23 , Meta( MetaCons, MetaSel ), D, C, S
24 )
25import GHC.TypeLits ( type (+), AppendSymbol, Div, Mod, Nat, Symbol )
26import Prelude hiding ( Show )
29type Recordize :: (Type -> Type) -> Type -> Type
30type family Recordize rep where
31 Recordize (M1 D meta rep) = M1 D meta (Recordize rep)
32 Recordize (l :+: r) = Recordize l :+: Recordize r
33 Recordize (M1 C ('MetaCons name fixity 'False) rep) =
34 M1 C ('MetaCons name fixity 'True) (Snd (Count 0 rep))
35 Recordize rep = rep
38type Count :: Nat -> (Type -> Type) -> (Nat, Type -> Type)
39type family Count n rep where
40 Count n (M1 S ('MetaSel _selector su ss ds) rep) =
41 '(n + 1, M1 S ('MetaSel ('Just (Show (n + 1))) su ss ds) rep)
42 Count n (a :*: b) = CountHelper1 (Count n a) b
43 Count n rep = '(n, rep)
46type CountHelper1 :: (Nat, Type -> Type) -> (Type -> Type) -> (Nat, Type -> Type)
47type family CountHelper1 tuple b where
48 CountHelper1 '(n, a) b = CountHelper2 a (Count n b)
51type CountHelper2 :: (Type -> Type) -> (Nat, Type -> Type) -> (Nat, Type -> Type)
52type family CountHelper2 a tuple where
53 CountHelper2 a '(n, b) = '(n, a :*: b)
56type Show :: Nat -> Symbol
57type Show n =
58 AppendSymbol "_" (AppendSymbol (Show' (Div n 10)) (ShowDigit (Mod n 10)))
61type Show' :: Nat -> Symbol
62type family Show' n where
63 Show' 0 = ""
64 Show' n = AppendSymbol (Show' (Div n 10)) (ShowDigit (Mod n 10))
67type ShowDigit :: Nat -> Symbol
68type family ShowDigit n where
69 ShowDigit 0 = "0"
70 ShowDigit 1 = "1"
71 ShowDigit 2 = "2"
72 ShowDigit 3 = "3"
73 ShowDigit 4 = "4"
74 ShowDigit 5 = "5"
75 ShowDigit 6 = "6"
76 ShowDigit 7 = "7"
77 ShowDigit 8 = "8"
78 ShowDigit 9 = "9"
81type Snd :: (a, b) -> b
82type family Snd tuple where
83 Snd '(_a, b) = b
86type Recordizable :: (Type -> Type) -> Constraint
87class Recordizable rep where
88 recordize :: rep x -> Recordize rep x
89 unrecordize :: Recordize rep x -> rep x
92instance Recordizable rep => Recordizable (M1 D meta rep) where
93 recordize (M1 a) = M1 (recordize a)
94 unrecordize (M1 a) = M1 (unrecordize a)
97instance (Recordizable l, Recordizable r) => Recordizable (l :+: r) where
98 recordize (L1 a) = L1 (recordize a)
99 recordize (R1 a) = R1 (recordize a)
100 unrecordize (L1 a) = L1 (unrecordize a)
101 unrecordize (R1 a) = R1 (unrecordize a)
104instance Countable 0 rep =>
105 Recordizable (M1 C ('MetaCons name fixity 'False) rep)
106 where
107 recordize (M1 a) = M1 (count @0 a)
108 unrecordize (M1 a) = M1 (uncount @0 a)
111instance {-# OVERLAPPABLE #-} Recordize rep ~ rep => Recordizable rep where
112 recordize = id
113 unrecordize = id
116type Countable :: Nat -> (Type -> Type) -> Constraint
117class Countable n rep where
118 count :: rep x -> Snd (Count n rep) x
119 uncount :: Snd (Count n rep) x -> rep x
122instance Countable n (M1 S ('MetaSel selector su ss ds) rep) where
123 count (M1 a) = M1 a
124 uncount (M1 a) = M1 a
127instance
128 ( Countable n a, Countable n' b
129 , '(n', a') ~ Count n a
130 , Snd (CountHelper2 a' (Count n' b)) ~ (a' :*: Snd (Count n' b))
131 )
132 => Countable n (a :*: b)
133 where
134 count (a :*: b) = count @n a :*: count @n' b
135 uncount (a :*: b) = uncount @n a :*: uncount @n' b
138instance {-# OVERLAPPABLE #-} Snd (Count n rep) ~ rep => Countable n rep where
139 count = id
140 uncount = id
143newtype Record a = Record
144 { unrecord :: a
145 }
148instance (Generic a, Recordizable (Rep a)) => Generic (Record a) where
149 type Rep (Record a) = Recordize (Rep a)
151 from (Record a) = recordize (from a)
152 to = Record . to . unrecordize