git.iko.soy/rel8
on master help sign in
Add build{ADT,HKD} alternative to church encoded construct{ADT,HKD}
commit4017859c0ca45ddde9207e54560107a19b8618da authorShane O'Brien <shane.obrien@circuithub.com> dateFri 11 Jun 2021, 14:15 (5 years ago) parent8301eb7
7 files changed+356−84
compare with master
unifiedsplit
src/Rel8.hs+2 src/Rel8/Generic/Construction.hs+131−52 src/Rel8/Generic/Construction/ADT.hs+143−2 src/Rel8/Generic/Construction/Record.hs+16−3 src/Rel8/Generic/Rel8able/Test.hs+1−1 src/Rel8/Table/ADT.hs+32−13 src/Rel8/Table/HKD.hs+31−13
src/Rel8.hs+2
@@ -110,6 +110,7 @@ module Rel8
110110
111111 -- ** @ADT@
112112 , ADT, ADTable, fromADT, toADT
113+ , BuildADT, buildADT
113114 , ConstructADT, constructADT
114115 , DeconstructADT, deconstructADT
115116 , InsertADT, insertADT
@@ -118,6 +119,7 @@ module Rel8
118119
119120 -- ** @HKD@
120121 , HKD, HKDable, fromHKD, toHKD
122+ , BuildHKD, buildHKD
121123 , ConstructHKD, constructHKD
122124 , DeconstructHKD, deconstructHKD
123125 , InsertHKD, insertHKD
src/Rel8/Generic/Construction.hs+131−52
@@ -14,10 +14,12 @@
1414{-# language ViewPatterns #-}
1515
1616module Rel8.Generic.Construction
17− ( GGConstructable
17+ ( GGBuildable
18+ , GGBuild, ggbuild
19+ , GGInsert, gginsert
20+ , GGConstructable
1821 , GGConstruct, ggconstruct
1922 , GGDeconstruct, ggdeconstruct
20− , GGInsert, gginsert
2123 , GGName, ggname
2224 , GGAggregate, ggaggregate
2325 , GGAggregate', ggaggregate'
@@ -29,6 +31,7 @@ import Data.Bifunctor ( first )
2931import Data.Kind ( Constraint, Type )
3032import Data.List.NonEmpty ( NonEmpty( (:|) ) )
3133import Data.Type.Equality ( (:~:)( Refl ) )
34+import GHC.TypeLits ( Symbol )
3235import Prelude
3336
3437-- rel8
@@ -40,14 +43,16 @@ import Rel8.Expr.Null ( nullify, snull, unsafeUnnullify )
4043import Rel8.Expr.Serialize ( litExpr )
4144import Rel8.FCF ( Compose, Eval, Exp )
4245import Rel8.Generic.Construction.ADT
43− ( GConstructableADT
46+ ( GConstructorADT, GMakeableADT, gmakeADT
47+ , GConstructableADT
4448 , GBuildADT, gbuildADT, gunbuildADT
4549 , GConstructADT, gconstructADT, gdeconstructADT
4650 , CorepConstructors, GConstructors, gcindex, gctabulate
4751 , CorepFields, gfindex, gftabulate, gftraverse
4852 )
4953import Rel8.Generic.Construction.Record
50− ( GConstructable, GConstruct, gconstruct, gdeconstruct
54+ ( GConstructor
55+ , GConstructable, GConstruct, gconstruct, gdeconstruct
5156 , Corep, gindex, gtabulate, gtraverse
5257 )
5358import Rel8.Generic.Table ( GGColumns )
@@ -78,6 +83,124 @@ import Rel8.Type.Tag ( Tag )
7883import Data.Functor.Apply ( Apply, MaybeApply( MaybeApply ), liftF2 )
7984
8085
86+type GGBuildable :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Constraint
87+type GGBuildable algebra name rep =
88+ ( KnownAlgebra algebra
89+ , Eval (GGColumns algebra TColumns (Eval (rep (Reify Aggregate)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
90+ , Eval (GGColumns algebra TColumns (Eval (rep (Reify Expr)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
91+ , Eval (GGColumns algebra TColumns (Eval (rep (Reify Insert)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
92+ , Eval (GGColumns algebra TColumns (Eval (rep (Reify Name)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
93+ , HTable (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))))
94+ , GGBuildable' algebra name rep
95+ )
96+
97+
98+type GGBuildable' :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Constraint
99+type family GGBuildable' algebra name rep where
100+ GGBuildable' 'K.Product name rep =
101+ ( name ~ GConstructor (Eval (rep (Reify Expr)))
102+ , name ~ GConstructor (Eval (rep (Reify Insert)))
103+ , Corep TUnreify (Eval (rep (Reify Expr)))
104+ , Corep TUnreify (Eval (rep (Reify Insert)))
105+ , GConstructable (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (Eval (rep (Reify Expr)))
106+ , GConstructable (TTable (Reify Insert)) TColumns TUnreify (Col (Reify Insert)) (Eval (rep (Reify Insert)))
107+ )
108+ GGBuildable' 'K.Sum name rep =
109+ ( Corep TUnreify (GConstructorADT name (Eval (rep (Reify Expr))))
110+ , Corep TUnreify (GConstructorADT name (Eval (rep (Reify Insert))))
111+ , GMakeableADT (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) name (Eval (rep (Reify Expr)))
112+ , GMakeableADT (TTable (Reify Insert)) TColumns TUnreify (Col (Reify Insert)) name (Eval (rep (Reify Insert)))
113+ )
114+
115+
116+type GGBuild :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
117+type family GGBuild algebra name rep r where
118+ GGBuild 'K.Product _name rep r =
119+ GConstruct TUnreify (Eval (rep (Reify Expr))) r
120+ GGBuild 'K.Sum name rep r =
121+ GConstruct TUnreify (GConstructorADT name (Eval (rep (Reify Expr)))) r
122+
123+
124+ggbuild :: forall algebra name rep a. GGBuildable algebra name rep
125+ => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr) -> a)
126+ -> GGBuild algebra name rep a
127+ggbuild gfromColumns = case algebraSing @algebra of
128+ SProduct ->
129+ gtabulate @TUnreify @(Eval (rep (Reify Expr))) @a $
130+ gfromColumns .
131+ hunreify .
132+ gconstruct
133+ @(TTable (Reify Expr))
134+ @TColumns
135+ @TUnreify
136+ @(Col (Reify Expr))
137+ @(Eval (rep (Reify Expr)))
138+ (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
139+ SSum ->
140+ gtabulate @TUnreify @(GConstructorADT name (Eval (rep (Reify Expr)))) @a $
141+ gfromColumns .
142+ hunreify .
143+ gmakeADT
144+ @(TTable (Reify Expr))
145+ @TColumns
146+ @TUnreify
147+ @(Col (Reify Expr))
148+ @name
149+ @(Eval (rep (Reify Expr)))
150+ (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
151+ (\SSpec {info} -> Reify (DB (snull info)))
152+ (\SSpec {nullity} -> case nullity of
153+ Null -> id
154+ NotNull -> \(Reify (DB a)) -> Reify (DB (nullify a)))
155+ (HType . Reify . DB . litExpr)
156+
157+
158+type GGInsert :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
159+type family GGInsert algebra name rep r where
160+ GGInsert 'K.Product _name rep r =
161+ GConstruct TUnreify (Eval (rep (Reify Insert))) r
162+ GGInsert 'K.Sum name rep r =
163+ GConstruct TUnreify (GConstructorADT name (Eval (rep (Reify Insert)))) r
164+
165+
166+gginsert :: forall algebra name rep a. GGBuildable algebra name rep
167+ => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Insert) -> a)
168+ -> GGInsert algebra name rep a
169+gginsert gfromColumns = case algebraSing @algebra of
170+ SProduct ->
171+ gtabulate @TUnreify @(Eval (rep (Reify Insert))) @a $
172+ gfromColumns .
173+ hunreify .
174+ gconstruct
175+ @(TTable (Reify Insert))
176+ @TColumns
177+ @TUnreify
178+ @(Col (Reify Insert))
179+ @(Eval (rep (Reify Insert)))
180+ (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
181+ SSum ->
182+ gtabulate @TUnreify @(GConstructorADT name (Eval (rep (Reify Insert)))) @a $
183+ gfromColumns .
184+ hunreify .
185+ gmakeADT
186+ @(TTable (Reify Insert))
187+ @TColumns
188+ @TUnreify
189+ @(Col (Reify Insert))
190+ @name
191+ @(Eval (rep (Reify Insert)))
192+ (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
193+ (\SSpec {necessity, info} -> Reify $ case necessity of
194+ SRequired -> RequiredInsert (snull info)
195+ SOptional -> OptionalInsert (Just (snull info)))
196+ (\SSpec {nullity} -> case nullity of
197+ Null -> id
198+ NotNull -> \case
199+ Reify (RequiredInsert a) -> Reify (RequiredInsert (nullify a))
200+ Reify (OptionalInsert a) -> Reify (OptionalInsert (nullify <$> a)))
201+ (HType . Reify . RequiredInsert . litExpr)
202+
203+
81204type GGConstructable :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
82205type GGConstructable algebra rep =
83206 ( KnownAlgebra algebra
@@ -121,8 +244,10 @@ type family GGConstructable' algebra rep where
121244
122245type GGConstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
123246type family GGConstruct algebra rep r where
124− GGConstruct 'K.Product rep r = GConstruct TUnreify (Eval (rep (Reify Expr))) r -> r
125− GGConstruct 'K.Sum rep r = GConstructADT TUnreify (Eval (rep (Reify Expr))) r r
247+ GGConstruct 'K.Product rep r =
248+ GConstruct TUnreify (Eval (rep (Reify Expr))) r -> r
249+ GGConstruct 'K.Sum rep r =
250+ GConstructADT TUnreify (Eval (rep (Reify Expr))) r r
126251
127252
128253ggconstruct :: forall algebra rep a. GGConstructable algebra rep
@@ -204,52 +329,6 @@ ggdeconstruct gtoColumns = case algebraSing @algebra of
204329 case_ cases' r
205330
206331
207−type GGInsert :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
208−type family GGInsert algebra rep r where
209− GGInsert 'K.Product rep r =
210− GConstruct TUnreify (Eval (rep (Reify Insert))) r -> r
211− GGInsert 'K.Sum rep r =
212− GConstructADT TUnreify (Eval (rep (Reify Insert))) r r
213−
214−
215−gginsert :: forall algebra rep a. GGConstructable algebra rep
216− => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Insert) -> a)
217− -> GGInsert algebra rep a
218− -> a
219−gginsert gfromColumns f = case algebraSing @algebra of
220− SProduct ->
221− f $
222− gtabulate @TUnreify @(Eval (rep (Reify Insert))) @a $
223− gfromColumns .
224− hunreify .
225− gconstruct
226− @(TTable (Reify Insert))
227− @TColumns
228− @TUnreify
229− @(Col (Reify Insert))
230− @(Eval (rep (Reify Insert)))
231− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
232− SSum ->
233− gcindex @TUnreify @(Eval (rep (Reify Insert))) @a f $
234− fmap (gfromColumns . hunreify) $
235− gconstructADT
236− @(TTable (Reify Insert))
237− @TColumns
238− @TUnreify
239− @(Col (Reify Insert))
240− @(Eval (rep (Reify Insert)))
241− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
242− (\SSpec {necessity, info} -> Reify $ case necessity of
243− SRequired -> RequiredInsert (snull info)
244− SOptional -> OptionalInsert (Just (snull info)))
245− (\SSpec {nullity} -> case nullity of
246− Null -> id
247− NotNull -> \case
248− Reify (RequiredInsert a) -> Reify (RequiredInsert (nullify a))
249− Reify (OptionalInsert a) -> Reify (OptionalInsert (nullify <$> a)))
250− (HType . Reify . RequiredInsert . litExpr)
251−
252−
253332type GGName :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
254333type family GGName algebra rep a where
255334 GGName 'K.Product rep a = GConstruct TUnreify (Eval (rep (Reify Name))) a
src/Rel8/Generic/Construction/ADT.hs+143−2
@@ -18,6 +18,7 @@ module Rel8.Generic.Construction.ADT
1818 , GConstructADT, gconstructADT, gdeconstructADT
1919 , GFields, CorepFields, gftabulate, gfindex, gftraverse
2020 , GConstructors, CorepConstructors, gctabulate, gcindex
21+ , GConstructorADT, GMakeableADT, gmakeADT
2122 )
2223where
2324
@@ -31,9 +32,12 @@ import Data.Proxy ( Proxy( Proxy ) )
3132import GHC.Generics
3233 ( (:+:), (:*:)( (:*:) ), M1, U1
3334 , C, D
34− , Meta( MetaCons )
35+ , Meta( MetaData, MetaCons )
36+ )
37+import GHC.TypeLits
38+ ( ErrorMessage( (:<>:), Text ), TypeError
39+ , Symbol, KnownSymbol, symbolVal
3540 )
36−import GHC.TypeLits ( KnownSymbol, symbolVal )
3741import Prelude hiding ( null )
3842
3943-- rel8
@@ -80,6 +84,32 @@ type Unnullifier context = forall labels necessity a. ()
8084 -> context ('Spec labels necessity a)
8185
8286
87+type NoConstructor :: Symbol -> Symbol -> ErrorMessage
88+type NoConstructor datatype constructor =
89+ ( 'Text "The type `" ':<>:
90+ 'Text datatype ':<>:
91+ 'Text "` has no constructor `" ':<>:
92+ 'Text constructor ':<>:
93+ 'Text "`."
94+ )
95+
96+
97+type GConstructorADT :: Symbol -> (Type -> Type) -> Type -> Type
98+type family GConstructorADT name rep where
99+ GConstructorADT name (M1 D ('MetaData datatype _ _ _) rep) =
100+ GConstructorADT' name rep (TypeError (NoConstructor datatype name))
101+
102+
103+type GConstructorADT' :: Symbol -> (Type -> Type) -> (Type -> Type) -> Type -> Type
104+type family GConstructorADT' name rep fallback where
105+ GConstructorADT' name (M1 D _ rep) fallback =
106+ GConstructorADT' name rep fallback
107+ GConstructorADT' name (a :+: b) fallback =
108+ GConstructorADT' name a (GConstructorADT' name b fallback)
109+ GConstructorADT' name (M1 C ('MetaCons name _ _) rep) _ = rep
110+ GConstructorADT' _ _ fallback = fallback
111+
112+
83113type GConstructADT
84114 :: (Type -> Exp Type)
85115 -> (Type -> Type) -> Type -> Type -> Type
@@ -357,3 +387,114 @@ instance {-# OVERLAPPABLE #-}
357387 tag = Tag $ pack $ symbolVal (Proxy @label)
358388
359389 gfill null htable = HProduct htable (hlabel hlabeler (hnulls null))
390+
391+
392+type GMakeableADT
393+ :: (Type -> Exp Constraint)
394+ -> (Type -> Exp K.HTable)
395+ -> (Type -> Exp Type)
396+ -> K.HContext -> Symbol -> (Type -> Type) -> Constraint
397+class GMakeableADT _Table _Columns f context name rep where
398+ gmakeADT :: ()
399+ => ToColumns _Table _Columns f context
400+ -> Null context
401+ -> Nullifier context
402+ -> (Tag -> HType Tag context)
403+ -> GFields f (GConstructorADT name rep)
404+ -> GColumnsADT _Columns rep context
405+
406+
407+instance
408+ ( htable ~ HLabel "tag" (HType Tag)
409+ , meta ~ 'MetaData datatype _module _package _newtype
410+ , fallback ~ TypeError (NoConstructor datatype name)
411+ , fields ~ GFields f (GConstructorADT' name rep fallback)
412+ , GMakeableADT' _Table _Columns f context htable name rep fields
413+ , HLabelable context
414+ , KnownSymbol name
415+ )
416+ => GMakeableADT _Table _Columns f context name (M1 D meta rep)
417+ where
418+ gmakeADT toColumns null nullifier wrap =
419+ gmakeADT'
420+ @_Table @_Columns @f @context @htable @name @rep @fields
421+ toColumns null nullifier htable
422+ where
423+ tag = Tag $ pack $ symbolVal (Proxy @name)
424+ htable = hlabel hlabeler (wrap tag)
425+
426+
427+type GMakeableADT'
428+ :: (Type -> Exp Constraint)
429+ -> (Type -> Exp K.HTable)
430+ -> (Type -> Exp Type)
431+ -> K.HContext -> K.HTable -> Symbol -> (Type -> Type) -> Type -> Constraint
432+class GMakeableADT' _Table _Columns f context htable name rep fields where
433+ gmakeADT' :: ()
434+ => ToColumns _Table _Columns f context
435+ -> Null context
436+ -> Nullifier context
437+ -> htable context
438+ -> fields
439+ -> GColumnsADT' _Columns htable rep context
440+
441+
442+instance
443+ ( htable' ~ GColumnsADT' _Columns htable a
444+ , GMakeableADT' _Table _Columns f context htable name a fields
445+ , GMakeableADT' _Table _Columns f context htable' name b fields
446+ )
447+ => GMakeableADT' _Table _Columns f context htable name (a :+: b) fields
448+ where
449+ gmakeADT' toColumns null nullifier htable x =
450+ gmakeADT' @_Table @_Columns @f @context @htable' @name @b @fields
451+ toColumns null nullifier
452+ (gmakeADT'
453+ @_Table @_Columns @f @context @htable @name @a @fields toColumns
454+ null nullifier htable x)
455+ x
456+
457+
458+instance {-# OVERLAPPING #-}
459+ GMakeableADT' _Table _Columns f context htable name (M1 C ('MetaCons name _fixity _isRecord) U1) fields
460+ where
461+ gmakeADT' _ _ _ = const
462+
463+
464+instance {-# OVERLAPS #-}
465+ GMakeableADT' _Table _Columns f context htable name (M1 C ('MetaCons label _fixity _isRecord) U1) fields
466+ where
467+ gmakeADT' _ _ _ = const
468+
469+
470+instance {-# OVERLAPS #-}
471+ ( HTable (GColumns _Columns rep)
472+ , KnownSymbol name
473+ , HLabelable context
474+ , GConstructable _Table _Columns f context rep
475+ , fields ~ GFields f rep
476+ , GColumnsADT' _Columns htable (M1 C ('MetaCons name _fixity _isRecord) rep) ~
477+ HProduct htable (HLabel name (HNullify (GColumns _Columns rep)))
478+ )
479+ => GMakeableADT' _Table _Columns f context htable name (M1 C ('MetaCons name _fixity _isRecord) rep) fields
480+ where
481+ gmakeADT' toColumns _ nullifier htable =
482+ HProduct htable .
483+ hlabel hlabeler .
484+ hnullify nullifier .
485+ gconstruct @_Table @_Columns @f @context @rep toColumns
486+
487+
488+instance {-# OVERLAPPABLE #-}
489+ ( HTable (GColumns _Columns rep)
490+ , KnownSymbol label
491+ , HLabelable context
492+ , GColumnsADT' _Columns htable (M1 C ('MetaCons label _fixity _isRecord) rep) ~
493+ HProduct htable (HLabel label (HNullify (GColumns _Columns rep)))
494+ )
495+ => GMakeableADT' _Table _Columns f context htable name (M1 C ('MetaCons label _fixity _isRecord) rep) fields
496+ where
497+ gmakeADT' _ null _ htable _ =
498+ HProduct htable $
499+ hlabel hlabeler $
500+ hnulls null
src/Rel8/Generic/Construction/Record.hs+16−3
@@ -12,7 +12,7 @@
1212{-# language UndecidableInstances #-}
1313
1414module Rel8.Generic.Construction.Record
15− ( GConstruct, GConstructable, gconstruct, gdeconstruct
15+ ( GConstructor, GConstruct, GConstructable, gconstruct, gdeconstruct
1616 , GFields, Corep, gtabulate, gindex, gtraverse
1717 , FromColumns, ToColumns
1818 )
@@ -24,9 +24,12 @@ import Data.Kind ( Constraint, Type )
2424import Data.Proxy ( Proxy( Proxy ) )
2525import GHC.Generics
2626 ( (:*:), K1, M1, U1
27− , D, C, S, Meta( MetaSel )
27+ , D, C, S, Meta( MetaData, MetaCons, MetaSel )
28+ )
29+import GHC.TypeLits
30+ ( ErrorMessage( (:<>:), Text ), TypeError
31+ , Symbol, KnownSymbol
2832 )
29−import GHC.TypeLits ( KnownSymbol )
3033import Prelude
3134
3235-- rel8
@@ -59,6 +62,16 @@ type ToColumns _Table _Columns f context = forall proxy x.
5962 Eval (_Table x) => proxy x -> Eval (f x) -> Eval (_Columns x) context
6063
6164
65+type GConstructor :: (Type -> Type) -> Symbol
66+type family GConstructor rep where
67+ GConstructor (M1 D _ (M1 C ('MetaCons name _ _) _)) = name
68+ GConstructor (M1 D ('MetaData name _ _ _) _) = TypeError (
69+ 'Text "`" ':<>:
70+ 'Text name ':<>:
71+ 'Text "` does not appear to have exactly 1 constructor"
72+ )
73+
74+
6275type GConstruct :: (Type -> Exp Type) -> (Type -> Type) -> Type -> Type
6376type family GConstruct f rep r where
6477 GConstruct f (M1 _ _ rep) r = GConstruct f rep r
src/Rel8/Generic/Rel8able/Test.hs+1−1
@@ -106,7 +106,7 @@ deriving via HKDT S3Object
106106 instance x ~ HKD S3Object Expr => ToExprs x S3Object
107107
108108
109−data HKDSum = HKDSumA Text | HKDSumB Bool Char
109+data HKDSum = HKDSumA Text | HKDSumB Bool Char | HKDSumC
110110 deriving stock Generic
111111
112112
src/Rel8/Table/ADT.hs+32−13
@@ -2,6 +2,7 @@
22{-# language DataKinds #-}
33{-# language FlexibleContexts #-}
44{-# language FlexibleInstances #-}
5+{-# language MultiParamTypeClasses #-}
56{-# language RankNTypes #-}
67{-# language ScopedTypeVariables #-}
78{-# language StandaloneKindSignatures #-}
@@ -13,10 +14,12 @@
1314module Rel8.Table.ADT
1415 ( ADT( ADT )
1516 , ADTable, fromADT, toADT
17+ , BuildableADT
18+ , BuildADT, buildADT
19+ , InsertADT, insertADT
1620 , ConstructableADT
1721 , ConstructADT, constructADT
1822 , DeconstructADT, deconstructADT
19− , InsertADT, insertADT
2023 , NameADT, nameADT
2124 , AggregateADT, aggregateADT
2225 , ADTRep
@@ -28,6 +31,7 @@ import Data.Kind ( Constraint, Type )
2831import Data.Proxy ( Proxy( Proxy ) )
2932import Data.Type.Equality ( (:~:)( Refl ) )
3033import GHC.Generics ( Generic, Rep, from, to )
34+import GHC.TypeLits ( Symbol )
3135import Prelude
3236
3337-- rel8
@@ -35,10 +39,12 @@ import Rel8.Aggregate ( Aggregate )
3539import Rel8.Expr ( Expr )
3640import Rel8.FCF ( Eval, Exp )
3741import Rel8.Generic.Construction
38− ( GGConstructable
42+ ( GGBuildable
43+ , GGBuild, ggbuild
44+ , GGInsert, gginsert
45+ , GGConstructable
3946 , GGConstruct, ggconstruct
4047 , GGDeconstruct, ggdeconstruct
41− , GGInsert, gginsert
4248 , GGName, ggname
4349 , GGAggregate, ggaggregate
4450 )
@@ -136,6 +142,29 @@ instance
136142 => ADTable t
137143
138144
145+type BuildableADT :: K.Rel8able -> Symbol -> Constraint
146+class GGBuildable 'K.Sum name (ADTRep t) => BuildableADT t name
147+instance GGBuildable 'K.Sum name (ADTRep t) => BuildableADT t name
148+
149+
150+type BuildADT :: K.Rel8able -> Symbol -> Type
151+type BuildADT t name = GGBuild 'K.Sum name (ADTRep t) (ADT t Expr)
152+
153+
154+buildADT :: forall t name. BuildableADT t name => BuildADT t name
155+buildADT =
156+ ggbuild @'K.Sum @name @(ADTRep t) @(ADT t Expr) ADT
157+
158+
159+type InsertADT :: K.Rel8able -> Symbol -> Type
160+type InsertADT t name = GGInsert 'K.Sum name (ADTRep t) (ADT t Insert)
161+
162+
163+insertADT :: forall t name. BuildableADT t name => InsertADT t name
164+insertADT =
165+ gginsert @'K.Sum @name @(ADTRep t) @(ADT t Insert) ADT
166+
167+
139168type ConstructableADT :: K.Rel8able -> Constraint
140169class GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
141170instance GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
@@ -161,16 +190,6 @@ deconstructADT =
161190 ggdeconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) @r (\(ADT a) -> a)
162191
163192
164−type InsertADT :: K.Rel8able -> Type
165−type InsertADT t = forall r. GGInsert 'K.Sum (ADTRep t) r
166−
167−
168−insertADT :: forall t. ConstructableADT t => InsertADT t -> ADT t Insert
169−insertADT f =
170− gginsert @'K.Sum @(ADTRep t) @(ADT t Insert) ADT
171− (f @(ADT t Insert))
172−
173−
174193type NameADT :: K.Rel8able -> Type
175194type NameADT t = GGName 'K.Sum (ADTRep t) (ADT t Name)
176195
src/Rel8/Table/HKD.hs+31−13
@@ -14,10 +14,12 @@
1414module Rel8.Table.HKD
1515 ( HKD( HKD )
1616 , HKDable, fromHKD, toHKD, HKDT(..)
17+ , BuildableHKD
18+ , BuildHKD, buildHKD
19+ , InsertHKD, insertHKD
1720 , ConstructableHKD
1821 , ConstructHKD, constructHKD
1922 , DeconstructHKD, deconstructHKD
20− , InsertHKD, insertHKD
2123 , NameHKD, nameHKD
2224 , AggregateHKD, aggregateHKD
2325 , HKDRep
@@ -30,6 +32,7 @@ import Data.Proxy ( Proxy( Proxy ) )
3032import Data.Type.Equality ( (:~:)( Refl ) )
3133import Data.Void ( Void )
3234import GHC.Generics ( Generic, Rep, from, to )
35+import GHC.TypeLits ( Symbol )
3336import Prelude
3437
3538-- rel8
@@ -39,10 +42,12 @@ import Rel8.Expr ( Expr )
3942import Rel8.FCF ( Eval, Exp )
4043import Rel8.Kind.Algebra ( KnownAlgebra )
4144import Rel8.Generic.Construction
42− ( GGConstructable
45+ ( GGBuildable
46+ , GGBuild, ggbuild
47+ , GGInsert, gginsert
48+ , GGConstructable
4349 , GGConstruct, ggconstruct
4450 , GGDeconstruct, ggdeconstruct
45− , GGInsert, gginsert
4651 , GGName, ggname
4752 , GGAggregate, ggaggregate
4853 )
@@ -204,6 +209,29 @@ instance
204209 => HKDable a
205210
206211
212+type BuildableHKD :: Type -> Symbol -> Constraint
213+class GGBuildable (GAlgebra (Rep a)) name (HKDRep a) => BuildableHKD a name
214+instance GGBuildable (GAlgebra (Rep a)) name (HKDRep a) => BuildableHKD a name
215+
216+
217+type BuildHKD :: Type -> Symbol -> Type
218+type BuildHKD a name = GGBuild (GAlgebra (Rep a)) name (HKDRep a) (HKD a Expr)
219+
220+
221+buildHKD :: forall a name. BuildableHKD a name => BuildHKD a name
222+buildHKD =
223+ ggbuild @(GAlgebra (Rep a)) @name @(HKDRep a) @(HKD a Expr) HKD
224+
225+
226+type InsertHKD :: Type -> Symbol -> Type
227+type InsertHKD a name = GGInsert (GAlgebra (Rep a)) name (HKDRep a) (HKD a Insert)
228+
229+
230+insertHKD :: forall a name. BuildableHKD a name => InsertHKD a name
231+insertHKD =
232+ gginsert @(GAlgebra (Rep a)) @name @(HKDRep a) @(HKD a Insert) HKD
233+
234+
207235type ConstructableHKD :: Type -> Constraint
208236class GGConstructable (GAlgebra (Rep a)) (HKDRep a) => ConstructableHKD a
209237instance GGConstructable (GAlgebra (Rep a)) (HKDRep a) => ConstructableHKD a
@@ -228,16 +256,6 @@ deconstructHKD :: forall a r. (ConstructableHKD a, Table Expr r)
228256deconstructHKD = ggdeconstruct @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Expr) @r (\(HKD a) -> a)
229257
230258
231−type InsertHKD :: Type -> Type
232−type InsertHKD a = forall r. GGInsert (GAlgebra (Rep a)) (HKDRep a) r
233−
234−
235−insertHKD :: forall a. ConstructableHKD a => InsertHKD a -> HKD a Insert
236−insertHKD f =
237− gginsert @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Insert) HKD
238− (f @(HKD a Insert))
239−
240−
241259type NameHKD :: Type -> Type
242260type NameHKD a = GGName (GAlgebra (Rep a)) (HKDRep a) (HKD a Name)
243261