git.iko.soy/rel8
on 22deaf2 help sign in
rel8/src/Rel8/Generic/Record.hs
153 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 , GRecordable, GRecord, grecord, gunrecord
16 )
17where
19-- base
20import Data.Kind ( Constraint, Type )
21import GHC.Generics
22 ( Generic, Rep, from, to
23 , (:+:)( L1, R1 ), (:*:)( (:*:) ), M1( M1 )
24 , Meta( MetaCons, MetaSel ), D, C, S
25 )
26import GHC.TypeLits ( type (+), AppendSymbol, Div, Mod, Nat, Symbol )
27import Prelude hiding ( Show )
30type GRecord :: (Type -> Type) -> Type -> Type
31type family GRecord rep where
32 GRecord (M1 D meta rep) = M1 D meta (GRecord rep)
33 GRecord (l :+: r) = GRecord l :+: GRecord r
34 GRecord (M1 C ('MetaCons name fixity 'False) rep) =
35 M1 C ('MetaCons name fixity 'True) (Snd (Count 0 rep))
36 GRecord rep = rep
39type Count :: Nat -> (Type -> Type) -> (Nat, Type -> Type)
40type family Count n rep where
41 Count n (M1 S ('MetaSel _selector su ss ds) rep) =
42 '(n + 1, M1 S ('MetaSel ('Just (Show (n + 1))) su ss ds) rep)
43 Count n (a :*: b) = CountHelper1 (Count n a) b
44 Count n rep = '(n, rep)
47type CountHelper1 :: (Nat, Type -> Type) -> (Type -> Type) -> (Nat, Type -> Type)
48type family CountHelper1 tuple b where
49 CountHelper1 '(n, a) b = CountHelper2 a (Count n b)
52type CountHelper2 :: (Type -> Type) -> (Nat, Type -> Type) -> (Nat, Type -> Type)
53type family CountHelper2 a tuple where
54 CountHelper2 a '(n, b) = '(n, a :*: b)
57type Show :: Nat -> Symbol
58type Show n =
59 AppendSymbol "_" (AppendSymbol (Show' (Div n 10)) (ShowDigit (Mod n 10)))
62type Show' :: Nat -> Symbol
63type family Show' n where
64 Show' 0 = ""
65 Show' n = AppendSymbol (Show' (Div n 10)) (ShowDigit (Mod n 10))
68type ShowDigit :: Nat -> Symbol
69type family ShowDigit n where
70 ShowDigit 0 = "0"
71 ShowDigit 1 = "1"
72 ShowDigit 2 = "2"
73 ShowDigit 3 = "3"
74 ShowDigit 4 = "4"
75 ShowDigit 5 = "5"
76 ShowDigit 6 = "6"
77 ShowDigit 7 = "7"
78 ShowDigit 8 = "8"
79 ShowDigit 9 = "9"
82type Snd :: (a, b) -> b
83type family Snd tuple where
84 Snd '(_a, b) = b
87type GRecordable :: (Type -> Type) -> Constraint
88class GRecordable rep where
89 grecord :: rep x -> GRecord rep x
90 gunrecord :: GRecord rep x -> rep x
93instance GRecordable rep => GRecordable (M1 D meta rep) where
94 grecord (M1 a) = M1 (grecord a)
95 gunrecord (M1 a) = M1 (gunrecord a)
98instance (GRecordable l, GRecordable r) => GRecordable (l :+: r) where
99 grecord (L1 a) = L1 (grecord a)
100 grecord (R1 a) = R1 (grecord a)
101 gunrecord (L1 a) = L1 (gunrecord a)
102 gunrecord (R1 a) = R1 (gunrecord a)
105instance Countable 0 rep =>
106 GRecordable (M1 C ('MetaCons name fixity 'False) rep)
107 where
108 grecord (M1 a) = M1 (count @0 a)
109 gunrecord (M1 a) = M1 (uncount @0 a)
112instance {-# OVERLAPPABLE #-} GRecord rep ~ rep => GRecordable rep where
113 grecord = id
114 gunrecord = id
117type Countable :: Nat -> (Type -> Type) -> Constraint
118class Countable n rep where
119 count :: rep x -> Snd (Count n rep) x
120 uncount :: Snd (Count n rep) x -> rep x
123instance Countable n (M1 S ('MetaSel selector su ss ds) rep) where
124 count (M1 a) = M1 a
125 uncount (M1 a) = M1 a
128instance
129 ( Countable n a, Countable n' b
130 , '(n', a') ~ Count n a
131 , Snd (CountHelper2 a' (Count n' b)) ~ (a' :*: Snd (Count n' b))
132 )
133 => Countable n (a :*: b)
134 where
135 count (a :*: b) = count @n a :*: count @n' b
136 uncount (a :*: b) = uncount @n a :*: uncount @n' b
139instance {-# OVERLAPPABLE #-} Snd (Count n rep) ~ rep => Countable n rep where
140 count = id
141 uncount = id
144newtype Record a = Record
145 { unrecord :: a
146 }
149instance (Generic a, GRecordable (Rep a)) => Generic (Record a) where
150 type Rep (Record a) = GRecord (Rep a)
152 from (Record a) = grecord (from a)
153 to = Record . to . gunrecord