git.iko.soy/rel8
on master help sign in
Generalize constructor functions in Rel8.Table.ADT to Rel8.Generic.Construction
commit7a526b6ec11d104d7a724442f27d742441509a38 authorShane O'Brien <shane.obrien@circuithub.com> dateWed 5 May 2021, 01:27 (6 years ago) parent9fd885f
4 files changed+544−251
compare with master
unifiedsplit
rel8.cabal+1 src/Rel8/Aggregate/Legacy.hs+25−2 src/Rel8/Generic/Construction.hs+482 src/Rel8/Table/ADT.hs+36−249
rel8.cabal+1
@@ -77,6 +77,7 @@ library
7777 Rel8.Kind.Labels
7878 Rel8.Kind.Necessity
7979
80+ Rel8.Generic.Construction
8081 Rel8.Generic.Construction.ADT
8182 Rel8.Generic.Construction.Record
8283 Rel8.Generic.Map
src/Rel8/Aggregate/Legacy.hs+25−2
@@ -1,5 +1,9 @@
1+{-# language AllowAmbiguousTypes #-}
2+{-# language DataKinds #-}
13{-# language FlexibleContexts #-}
4+{-# language RankNTypes #-}
25{-# language ScopedTypeVariables #-}
6+{-# language StandaloneKindSignatures #-}
37{-# language TypeApplications #-}
48{-# language TypeFamilies #-}
59{-# language ViewPatterns #-}
@@ -11,26 +15,34 @@ module Rel8.Aggregate.Legacy
1115 , groupBy
1216 , listAgg
1317 , nonEmptyAgg
18+
19+ , AggregateADT
20+ , aggregateADT
1421 )
1522where
1623
1724-- base
1825import Data.Functor.Identity ( Identity( Identity ) )
26+import Data.Kind ( Type )
1927import Prelude
2028
2129-- opaleye
2230import qualified Opaleye.Aggregate as Opaleye
2331
2432-- rel8
25−import Rel8.Aggregate ( Aggregates, Col(..) )
26−import Rel8.Expr ( Col(..) )
33+import Rel8.Aggregate ( Aggregate, Aggregates, Col(..) )
34+import Rel8.Expr ( Col(..), Expr )
2735import Rel8.Expr.Aggregate ( groupByExpr, listAggExpr, nonEmptyAggExpr )
36+import Rel8.Generic.Construction ( GGAggregate', ggaggregate' )
37+import Rel8.Kind.Algebra ( Algebra( Sum ) )
2838import Rel8.Query ( Query )
2939import Rel8.Query.Opaleye ( mapOpaleye )
3040import Rel8.Schema.Dict ( Dict( Dict ) )
3141import Rel8.Schema.HTable ( htabulate, hfield )
3242import Rel8.Schema.HTable.Vectorize ( hvectorize )
43+import Rel8.Schema.Kind ( Rel8able )
3344import Rel8.Table ( toColumns, fromColumns )
45+import Rel8.Table.ADT ( ConstructableADT, ADT( ADT ), ADTRep )
3446import Rel8.Table.Eq ( EqTable, eqTable )
3547import Rel8.Table.List ( ListTable )
3648import Rel8.Table.NonEmpty ( NonEmptyTable )
@@ -90,3 +102,14 @@ nonEmptyAgg (toColumns -> exprs) = fromColumns $
90102 hvectorize
91103 (\_ (Identity (DB a)) -> Aggregation $ nonEmptyAggExpr a)
92104 (pure exprs)
105+
106+
107+type AggregateADT :: Rel8able -> Type
108+type AggregateADT t = forall r. GGAggregate' 'Sum (ADTRep t) r
109+
110+
111+aggregateADT :: forall t. ConstructableADT t
112+ => AggregateADT t -> ADT t Expr -> ADT t Aggregate
113+aggregateADT f =
114+ ggaggregate' @'Sum @(ADTRep t) @(ADT t Expr) @(ADT t Aggregate) ADT (\(ADT a) -> a)
115+ (f @(ADT t Aggregate))
src/Rel8/Generic/Construction.hsnew file+482
@@ -0,0 +1,482 @@
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 #-}
15+
16+module Rel8.Generic.Construction
17+ ( GGConstructable
18+ , GGConstruct, ggconstruct
19+ , GGDeconstruct, ggdeconstruct
20+ , GGInsert, gginsert
21+ , GGName, ggname
22+ , GGAggregate, ggaggregate
23+ , GGAggregate', ggaggregate'
24+ )
25+where
26+
27+-- base
28+import Data.Bifunctor ( first )
29+import Data.Kind ( Constraint, Type )
30+import Data.List.NonEmpty ( NonEmpty( (:|) ) )
31+import Data.Type.Equality ( (:~:)( Refl ) )
32+import Prelude
33+
34+-- rel8
35+import Rel8.Aggregate ( Col( Aggregation ), Aggregate )
36+import Rel8.Expr ( Col( DB ), Expr )
37+import Rel8.Expr.Aggregate ( groupByExpr )
38+import Rel8.Expr.Eq ( (==.) )
39+import Rel8.Expr.Null ( nullify, snull, unsafeUnnullify )
40+import Rel8.Expr.Serialize ( litExpr )
41+import Rel8.FCF ( Compose, Eval, Exp )
42+import 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+ )
49+import Rel8.Generic.Construction.Record
50+ ( GConstructable, GConstruct, gconstruct, gdeconstruct
51+ , Corep, gindex, gtabulate, gtraverse
52+ )
53+import Rel8.Generic.Table ( GGColumns )
54+import Rel8.Kind.Algebra
55+ ( SAlgebra( SProduct, SSum )
56+ , KnownAlgebra, algebraSing
57+ )
58+import qualified Rel8.Kind.Algebra as K
59+import Rel8.Kind.Necessity ( SNecessity( SOptional, SRequired ) )
60+import Rel8.Schema.Context.Nullify ( runTag )
61+import Rel8.Schema.HTable ( HTable )
62+import Rel8.Schema.HTable.Type ( HType( HType ) )
63+import Rel8.Schema.Insert ( Col( OptionalInsert, RequiredInsert ), Insert )
64+import qualified Rel8.Schema.Kind as K
65+import Rel8.Schema.Name ( Col( NameCol ), Name( Name ) )
66+import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
67+import Rel8.Schema.Spec ( SSpec( SSpec, necessity, nullity, info ) )
68+import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify )
69+import Rel8.Schema.Result ( Result )
70+import Rel8.Table
71+ ( TTable, TColumns, TUnreify
72+ , Table, fromColumns, toColumns, reify, unreify
73+ )
74+import Rel8.Table.Bool ( case_ )
75+import Rel8.Type.Tag ( Tag )
76+
77+-- semigroupoids
78+import Data.Functor.Apply ( Apply, MaybeApply( MaybeApply ), liftF2 )
79+
80+
81+type GGConstructable :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
82+type 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+ )
91+
92+
93+type GGConstructable' :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
94+type 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+ )
120+
121+
122+type GGConstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
123+type 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
129+
130+
131+ggconstruct :: forall algebra rep a. GGConstructable algebra rep
132+ => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr) -> a)
133+ -> GGConstruct algebra rep a
134+ggconstruct 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)
161+
162+
163+type GGDeconstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type -> Type
164+type 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)
169+
170+
171+ggdeconstruct :: 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
174+ggdeconstruct 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
207+
208+
209+type GGInsert :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
210+type 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
216+
217+
218+gginsert :: forall algebra rep a. GGConstructable algebra rep
219+ => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Insert) -> a)
220+ -> GGInsert algebra rep a
221+gginsert 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)
252+
253+
254+type GGName :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
255+type 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
258+
259+
260+ggname :: forall algebra rep a. GGConstructable algebra rep
261+ => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Name) -> a)
262+ -> GGName algebra rep a
263+ggname 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))
288+
289+
290+type GGAggregate :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
291+type family GGAggregate algebra rep r where
292+ GGAggregate 'K.Product rep r =
293+ GConstruct TUnreify (Eval (rep (Reify Expr)))
294+ (GConstruct (Compose Aggregate TUnreify) (Eval (rep (Reify Expr))) r -> r)
295+ GGAggregate 'K.Sum rep r =
296+ GBuildADT TUnreify (Eval (rep (Reify Expr)))
297+ (GBuildADT (Compose Aggregate TUnreify) (Eval (rep (Reify Expr))) r -> r)
298+
299+
300+ggaggregate :: 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
304+ggaggregate gfromColumns gtoColumns agg es = case algebraSing @algebra of
305+ SProduct -> f $
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
322+ @TUnreify
323+ @(Eval (rep (Reify Expr)))
324+ @(GConstruct (Compose Aggregate TUnreify) (Eval (rep (Reify Expr))) (Aggregate a) -> Aggregate a)
325+ agg
326+ exprs .
327+ gtabulate
328+ @(Compose Aggregate TUnreify)
329+ @(Eval (rep (Reify Expr)))
330+ @(Aggregate a)
331+ exprs =
332+ gdeconstruct
333+ @(TTable (Reify Expr))
334+ @TColumns
335+ @TUnreify
336+ @(Col (Reify Expr))
337+ @(Eval (rep (Reify Expr)))
338+ (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns) $
339+ hreify $
340+ gtoColumns es
341+
342+ SSum -> f exprs $
343+ liftF1½
344+ (\tag' ->
345+ gfromColumns .
346+ hunreify .
347+ gbuildADT
348+ @(TTable (Reify Expr))
349+ @TColumns
350+ @TUnreify
351+ @(Col (Reify Expr))
352+ @(Eval (rep (Reify Expr)))
353+ (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
354+ (\tag'' SSpec {nullity} (Reify (DB a)) ->
355+ Reify $ DB $ runTag nullity (tag ==. litExpr tag'') a)
356+ (HType (Reify (DB tag'))))
357+ (groupByExpr tag) .
358+ gftraverse @TUnreify @(Eval (rep (Reify Expr))) @_ @Aggregate (MaybeApply . Left)
359+ where
360+ f e =
361+ gfindex
362+ @TUnreify
363+ @(Eval (rep (Reify Expr)))
364+ @(GBuildADT (Compose Aggregate TUnreify) (Eval (rep (Reify Expr))) (Aggregate a) -> Aggregate a)
365+ agg
366+ e .
367+ gftabulate
368+ @(Compose Aggregate TUnreify)
369+ @(Eval (rep (Reify Expr)))
370+ @(Aggregate a)
371+ (HType (Reify (DB tag)), exprs) =
372+ gunbuildADT
373+ @(TTable (Reify Expr))
374+ @TColumns
375+ @TUnreify
376+ @(Col (Reify Expr))
377+ @(Eval (rep (Reify Expr)))
378+ (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns)
379+ (\SSpec {nullity} -> case nullity of
380+ Null -> id
381+ NotNull -> \(Reify (DB a)) -> Reify (DB (unsafeUnnullify a))) $
382+ hreify $
383+ gtoColumns es
384+
385+
386+type GGAggregate' :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
387+type family GGAggregate' algebra rep r where
388+ GGAggregate' 'K.Product rep r =
389+ GConstruct TUnreify (Eval (rep (Reify Expr)))
390+ (GConstruct TUnreify (Eval (rep (Reify Aggregate))) r -> r)
391+ GGAggregate' 'K.Sum rep r =
392+ GBuildADT TUnreify (Eval (rep (Reify Expr)))
393+ (GBuildADT TUnreify (Eval (rep (Reify Aggregate))) r -> r)
394+
395+
396+ggaggregate' :: forall algebra rep exprs agg. GGConstructable algebra rep
397+ => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Aggregate) -> agg)
398+ -> (exprs -> Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr))
399+ -> GGAggregate' algebra rep agg -> exprs -> agg
400+ggaggregate' gfromColumns gtoColumns agg es = case algebraSing @algebra of
401+ SProduct -> f $
402+ gfromColumns .
403+ hunreify .
404+ gconstruct
405+ @(TTable (Reify Aggregate))
406+ @TColumns
407+ @TUnreify
408+ @(Col (Reify Aggregate))
409+ @(Eval (rep (Reify Aggregate)))
410+ (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
411+ where
412+ f =
413+ gindex
414+ @TUnreify
415+ @(Eval (rep (Reify Expr)))
416+ @(GConstruct TUnreify (Eval (rep (Reify Aggregate))) agg -> agg)
417+ agg
418+ exprs .
419+ gtabulate
420+ @TUnreify
421+ @(Eval (rep (Reify Aggregate)))
422+ @agg
423+ exprs =
424+ gdeconstruct
425+ @(TTable (Reify Expr))
426+ @TColumns
427+ @TUnreify
428+ @(Col (Reify Expr))
429+ @(Eval (rep (Reify Expr)))
430+ (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns) $
431+ hreify $
432+ gtoColumns es
433+ SSum -> f exprs $
434+ gfromColumns .
435+ hunreify .
436+ gbuildADT
437+ @(TTable (Reify Aggregate))
438+ @TColumns
439+ @TUnreify
440+ @(Col (Reify Aggregate))
441+ @(Eval (rep (Reify Aggregate)))
442+ (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
443+ (\tag' SSpec {nullity} (Reify (Aggregation a)) ->
444+ Reify $ Aggregation $ runTag nullity (tag ==. litExpr tag') <$> a)
445+ (HType (Reify (Aggregation (groupByExpr tag))))
446+ where
447+ f e =
448+ gfindex
449+ @TUnreify
450+ @(Eval (rep (Reify Expr)))
451+ @(GBuildADT TUnreify (Eval (rep (Reify Aggregate))) agg -> agg)
452+ agg
453+ e .
454+ gftabulate
455+ @TUnreify
456+ @(Eval (rep (Reify Aggregate)))
457+ @agg
458+ (HType (Reify (DB tag)), exprs) =
459+ gunbuildADT
460+ @(TTable (Reify Expr))
461+ @TColumns
462+ @TUnreify
463+ @(Col (Reify Expr))
464+ @(Eval (rep (Reify Expr)))
465+ (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns)
466+ (\SSpec {nullity} -> case nullity of
467+ Null -> id
468+ NotNull -> \(Reify (DB a)) -> Reify (DB (unsafeUnnullify a))) $
469+ hreify $
470+ gtoColumns es
471+
472+
473+liftF½ :: MaybeApply Aggregate a -> Aggregate a
474+liftF½ (MaybeApply ma) = case ma of
475+ Left a -> a
476+ Right a -> a <$ groupByExpr (litExpr False)
477+
478+
479+liftF1½ :: Apply v => (a -> b -> c) -> v a -> MaybeApply v b -> v c
480+liftF1½ f a (MaybeApply eb) = case eb of
481+ Left b -> liftF2 f a b
482+ Right b -> fmap (`f` b) a
src/Rel8/Table/ADT.hs+36−249
@@ -1,17 +1,14 @@
11{-# language AllowAmbiguousTypes #-}
2−{-# language BlockArguments #-}
32{-# language DataKinds #-}
43{-# language FlexibleContexts #-}
54{-# language FlexibleInstances #-}
6−{-# language LambdaCase #-}
7−{-# language NamedFieldPuns #-}
85{-# language RankNTypes #-}
96{-# language ScopedTypeVariables #-}
107{-# language StandaloneKindSignatures #-}
118{-# language TypeApplications #-}
129{-# language TypeFamilies #-}
1310{-# language UndecidableInstances #-}
14−{-# language ViewPatterns #-}
11+{-# language UndecidableSuperClasses #-}
1512
1613module Rel8.Table.ADT
1714 ( ADT( ADT )
@@ -21,31 +18,25 @@ module Rel8.Table.ADT
2118 , InsertADT, insertADT
2219 , NameADT, nameADT
2320 , AggregateADT, aggregateADT
24− , AggregateADT', aggregateADT'
21+ , ADTRep
2522 )
2623where
2724
2825-- base
29−import Data.Bifunctor ( first )
3026import Data.Kind ( Constraint, Type )
31−import Data.List.NonEmpty ( NonEmpty( (:|) ) )
32−import Data.Type.Equality ( (:~:)( Refl ) )
33−import Prelude
27+import Prelude ()
3428
3529-- rel8
36−import Rel8.Aggregate ( Col( Aggregation ), Aggregate )
37−import Rel8.Expr ( Col( DB ), Expr )
38−import Rel8.Expr.Aggregate ( groupByExpr )
39−import Rel8.Expr.Eq ( (==.) )
40−import Rel8.Expr.Null ( nullify, snull, unsafeUnnullify )
41−import Rel8.Expr.Serialize ( litExpr )
42−import Rel8.FCF ( Compose )
43−import Rel8.Generic.Construction.ADT
44− ( GConstructableADT
45− , GBuildADT, gbuildADT, gunbuildADT
46− , GConstructADT, gconstructADT, gdeconstructADT
47− , CorepConstructors, GConstructors, gcindex, gctabulate
48− , CorepFields, gfindex, gftabulate, gftraverse
30+import Rel8.Aggregate ( Aggregate )
31+import Rel8.Expr ( Expr )
32+import Rel8.FCF ( Eval, Exp )
33+import Rel8.Generic.Construction
34+ ( GGConstructable
35+ , GGConstruct, ggconstruct
36+ , GGDeconstruct, ggdeconstruct
37+ , GGInsert, gginsert
38+ , GGName, ggname
39+ , GGAggregate, ggaggregate
4940 )
5041import Rel8.Generic.Rel8able
5142 ( Rel8able, Algebra
@@ -53,28 +44,13 @@ import Rel8.Generic.Rel8able
5344 , GColumnsADT, gfromColumnsADT, gtoColumnsADT
5445 , greify, gunreify
5546 )
56−import qualified Rel8.Generic.Table.ADT as G
5747import qualified Rel8.Kind.Algebra as K
58−import Rel8.Kind.Necessity ( SNecessity( SOptional, SRequired ) )
59−import Rel8.Schema.Context.Nullify ( runTag )
60−import Rel8.Schema.HTable ( HTable )
61−import Rel8.Schema.HTable.Type ( HType( HType ) )
62−import Rel8.Schema.Insert ( Col( OptionalInsert, RequiredInsert ), Insert )
48+import Rel8.Schema.Context ( Col )
49+import Rel8.Schema.Insert ( Insert )
6350import qualified Rel8.Schema.Kind as K
64−import Rel8.Schema.Name ( Col( NameCol ), Name( Name ) )
65−import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
66−import Rel8.Schema.Spec ( SSpec( SSpec, necessity, nullity, info ) )
67−import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify )
68−import Rel8.Schema.Result ( Result )
69−import Rel8.Table
70− ( TTable, TColumns, TUnreify
71− , Table, fromColumns, toColumns, reify, unreify
72− )
73−import Rel8.Table.Bool ( case_ )
74−import Rel8.Type.Tag ( Tag )
75−
76−-- semigroupoids
77−import Data.Functor.Apply ( Apply, MaybeApply( MaybeApply ), liftF2 )
51+import Rel8.Schema.Name ( Name )
52+import Rel8.Schema.Reify ( hreify, hunreify )
53+import Rel8.Table ( Table )
7854
7955
8056type ADT :: K.Rel8able -> K.Rel8able
@@ -100,242 +76,53 @@ instance Rel8able t => Rel8able (ADT t) where
10076
10177
10278type ConstructableADT :: K.Rel8able -> Constraint
103−class
104− ( CorepConstructors TUnreify (GRep t (Reify Expr))
105− , CorepConstructors TUnreify (GRep t (Reify Insert))
106− , CorepFields (Compose Aggregate TUnreify) (GRep t (Reify Expr))
107− , CorepFields TUnreify (GRep t (Reify Aggregate))
108− , CorepFields TUnreify (GRep t (Reify Expr))
109− , CorepFields TUnreify (GRep t (Reify Name))
110− , G.GColumnsADT TColumns (GRep t (Reify Aggregate)) ~ GColumnsADT t
111− , G.GColumnsADT TColumns (GRep t (Reify Expr)) ~ GColumnsADT t
112− , G.GColumnsADT TColumns (GRep t (Reify Insert)) ~ GColumnsADT t
113− , G.GColumnsADT TColumns (GRep t (Reify Name)) ~ GColumnsADT t
114− , Functor (GConstructors TUnreify (GRep t (Reify Expr)))
115− , Functor (GConstructors TUnreify (GRep t (Reify Insert)))
116− , HTable (G.GColumnsADT TColumns (GRep t (Reify Result)))
117− , GConstructableADT (TTable (Reify Aggregate)) TColumns TUnreify (Col (Reify Aggregate)) (GRep t (Reify Aggregate))
118− , GConstructableADT (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (GRep t (Reify Expr))
119− , GConstructableADT (TTable (Reify Insert)) TColumns TUnreify (Col (Reify Insert)) (GRep t (Reify Insert))
120− , GConstructableADT (TTable (Reify Name)) TColumns TUnreify (Col (Reify Name)) (GRep t (Reify Name))
121− )
122− => ConstructableADT t
123−instance
124− ( CorepConstructors TUnreify (GRep t (Reify Expr))
125− , CorepConstructors TUnreify (GRep t (Reify Insert))
126− , CorepFields (Compose Aggregate TUnreify) (GRep t (Reify Expr))
127− , CorepFields TUnreify (GRep t (Reify Aggregate))
128− , CorepFields TUnreify (GRep t (Reify Expr))
129− , CorepFields TUnreify (GRep t (Reify Name))
130− , G.GColumnsADT TColumns (GRep t (Reify Aggregate)) ~ GColumnsADT t
131− , G.GColumnsADT TColumns (GRep t (Reify Expr)) ~ GColumnsADT t
132− , G.GColumnsADT TColumns (GRep t (Reify Insert)) ~ GColumnsADT t
133− , G.GColumnsADT TColumns (GRep t (Reify Name)) ~ GColumnsADT t
134− , Functor (GConstructors TUnreify (GRep t (Reify Expr)))
135− , Functor (GConstructors TUnreify (GRep t (Reify Insert)))
136− , HTable (G.GColumnsADT TColumns (GRep t (Reify Result)))
137− , GConstructableADT (TTable (Reify Aggregate)) TColumns TUnreify (Col (Reify Aggregate)) (GRep t (Reify Aggregate))
138− , GConstructableADT (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (GRep t (Reify Expr))
139− , GConstructableADT (TTable (Reify Insert)) TColumns TUnreify (Col (Reify Insert)) (GRep t (Reify Insert))
140− , GConstructableADT (TTable (Reify Name)) TColumns TUnreify (Col (Reify Name)) (GRep t (Reify Name))
141− )
142− => ConstructableADT t
79+class GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
80+instance GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
14381
14482
14583type ConstructADT :: K.Rel8able -> Type
146−type ConstructADT t = (forall r. GConstructADT TUnreify (GRep t (Reify Expr)) r r) -> ADT t Expr
84+type ConstructADT t = GGConstruct 'K.Sum (ADTRep t) (ADT t Expr)
14785
14886
14987constructADT :: forall t. ConstructableADT t => ConstructADT t
150−constructADT f =
151− gcindex @TUnreify @(GRep t (Reify Expr)) @(ADT t Expr) (f @(ADT t Expr)) $
152− fmap (ADT . hunreify) $
153− gconstructADT
154− @(TTable (Reify Expr))
155− @TColumns
156− @TUnreify
157− @(Col (Reify Expr))
158− @(GRep t (Reify Expr))
159− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
160− (\SSpec {info} -> Reify (DB (snull info)))
161− (\SSpec {nullity} -> case nullity of
162− Null -> id
163− NotNull -> \(Reify (DB a)) -> Reify (DB (nullify a)))
164− (HType . Reify . DB . litExpr)
88+constructADT = ggconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) ADT
16589
16690
16791type DeconstructADT :: K.Rel8able -> Type -> Type
168−type DeconstructADT t r = GConstructADT TUnreify (GRep t (Reify Expr)) r (ADT t Expr -> r)
92+type DeconstructADT t r = GGDeconstruct 'K.Sum (ADTRep t) (ADT t Expr) r
16993
17094
17195deconstructADT :: forall t r. (ConstructableADT t, Table Expr r)
17296 => DeconstructADT t r
173−deconstructADT =
174− gctabulate @TUnreify @(GRep t (Reify Expr)) @r @(ADT t Expr -> r)
175− \constructors (ADT columns) ->
176− let
177− (HType (Reify (DB tag)), cases) = gdeconstructADT
178− @(TTable (Reify Expr))
179− @TColumns
180− @TUnreify
181− @(Col (Reify Expr))
182− @(GRep t (Reify Expr))
183− (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns)
184− (\SSpec {nullity} -> case nullity of
185− Null -> id
186− NotNull -> \(Reify (DB a)) -> Reify (DB (unsafeUnnullify a)))
187− constructors
188− (hreify columns)
189− in
190− case cases of
191− ((_, r) :| (map (first ((tag ==.) . litExpr)) -> cases')) ->
192− case_ cases' r
97+deconstructADT = ggdeconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) @r (\(ADT a) -> a)
19398
19499
195100type InsertADT :: K.Rel8able -> Type
196−type InsertADT t = (forall r. GConstructADT TUnreify (GRep t (Reify Insert)) r r) -> ADT t Insert
101+type InsertADT t = GGInsert 'K.Sum (ADTRep t) (ADT t Insert)
197102
198103
199104insertADT :: forall t. ConstructableADT t => InsertADT t
200−insertADT f =
201− gcindex @TUnreify @(GRep t (Reify Insert)) @(ADT t Insert) (f @(ADT t Insert)) $
202− fmap (ADT . hunreify) $
203− gconstructADT
204− @(TTable (Reify Insert))
205− @TColumns
206− @TUnreify
207− @(Col (Reify Insert))
208− @(GRep t (Reify Insert))
209− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
210− (\SSpec {necessity, info} -> Reify $ case necessity of
211− SRequired -> RequiredInsert (snull info)
212− SOptional -> OptionalInsert (Just (snull info)))
213− (\SSpec {nullity} -> case nullity of
214− Null -> id
215− NotNull -> \case
216− Reify (RequiredInsert a) -> Reify (RequiredInsert (nullify a))
217− Reify (OptionalInsert a) -> Reify (OptionalInsert (nullify <$> a)))
218− (HType . Reify . RequiredInsert . litExpr)
105+insertADT = gginsert @'K.Sum @(ADTRep t) @(ADT t Insert) ADT
219106
220107
221108type NameADT :: K.Rel8able -> Type
222−type NameADT t = Name Tag -> GBuildADT TUnreify (GRep t (Reify Name)) (ADT t Name)
109+type NameADT t = GGName 'K.Sum (ADTRep t) (ADT t Name)
223110
224111
225112nameADT :: forall t. ConstructableADT t => NameADT t
226−nameADT tag = gftabulate @TUnreify @(GRep t (Reify Name)) @(ADT t Name) $
227− ADT .
228− hunreify .
229− gbuildADT
230− @(TTable (Reify Name))
231− @TColumns
232− @TUnreify
233− @(Col (Reify Name))
234− @(GRep t (Reify Name))
235− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
236− (\_ _ (Reify (NameCol a)) -> Reify (NameCol a))
237− (HType ((\(Name a) -> Reify (NameCol a)) tag))
113+nameADT = ggname @'K.Sum @(ADTRep t) @(ADT t Name) ADT
238114
239115
240116type AggregateADT :: K.Rel8able -> Type
241−type AggregateADT t = forall r.
242− GBuildADT TUnreify (GRep t (Reify Expr))
243− (GBuildADT (Compose Aggregate TUnreify) (GRep t (Reify Expr)) r -> r)
117+type AggregateADT t = forall r. GGAggregate 'K.Sum (ADTRep t) r
244118
245119
246120aggregateADT :: forall t. ConstructableADT t
247121 => AggregateADT t -> ADT t Expr -> Aggregate (ADT t Expr)
248−aggregateADT builder (ADT columns) = f exprs $
249− liftF1½
250− (\tag' ->
251− ADT .
252− hunreify .
253− gbuildADT
254− @(TTable (Reify Expr))
255− @TColumns
256− @TUnreify
257− @(Col (Reify Expr))
258− @(GRep t (Reify Expr))
259− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
260− (\tag'' SSpec {nullity} (Reify (DB a)) ->
261− Reify $ DB $ runTag nullity (tag ==. litExpr tag'') a)
262− (HType (Reify (DB tag'))))
263− (groupByExpr tag) .
264− gftraverse @TUnreify @(GRep t (Reify Expr)) @_ @Aggregate (MaybeApply . Left)
265− where
266− f e =
267− gfindex
268− @TUnreify
269− @(GRep t (Reify Expr))
270− @(GBuildADT (Compose Aggregate TUnreify) (GRep t (Reify Expr)) (Aggregate (ADT t Expr)) -> Aggregate (ADT t Expr))
271− (builder @(Aggregate (ADT t Expr)))
272− e .
273− gftabulate
274− @(Compose Aggregate TUnreify)
275− @(GRep t (Reify Expr))
276− @(Aggregate (ADT t Expr))
277− (HType (Reify (DB tag)), exprs) =
278− gunbuildADT
279− @(TTable (Reify Expr))
280− @TColumns
281− @TUnreify
282− @(Col (Reify Expr))
283− @(GRep t (Reify Expr))
284− (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns)
285− (\SSpec {nullity} -> case nullity of
286− Null -> id
287− NotNull -> \(Reify (DB a)) -> Reify (DB (unsafeUnnullify a)))
288− (hreify columns)
289−
290−
291−type AggregateADT' :: K.Rel8able -> Type
292−type AggregateADT' t = forall r.
293− GBuildADT TUnreify (GRep t (Reify Expr))
294− (GBuildADT TUnreify (GRep t (Reify Aggregate)) r -> r)
295−
296−
297−aggregateADT' :: forall t. ConstructableADT t
298− => AggregateADT' t -> ADT t Expr -> ADT t Aggregate
299−aggregateADT' builder (ADT columns) = f exprs $
300− ADT .
301− hunreify .
302− gbuildADT
303− @(TTable (Reify Aggregate))
304− @TColumns
305− @TUnreify
306− @(Col (Reify Aggregate))
307− @(GRep t (Reify Aggregate))
308− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
309− (\tag' SSpec {nullity} (Reify (Aggregation a)) ->
310− Reify $ Aggregation $ runTag nullity (tag ==. litExpr tag') <$> a)
311− (HType (Reify (Aggregation (groupByExpr tag))))
312− where
313− f e =
314− gfindex
315− @TUnreify
316− @(GRep t (Reify Expr))
317− @(GBuildADT TUnreify (GRep t (Reify Aggregate)) (ADT t Aggregate) -> ADT t Aggregate)
318− (builder @(ADT t Aggregate))
319− e .
320− gftabulate
321− @TUnreify
322− @(GRep t (Reify Aggregate))
323− @(ADT t Aggregate)
324− (HType (Reify (DB tag)), exprs) =
325− gunbuildADT
326− @(TTable (Reify Expr))
327− @TColumns
328− @TUnreify
329− @(Col (Reify Expr))
330− @(GRep t (Reify Expr))
331− (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns)
332− (\SSpec {nullity} -> case nullity of
333− Null -> id
334− NotNull -> \(Reify (DB a)) -> Reify (DB (unsafeUnnullify a)))
335− (hreify columns)
336−
337−
338−liftF1½ :: Apply v => (a -> b -> c) -> v a -> MaybeApply v b -> v c
339−liftF1½ f a (MaybeApply eb) = case eb of
340− Left b -> liftF2 f a b
341− Right b -> fmap (`f` b) a
122+aggregateADT f =
123+ ggaggregate @'K.Sum @(ADTRep t) @(ADT t Expr) ADT (\(ADT a) -> a)
124+ (f @(Aggregate (ADT t Expr)))
125+
126+
127+data ADTRep :: K.Rel8able -> K.Context -> Exp (Type -> Type)
128+type instance Eval (ADTRep t context) = GRep t context