git.iko.soy/rel8
on db148ff help sign in
rel8/src/Rel8/Generic/Construction.hs
453 lines 17 kB history raw
1{-# language AllowAmbiguousTypes #-}
2{-# language ConstraintKinds #-}
3{-# language DataKinds #-}
4{-# language FlexibleContexts #-}
5{-# language FlexibleInstances #-}
6{-# language LambdaCase #-}
7{-# language MultiParamTypeClasses #-}
8{-# language NamedFieldPuns #-}
9{-# language ScopedTypeVariables #-}
10{-# language StandaloneKindSignatures #-}
11{-# language TypeApplications #-}
12{-# language TypeFamilies #-}
13{-# language UndecidableInstances #-}
14{-# language ViewPatterns #-}
16module Rel8.Generic.Construction
17 ( GGConstructable
18 , GGConstruct, ggconstruct
19 , GGDeconstruct, ggdeconstruct
20 , GGInsert, gginsert
21 , GGName, ggname
22 , GGAggregate, ggaggregate
23 , GGAggregate', ggaggregate'
24 )
25where
27-- base
28import Data.Bifunctor ( first )
29import Data.Kind ( Constraint, Type )
30import Data.List.NonEmpty ( NonEmpty( (:|) ) )
31import Data.Type.Equality ( (:~:)( Refl ) )
32import Prelude
34-- rel8
35import Rel8.Aggregate ( Col( Aggregation ), Aggregate )
36import Rel8.Expr ( Col( DB ), Expr )
37import Rel8.Expr.Aggregate ( groupByExpr )
38import Rel8.Expr.Eq ( (==.) )
39import Rel8.Expr.Null ( nullify, snull, unsafeUnnullify )
40import Rel8.Expr.Serialize ( litExpr )
41import Rel8.FCF ( Compose, Eval, Exp )
42import Rel8.Generic.Construction.ADT
43 ( GConstructableADT
44 , GBuildADT, gbuildADT, gunbuildADT
45 , GConstructADT, gconstructADT, gdeconstructADT
46 , CorepConstructors, GConstructors, gcindex, gctabulate
47 , CorepFields, gfindex, gftabulate, gftraverse
48 )
49import Rel8.Generic.Construction.Record
50 ( GConstructable, GConstruct, gconstruct, gdeconstruct
51 , Corep, gindex, gtabulate, gtraverse
52 )
53import Rel8.Generic.Table ( GGColumns )
54import Rel8.Kind.Algebra
55 ( SAlgebra( SProduct, SSum )
56 , KnownAlgebra, algebraSing
57 )
58import qualified Rel8.Kind.Algebra as K
59import Rel8.Kind.Necessity ( SNecessity( SOptional, SRequired ) )
60import Rel8.Schema.Context.Nullify ( runTag )
61import Rel8.Schema.HTable ( HTable )
62import Rel8.Schema.HTable.Type ( HType( HType ) )
63import Rel8.Schema.Insert ( Col( OptionalInsert, RequiredInsert ), Insert )
64import qualified Rel8.Schema.Kind as K
65import Rel8.Schema.Name ( Col( NameCol ), Name( Name ) )
66import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
67import Rel8.Schema.Spec ( SSpec( SSpec, necessity, nullity, info ) )
68import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify )
69import Rel8.Schema.Result ( Result )
70import Rel8.Table
71 ( TTable, TColumns, TUnreify
72 , Table, fromColumns, toColumns, reify, unreify
73 )
74import Rel8.Table.Bool ( case_ )
75import Rel8.Type.Tag ( Tag )
77-- semigroupoids
78import Data.Functor.Apply ( Apply, MaybeApply( MaybeApply ), liftF2 )
81type GGConstructable :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
82type GGConstructable algebra rep =
83 ( KnownAlgebra algebra
84 , Eval (GGColumns algebra TColumns (Eval (rep (Reify Aggregate)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
85 , Eval (GGColumns algebra TColumns (Eval (rep (Reify Expr)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
86 , Eval (GGColumns algebra TColumns (Eval (rep (Reify Insert)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
87 , Eval (GGColumns algebra TColumns (Eval (rep (Reify Name)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
88 , HTable (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))))
89 , GGConstructable' algebra rep
90 )
93type GGConstructable' :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
94type family GGConstructable' algebra rep where
95 GGConstructable' 'K.Product rep =
96 ( Corep (Compose Aggregate TUnreify) (Eval (rep (Reify Expr)))
97 , Corep TUnreify (Eval (rep (Reify Aggregate)))
98 , Corep TUnreify (Eval (rep (Reify Expr)))
99 , Corep TUnreify (Eval (rep (Reify Insert)))
100 , Corep TUnreify (Eval (rep (Reify Name)))
101 , GConstructable (TTable (Reify Aggregate)) TColumns TUnreify (Col (Reify Aggregate)) (Eval (rep (Reify Aggregate)))
102 , GConstructable (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (Eval (rep (Reify Expr)))
103 , GConstructable (TTable (Reify Insert)) TColumns TUnreify (Col (Reify Insert)) (Eval (rep (Reify Insert)))
104 , GConstructable (TTable (Reify Name)) TColumns TUnreify (Col (Reify Name)) (Eval (rep (Reify Name)))
105 )
106 GGConstructable' 'K.Sum rep =
107 ( CorepConstructors TUnreify (Eval (rep (Reify Expr)))
108 , CorepConstructors TUnreify (Eval (rep (Reify Insert)))
109 , CorepFields (Compose Aggregate TUnreify) (Eval (rep (Reify Expr)))
110 , CorepFields TUnreify (Eval (rep (Reify Aggregate)))
111 , CorepFields TUnreify (Eval (rep (Reify Expr)))
112 , CorepFields TUnreify (Eval (rep (Reify Name)))
113 , Functor (GConstructors TUnreify (Eval (rep (Reify Expr))))
114 , Functor (GConstructors TUnreify (Eval (rep (Reify Insert))))
115 , GConstructableADT (TTable (Reify Aggregate)) TColumns TUnreify (Col (Reify Aggregate)) (Eval (rep (Reify Aggregate)))
116 , GConstructableADT (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (Eval (rep (Reify Expr)))
117 , GConstructableADT (TTable (Reify Insert)) TColumns TUnreify (Col (Reify Insert)) (Eval (rep (Reify Insert)))
118 , GConstructableADT (TTable (Reify Name)) TColumns TUnreify (Col (Reify Name)) (Eval (rep (Reify Name)))
119 )
122type GGConstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
123type family GGConstruct algebra rep a where
124 GGConstruct 'K.Product rep a = GConstruct TUnreify (Eval (rep (Reify Expr))) a
125 GGConstruct 'K.Sum rep a =
126 -- Ideally this would be as follows, but GHC complains about "illegal polymorphic type"
127 -- (forall r. GConstructADT TUnreify (Eval (rep (Reify Expr))) r r) -> a
128 GConstructADT TUnreify (Eval (rep (Reify Expr))) a a -> a
131ggconstruct :: forall algebra rep a. GGConstructable algebra rep
132 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr) -> a)
133 -> GGConstruct algebra rep a
134ggconstruct gfromColumns = case algebraSing @algebra of
135 SProduct ->
136 gtabulate @TUnreify @(Eval (rep (Reify Expr))) @a $
137 gfromColumns .
138 hunreify .
139 gconstruct
140 @(TTable (Reify Expr))
141 @TColumns
142 @TUnreify
143 @(Col (Reify Expr))
144 @(Eval (rep (Reify Expr)))
145 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
146 SSum -> \f ->
147 gcindex @TUnreify @(Eval (rep (Reify Expr))) @a f $
148 fmap (gfromColumns . hunreify) $
149 gconstructADT
150 @(TTable (Reify Expr))
151 @TColumns
152 @TUnreify
153 @(Col (Reify Expr))
154 @(Eval (rep (Reify Expr)))
155 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
156 (\SSpec {info} -> Reify (DB (snull info)))
157 (\SSpec {nullity} -> case nullity of
158 Null -> id
159 NotNull -> \(Reify (DB a)) -> Reify (DB (nullify a)))
160 (HType . Reify . DB . litExpr)
163type GGDeconstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type -> Type
164type family GGDeconstruct algebra rep a r where
165 GGDeconstruct 'K.Product rep a r =
166 GConstruct TUnreify (Eval (rep (Reify Expr))) r -> a -> r
167 GGDeconstruct 'K.Sum rep a r =
168 GConstructADT TUnreify (Eval (rep (Reify Expr))) r (a -> r)
171ggdeconstruct :: forall algebra rep a r. (GGConstructable algebra rep, Table Expr r)
172 => (a -> Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr))
173 -> GGDeconstruct algebra rep a r
174ggdeconstruct gtoColumns = case algebraSing @algebra of
175 SProduct -> \build ->
176 gindex @TUnreify @(Eval (rep (Reify Expr))) @r build .
177 gdeconstruct
178 @(TTable (Reify Expr))
179 @TColumns
180 @TUnreify
181 @(Col (Reify Expr))
182 @(Eval (rep (Reify Expr)))
183 (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns) .
184 hreify .
185 gtoColumns
186 SSum ->
187 gctabulate @TUnreify @(Eval (rep (Reify Expr))) @r @(a -> r) $ \constructors as ->
188 let
189 (HType (Reify (DB tag)), cases) =
190 gdeconstructADT
191 @(TTable (Reify Expr))
192 @TColumns
193 @TUnreify
194 @(Col (Reify Expr))
195 @(Eval (rep (Reify Expr)))
196 (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns)
197 (\SSpec {nullity} -> case nullity of
198 Null -> id
199 NotNull -> \(Reify (DB a)) -> Reify (DB (unsafeUnnullify a)))
200 constructors $
201 hreify $
202 gtoColumns as
203 in
204 case cases of
205 ((_, r) :| (map (first ((tag ==.) . litExpr)) -> cases')) ->
206 case_ cases' r
209type GGInsert :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
210type family GGInsert algebra rep a where
211 GGInsert 'K.Product rep a = GConstruct TUnreify (Eval (rep (Reify Insert))) a
212 GGInsert 'K.Sum rep a =
213 -- Ideally this would be as follows, but GHC complains about "illegal polymorphic type"
214 -- (forall r. GConstructADT TUnreify (Eval (rep (Reify Insert))) r r) -> a
215 GConstructADT TUnreify (Eval (rep (Reify Insert))) a a -> a
218gginsert :: forall algebra rep a. GGConstructable algebra rep
219 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Insert) -> a)
220 -> GGInsert algebra rep a
221gginsert gfromColumns = case algebraSing @algebra of
222 SProduct ->
223 gtabulate @TUnreify @(Eval (rep (Reify Insert))) @a $
224 gfromColumns .
225 hunreify .
226 gconstruct
227 @(TTable (Reify Insert))
228 @TColumns
229 @TUnreify
230 @(Col (Reify Insert))
231 @(Eval (rep (Reify Insert)))
232 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
233 SSum -> \f ->
234 gcindex @TUnreify @(Eval (rep (Reify Insert))) @a f $
235 fmap (gfromColumns . hunreify) $
236 gconstructADT
237 @(TTable (Reify Insert))
238 @TColumns
239 @TUnreify
240 @(Col (Reify Insert))
241 @(Eval (rep (Reify Insert)))
242 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
243 (\SSpec {necessity, info} -> Reify $ case necessity of
244 SRequired -> RequiredInsert (snull info)
245 SOptional -> OptionalInsert (Just (snull info)))
246 (\SSpec {nullity} -> case nullity of
247 Null -> id
248 NotNull -> \case
249 Reify (RequiredInsert a) -> Reify (RequiredInsert (nullify a))
250 Reify (OptionalInsert a) -> Reify (OptionalInsert (nullify <$> a)))
251 (HType . Reify . RequiredInsert . litExpr)
254type GGName :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
255type family GGName algebra rep a where
256 GGName 'K.Product rep a = GConstruct TUnreify (Eval (rep (Reify Name))) a
257 GGName 'K.Sum rep a = Name Tag -> GBuildADT TUnreify (Eval (rep (Reify Name))) a
260ggname :: forall algebra rep a. GGConstructable algebra rep
261 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Name) -> a)
262 -> GGName algebra rep a
263ggname gfromColumns = case algebraSing @algebra of
264 SProduct ->
265 gtabulate @TUnreify @(Eval (rep (Reify Name))) @a $
266 gfromColumns .
267 hunreify .
268 gconstruct
269 @(TTable (Reify Name))
270 @TColumns
271 @TUnreify
272 @(Col (Reify Name))
273 @(Eval (rep (Reify Name)))
274 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
275 SSum -> \tag ->
276 gftabulate @TUnreify @(Eval (rep (Reify Name))) @a $
277 gfromColumns .
278 hunreify .
279 gbuildADT
280 @(TTable (Reify Name))
281 @TColumns
282 @TUnreify
283 @(Col (Reify Name))
284 @(Eval (rep (Reify Name)))
285 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
286 (\_ _ (Reify (NameCol a)) -> Reify (NameCol a))
287 (HType ((\(Name a) -> Reify (NameCol a)) tag))
290type GGAggregate :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
291type family GGAggregate algebra rep r where
292 GGAggregate 'K.Product rep r =
293 GConstruct (Compose Aggregate TUnreify) (Eval (rep (Reify Expr))) r ->
294 GConstruct TUnreify (Eval (rep (Reify Expr))) r
295 GGAggregate 'K.Sum rep r =
296 GBuildADT (Compose Aggregate TUnreify) (Eval (rep (Reify Expr))) r ->
297 GBuildADT TUnreify (Eval (rep (Reify Expr))) r
300ggaggregate :: forall algebra rep a. GGConstructable algebra rep
301 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr) -> a)
302 -> (a -> Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr))
303 -> GGAggregate algebra rep (Aggregate a) -> a -> Aggregate a
304ggaggregate gfromColumns gtoColumns agg es = case algebraSing @algebra of
305 SProduct -> flip f exprs $
306 fmap
307 ( gfromColumns
308 . hunreify
309 . gconstruct
310 @(TTable (Reify Expr))
311 @TColumns
312 @TUnreify
313 @(Col (Reify Expr))
314 @(Eval (rep (Reify Expr)))
315 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
316 ) .
317 liftF½ .
318 gtraverse @TUnreify @(Eval (rep (Reify Expr))) @_ @Aggregate (MaybeApply . Left)
319 where
320 f =
321 gindex @TUnreify @(Eval (rep (Reify Expr))) @(Aggregate a) .
322 agg .
323 gtabulate @(Compose Aggregate TUnreify) @(Eval (rep (Reify Expr))) @(Aggregate a)
324 exprs =
325 gdeconstruct
326 @(TTable (Reify Expr))
327 @TColumns
328 @TUnreify
329 @(Col (Reify Expr))
330 @(Eval (rep (Reify Expr)))
331 (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns) $
332 hreify $
333 gtoColumns es
334 SSum -> flip f exprs $
335 liftF1½
336 (\tag' ->
337 gfromColumns .
338 hunreify .
339 gbuildADT
340 @(TTable (Reify Expr))
341 @TColumns
342 @TUnreify
343 @(Col (Reify Expr))
344 @(Eval (rep (Reify Expr)))
345 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
346 (\tag'' SSpec {nullity} (Reify (DB a)) ->
347 Reify $ DB $ runTag nullity (tag ==. litExpr tag'') a)
348 (HType (Reify (DB tag'))))
349 (groupByExpr tag) .
350 gftraverse @TUnreify @(Eval (rep (Reify Expr))) @_ @Aggregate (MaybeApply . Left)
351 where
352 f =
353 gfindex @TUnreify @(Eval (rep (Reify Expr))) @(Aggregate a) .
354 agg .
355 gftabulate @(Compose Aggregate TUnreify) @(Eval (rep (Reify Expr))) @(Aggregate a)
356 (HType (Reify (DB tag)), exprs) =
357 gunbuildADT
358 @(TTable (Reify Expr))
359 @TColumns
360 @TUnreify
361 @(Col (Reify Expr))
362 @(Eval (rep (Reify Expr)))
363 (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns)
364 (\SSpec {nullity} -> case nullity of
365 Null -> id
366 NotNull -> \(Reify (DB a)) -> Reify (DB (unsafeUnnullify a))) $
367 hreify $
368 gtoColumns es
371type GGAggregate' :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
372type family GGAggregate' algebra rep r where
373 GGAggregate' 'K.Product rep r =
374 GConstruct TUnreify (Eval (rep (Reify Aggregate))) r ->
375 GConstruct TUnreify (Eval (rep (Reify Expr))) r
376 GGAggregate' 'K.Sum rep r =
377 GBuildADT TUnreify (Eval (rep (Reify Aggregate))) r ->
378 GBuildADT TUnreify (Eval (rep (Reify Expr))) r
381ggaggregate' :: forall algebra rep exprs agg. GGConstructable algebra rep
382 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Aggregate) -> agg)
383 -> (exprs -> Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr))
384 -> GGAggregate' algebra rep agg -> exprs -> agg
385ggaggregate' gfromColumns gtoColumns agg es = case algebraSing @algebra of
386 SProduct -> flip f exprs $
387 gfromColumns .
388 hunreify .
389 gconstruct
390 @(TTable (Reify Aggregate))
391 @TColumns
392 @TUnreify
393 @(Col (Reify Aggregate))
394 @(Eval (rep (Reify Aggregate)))
395 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
396 where
397 f =
398 gindex @TUnreify @(Eval (rep (Reify Expr))) @agg .
399 agg .
400 gtabulate @TUnreify @(Eval (rep (Reify Aggregate))) @agg
401 exprs =
402 gdeconstruct
403 @(TTable (Reify Expr))
404 @TColumns
405 @TUnreify
406 @(Col (Reify Expr))
407 @(Eval (rep (Reify Expr)))
408 (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns) $
409 hreify $
410 gtoColumns es
411 SSum -> flip f exprs $
412 gfromColumns .
413 hunreify .
414 gbuildADT
415 @(TTable (Reify Aggregate))
416 @TColumns
417 @TUnreify
418 @(Col (Reify Aggregate))
419 @(Eval (rep (Reify Aggregate)))
420 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
421 (\tag' SSpec {nullity} (Reify (Aggregation a)) ->
422 Reify $ Aggregation $ runTag nullity (tag ==. litExpr tag') <$> a)
423 (HType (Reify (Aggregation (groupByExpr tag))))
424 where
425 f =
426 gfindex @TUnreify @(Eval (rep (Reify Expr))) @agg .
427 agg .
428 gftabulate @TUnreify @(Eval (rep (Reify Aggregate))) @agg
429 (HType (Reify (DB tag)), exprs) =
430 gunbuildADT
431 @(TTable (Reify Expr))
432 @TColumns
433 @TUnreify
434 @(Col (Reify Expr))
435 @(Eval (rep (Reify Expr)))
436 (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns)
437 (\SSpec {nullity} -> case nullity of
438 Null -> id
439 NotNull -> \(Reify (DB a)) -> Reify (DB (unsafeUnnullify a))) $
440 hreify $
441 gtoColumns es
444liftF½ :: MaybeApply Aggregate a -> Aggregate a
445liftF½ (MaybeApply ma) = case ma of
446 Left a -> a
447 Right a -> a <$ groupByExpr (litExpr False)
450liftF1½ :: Apply v => (a -> b -> c) -> v a -> MaybeApply v b -> v c
451liftF1½ f a (MaybeApply eb) = case eb of
452 Left b -> liftF2 f a b
453 Right b -> fmap (`f` b) a