git.iko.soy/rel8
on 4bc16d3 help sign in
rel8/src/Rel8/Generic/Rel8able.hs
293 lines 8.9 kB history raw
1{-# language AllowAmbiguousTypes #-}
2{-# language ConstraintKinds #-}
3{-# language DataKinds #-}
4{-# language DefaultSignatures #-}
5{-# language FlexibleContexts #-}
6{-# language FlexibleInstances #-}
7{-# language MultiParamTypeClasses #-}
8{-# language ScopedTypeVariables #-}
9{-# language StandaloneKindSignatures #-}
10{-# language TypeApplications #-}
11{-# language TypeFamilies #-}
12{-# language UndecidableInstances #-}
14module Rel8.Generic.Rel8able
15 ( KRel8able, Rel8able
16 , Algebra
17 , GRep
18 , GColumns, GContext, gfromColumns, gtoColumns
19 , GColumnsADT, gfromColumnsADT, gtoColumnsADT
20 , greify, gunreify
21 )
22where
24-- base
25import Data.Kind ( Constraint, Type )
26import Data.Proxy ( Proxy( Proxy ) )
27import Data.Type.Equality ( (:~:)( Refl ) )
28import GHC.Generics ( Generic, Rep, from, to )
29import Prelude
31-- rel8
32import Rel8.Kind.Context ( Reifiable )
33import Rel8.FCF ( Eval, Exp )
34import Rel8.Generic.Map ( GMap, GMappable, gmap, gunmap )
35import Rel8.Generic.Record ( Record(..) )
36import Rel8.Generic.Table
37 ( GGTable, GGColumns, GGContext, ggfromColumns, ggtoColumns
38 , GAlgebra
39 )
40import qualified Rel8.Generic.Table.ADT as G
41import Rel8.Kind.Algebra
42 ( SAlgebra( SProduct, SSum )
43 , KnownAlgebra, algebraSing
44 )
45import qualified Rel8.Kind.Algebra as K ( Algebra(..) )
46import Rel8.Schema.Context ( Col )
47import Rel8.Schema.Context.Label ( Labelable )
48import Rel8.Schema.HTable ( HTable )
49import qualified Rel8.Schema.Kind as K
50import Rel8.Schema.Name ( Name )
51import Rel8.Schema.Reify ( Col( Reify ), Reify, UnwrapReify )
52import Rel8.Schema.Result ( Result )
53import Rel8.Table
54 ( fromColumns, toColumns, reify, unreify
55 , TTable, TColumns, TContext, TUnreify
56 )
59type KRel8able :: Type
60type KRel8able = K.Rel8able
63-- | This type class allows you to define custom 'Table's using higher-kinded
64-- data types. Higher-kinded data types are data types of the pattern:
65--
66-- @
67-- data MyType f =
68-- MyType { field1 :: Column f T1 OR HK1 f
69-- , field2 :: Column f T2 OR HK2 f
70-- , ...
71-- , fieldN :: Column f Tn OR HKn f
72-- }
73-- @
74--
75-- where @Tn@ is any Haskell type, and @HKn@ is any higher-kinded type.
76--
77-- That is, higher-kinded data are records where all fields in the record are
78-- all either of the type @Column f T@ (for any @T@), or are themselves
79-- higher-kinded data:
80--
81-- [Nested]
82--
83-- @
84-- data Nested f =
85-- Nested { nested1 :: MyType f
86-- , nested2 :: MyType f
87-- }
88-- @
89--
90-- The @Rel8able@ type class is used to give us a special mapping operation
91-- that lets us change the type parameter @f@.
92--
93-- [Supplying @Rel8able@ instances]
94--
95-- This type class should be derived generically for all table types in your
96-- project. To do this, enable the @DeriveAnyType@ and @DeriveGeneric@ language
97-- extensions:
98--
99-- @
100-- \{\-\# LANGUAGE DeriveAnyClass, DeriveGeneric #-\}
101--
102-- data MyType f = MyType { fieldA :: Column f T }
103-- deriving ( GHC.Generics.Generic, Rel8able )
104-- @
105type Rel8able :: K.Rel8able -> Constraint
106class
107 ( HTable (GColumns t)
108 , HTable (GColumnsADT t)
109 , GContext t Result ~ Result
110 )
111 => Rel8able t
112 where
113 type Algebra t :: K.Algebra
115 type GRep t (context :: K.Context) :: Type -> Type
117 type GColumns t :: K.HTable
119 type GContext t (context :: K.Context) :: K.Context
121 gfromColumns :: (Labelable context, Reifiable context, GContext t context ~ context)
122 => GColumns t (Col (Reify context)) -> t (Reify context)
124 gtoColumns :: (Labelable context, Reifiable context, GContext t context ~ context)
125 => t (Reify context) -> GColumns t (Col (Reify context))
127 gfromColumnsADT :: GColumnsADT t (Col (Reify Result)) -> t (Reify Result)
129 gtoColumnsADT :: t (Reify Result) -> GColumnsADT t (Col (Reify Result))
131 greify :: (Labelable context, Reifiable context)
132 => t context -> t (Reify context)
134 gunreify :: (Labelable context, Reifiable context)
135 => t (Reify context) -> t context
137 type Algebra t = GAlgebra (GRep t (Reify Name))
139 type GRep t context = Rep (Record (t context))
141 type GColumns t = Eval (GGColumns (Algebra t) TColumns (GRep t (Reify Name)))
143 type GContext t context =
144 Eval (GGContext (Algebra t) TUnreifyContext (GRep t (Reify context)))
146 default gfromColumns :: forall context.
147 ( Generic (Record (t (Reify context)))
148 , GRep t (Reify context) ~ Rep (Record (t (Reify context)))
149 , KnownAlgebra (Algebra t)
150 , Eval (GGTable (Algebra t) (TTable (Reify context)) TColumns (Col (Reify context)) (GRep t (Reify context)))
151 , Eval (GGColumns (Algebra t) TColumns (GRep t (Reify context))) ~ GColumns t
152 , Constraints t context
153 )
154 => GColumns t (Col (Reify context)) -> t (Reify context)
155 gfromColumns =
156 unrecord .
157 to .
158 ggfromColumns
159 @(Algebra t)
160 @(TTable (Reify context))
161 @TColumns
162 @TContext
163 (fromContext @t @context)
164 (toContext @t @context)
165 fromColumns
167 default gtoColumns :: forall context.
168 ( Generic (Record (t (Reify context)))
169 , GRep t (Reify context) ~ Rep (Record (t (Reify context)))
170 , KnownAlgebra (Algebra t)
171 , Eval (GGTable (Algebra t) (TTable (Reify context)) TColumns (Col (Reify context)) (GRep t (Reify context)))
172 , Eval (GGColumns (Algebra t) TColumns (GRep t (Reify context))) ~ GColumns t
173 , Constraints t context
174 )
175 => t (Reify context) -> GColumns t (Col (Reify context))
176 gtoColumns =
177 ggtoColumns
178 @(Algebra t)
179 @(TTable (Reify context))
180 @TColumns
181 @TContext
182 (fromContext @t @context)
183 (toContext @t @context)
184 toColumns .
185 from .
186 Record
188 default gfromColumnsADT ::
189 ( Generic (Record (t (Reify Result)))
190 , GRep t (Reify Result) ~ Rep (Record (t (Reify Result)))
191 , G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRep t (Reify Result))
192 , G.GColumnsADT TColumns (GRep t (Reify Result)) ~ GColumnsADT t
193 )
194 => GColumnsADT t (Col (Reify Result)) -> t (Reify Result)
195 gfromColumnsADT =
196 unrecord .
197 to .
198 G.gfromColumnsADT
199 @(TTable (Reify Result))
200 @TColumns
201 (\(Reify a) -> a)
202 Reify
203 fromColumns
205 default gtoColumnsADT ::
206 ( Generic (Record (t (Reify Result)))
207 , GRep t (Reify Result) ~ Rep (Record (t (Reify Result)))
208 , G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRep t (Reify Result))
209 , G.GColumnsADT TColumns (GRep t (Reify Result)) ~ GColumnsADT t
210 )
211 => t (Reify Result) -> GColumnsADT t (Col (Reify Result))
212 gtoColumnsADT =
213 G.gtoColumnsADT
214 @(TTable (Reify Result))
215 @TColumns
216 (\(Reify a) -> a)
217 Reify
218 toColumns .
219 from .
220 Record
222 default greify :: forall context.
223 ( Generic (Record (t context))
224 , GRep t context ~ Rep (Record (t context))
225 , Generic (Record (t (Reify context)))
226 , GRep t (Reify context) ~ Rep (Record (t (Reify context)))
227 , GMappable (TTable (Reify context)) (GRep t (Reify context))
228 , GRep t context ~ GMap TUnreify (GRep t (Reify context))
229 )
230 => t context -> t (Reify context)
231 greify =
232 unrecord .
233 to .
234 gunmap @(TTable (Reify context)) (Proxy @TUnreify) (reify Refl) .
235 from .
236 Record
238 default gunreify :: forall context.
239 ( Generic (Record (t context))
240 , GRep t context ~ Rep (Record (t context))
241 , Generic (Record (t (Reify context)))
242 , GRep t (Reify context) ~ Rep (Record (t (Reify context)))
243 , GMappable (TTable (Reify context)) (GRep t (Reify context))
244 , GRep t context ~ GMap TUnreify (GRep t (Reify context))
245 )
246 => t (Reify context) -> t context
247 gunreify =
248 unrecord .
249 to .
250 gmap @(TTable (Reify context)) (Proxy @TUnreify) (unreify Refl) .
251 from .
252 Record
255type GColumnsADT t = G.GColumnsADT TColumns (GRep t (Reify Name))
258data TUnreifyContext :: Type -> Exp K.Context
259type instance Eval (TUnreifyContext a) = UnwrapReify (Eval (TContext a))
262type Constraints :: K.Rel8able -> K.Context -> Constraint
263type Constraints t context = Constraints' (Algebra t) t context
266type Constraints' :: K.Algebra -> K.Rel8able -> K.Context -> Constraint
267type family Constraints' algebra t context where
268 Constraints' 'K.Product t context =
269 Eval (GGContext 'K.Product TContext (GRep t (Reify context))) ~
270 Reify context
271 Constraints' 'K.Sum _ context = context ~ Result
274fromContext :: forall t context spec.
275 ( KnownAlgebra (Algebra t)
276 , Constraints t context
277 )
278 => Col (Reify context) spec
279 -> Col (Eval (GGContext (Algebra t) TContext (GRep t (Reify context)))) spec
280fromContext = case algebraSing @(Algebra t) of
281 SProduct -> id
282 SSum -> \(Reify a) -> a
285toContext :: forall t context spec.
286 ( KnownAlgebra (Algebra t)
287 , Constraints t context
288 )
289 => Col (Eval (GGContext (Algebra t) TContext (GRep t (Reify context)))) spec
290 -> Col (Reify context) spec
291toContext = case algebraSing @(Algebra t) of
292 SProduct -> id
293 SSum -> Reify