git.iko.soy/rel8
on da76712 help sign in
rel8/src/Rel8/Generic/Record.hs
155 lines 4.0 kB history raw
1{-# language AllowAmbiguousTypes #-}
2{-# language DataKinds #-}
3{-# language FlexibleContexts #-}
4{-# language FlexibleInstances #-}
5{-# language MultiParamTypeClasses #-}
6{-# language PolyKinds #-}
7{-# language ScopedTypeVariables #-}
8{-# language StandaloneKindSignatures #-}
9{-# language TypeApplications #-}
10{-# language TypeFamilies #-}
11{-# language TypeOperators #-}
12{-# language UndecidableInstances #-}
14module Rel8.Generic.Record
15 ( Record(..)
16 , GRecordable, GRecord, grecord, gunrecord
17 )
18where
20-- base
21import Data.Kind ( Constraint, Type )
22import GHC.Generics
23 ( Generic, Rep, from, to
24 , (:+:)( L1, R1 ), (:*:)( (:*:) ), M1( M1 )
25 , Meta( MetaCons, MetaSel ), D, C, S
26 )
27import GHC.TypeLits ( type (+), AppendSymbol, Div, Mod, Nat, Symbol )
28import Prelude hiding ( Show )
31type GRecord :: (Type -> Type) -> Type -> Type
32type family GRecord rep where
33 GRecord (M1 D meta rep) = M1 D meta (GRecord rep)
34 GRecord (l :+: r) = GRecord l :+: GRecord r
35 GRecord (M1 C ('MetaCons name fixity 'False) rep) =
36 M1 C ('MetaCons name fixity 'True) (Snd (Count 0 rep))
37 GRecord rep = rep
40type Count :: Nat -> (Type -> Type) -> (Nat, Type -> Type)
41type family Count n rep where
42 Count n (M1 S ('MetaSel _selector su ss ds) rep) =
43 '(n + 1, M1 S ('MetaSel ('Just (Show (n + 1))) su ss ds) rep)
44 Count n (a :*: b) = CountHelper1 (Count n a) b
45 Count n rep = '(n, rep)
48type CountHelper1 :: (Nat, Type -> Type) -> (Type -> Type) -> (Nat, Type -> Type)
49type family CountHelper1 tuple b where
50 CountHelper1 '(n, a) b = CountHelper2 a (Count n b)
53type CountHelper2 :: (Type -> Type) -> (Nat, Type -> Type) -> (Nat, Type -> Type)
54type family CountHelper2 a tuple where
55 CountHelper2 a '(n, b) = '(n, a :*: b)
58type Show :: Nat -> Symbol
59type Show n =
60 AppendSymbol "_" (AppendSymbol (Show' (Div n 10)) (ShowDigit (Mod n 10)))
63type Show' :: Nat -> Symbol
64type family Show' n where
65 Show' 0 = ""
66 Show' n = AppendSymbol (Show' (Div n 10)) (ShowDigit (Mod n 10))
69type ShowDigit :: Nat -> Symbol
70type family ShowDigit n where
71 ShowDigit 0 = "0"
72 ShowDigit 1 = "1"
73 ShowDigit 2 = "2"
74 ShowDigit 3 = "3"
75 ShowDigit 4 = "4"
76 ShowDigit 5 = "5"
77 ShowDigit 6 = "6"
78 ShowDigit 7 = "7"
79 ShowDigit 8 = "8"
80 ShowDigit 9 = "9"
83type Snd :: (a, b) -> b
84type family Snd tuple where
85 Snd '(_a, b) = b
88type GRecordable :: (Type -> Type) -> Constraint
89class GRecordable rep where
90 grecord :: rep x -> GRecord rep x
91 gunrecord :: GRecord rep x -> rep x
94instance GRecordable rep => GRecordable (M1 D meta rep) where
95 grecord (M1 a) = M1 (grecord a)
96 gunrecord (M1 a) = M1 (gunrecord a)
99instance (GRecordable l, GRecordable r) => GRecordable (l :+: r) where
100 grecord (L1 a) = L1 (grecord a)
101 grecord (R1 a) = R1 (grecord a)
102 gunrecord (L1 a) = L1 (gunrecord a)
103 gunrecord (R1 a) = R1 (gunrecord a)
106instance Countable 0 rep =>
107 GRecordable (M1 C ('MetaCons name fixity 'False) rep)
108 where
109 grecord (M1 a) = M1 (count @0 a)
110 gunrecord (M1 a) = M1 (uncount @0 a)
113instance {-# OVERLAPPABLE #-} GRecord rep ~ rep => GRecordable rep where
114 grecord = id
115 gunrecord = id
118type Countable :: Nat -> (Type -> Type) -> Constraint
119class Countable n rep where
120 count :: rep x -> Snd (Count n rep) x
121 uncount :: Snd (Count n rep) x -> rep x
124instance Countable n (M1 S ('MetaSel selector su ss ds) rep) where
125 count (M1 a) = M1 a
126 uncount (M1 a) = M1 a
129instance
130 ( Countable n a, Countable n' b
131 , '(n', a') ~ Count n a
132 , Snd (CountHelper2 a' (Count n' b)) ~ (a' :*: Snd (Count n' b))
133 )
134 => Countable n (a :*: b)
135 where
136 count (a :*: b) = count @n a :*: count @n' b
137 uncount (a :*: b) = uncount @n a :*: uncount @n' b
140instance {-# OVERLAPPABLE #-} Snd (Count n rep) ~ rep => Countable n rep where
141 count = id
142 uncount = id
145type Record :: Type -> Type
146newtype Record a = Record
147 { unrecord :: a
148 }
151instance (Generic a, GRecordable (Rep a)) => Generic (Record a) where
152 type Rep (Record a) = GRecord (Rep a)
154 from (Record a) = grecord (from a)
155 to = Record . to . gunrecord