git.iko.soy/rel8
on master help sign in
Don't try to cram ADT into Rel8able
cfe8a70Shane O'Brien
src/Rel8.hs+2−2
compare with master
unifiedsplit
@@ -106,7 +106,7 @@ module Rel8
106 , some
106 , some
107
107
108 -- ** @ADT@
108 -- ** @ADT@
109− , ADT
109+ , ADT, ADTable
110 , ConstructADT, constructADT
110 , ConstructADT, constructADT
111 , DeconstructADT, deconstructADT
111 , DeconstructADT, deconstructADT
112 , InsertADT, insertADT
112 , InsertADT, insertADT
@@ -114,7 +114,7 @@ module Rel8
114 , AggregateADT, aggregateADT
114 , AggregateADT, aggregateADT
115
115
116 -- ** @HKD@
116 -- ** @HKD@
117− , HKD
117+ , HKD, HKDable
118 , ConstructHKD, constructHKD
118 , ConstructHKD, constructHKD
119 , DeconstructHKD, deconstructHKD
119 , DeconstructHKD, deconstructHKD
120 , InsertHKD, insertHKD
120 , InsertHKD, insertHKD
src/Rel8/Column.hs+6
@@ -4,6 +4,7 @@
4
4
5module Rel8.Column
5module Rel8.Column
6 ( Column, Default
6 ( Column, Default
7+ , TColumn
7 )
8 )
8where
9where
9
10
@@ -13,6 +14,7 @@ import Prelude ()
13
14
14-- rel8
15-- rel8
15import Rel8.Column.Field ( Field )
16import Rel8.Column.Field ( Field )
17+import Rel8.FCF ( Eval, Exp )
16import Rel8.Kind.Necessity ( Necessity( Required, Optional ) )
18import Rel8.Kind.Necessity ( Necessity( Required, Optional ) )
17import qualified Rel8.Schema.Kind as K
19import qualified Rel8.Schema.Kind as K
18
20
@@ -27,3 +29,7 @@ type Column context a = Field context 'Required a
27
29
28type Default :: K.Context -> Type -> Type
30type Default :: K.Context -> Type -> Type
29type Default context a = Field context 'Optional a
31type Default context a = Field context 'Optional a
32+
33+
34+data TColumn :: K.Context -> Type -> Exp Type
35+type instance Eval (TColumn f a) = Column f a
src/Rel8/Column/ADT.hs+11−15
@@ -15,11 +15,7 @@ import Data.Kind ( Type )
15import Prelude
15import Prelude
16
16
17-- rel8
17-- rel8
18−import Rel8.Generic.Rel8able
18+import Rel8.Generic.Rel8able ( GColumns )
19− ( Rel8able
20− , GColumnsADT, gfromColumnsADT, gtoColumnsADT
21− , greify, gunreify
22− )
23import Rel8.Kind.Context ( SContext(..), Reifiable, contextSing )
19import Rel8.Kind.Context ( SContext(..), Reifiable, contextSing )
24import Rel8.Schema.Context ( Col )
20import Rel8.Schema.Context ( Col )
25import qualified Rel8.Schema.Kind as K
21import qualified Rel8.Schema.Kind as K
@@ -29,7 +25,7 @@ import Rel8.Table
29 ( Table, Columns, Context, fromColumns, toColumns
25 ( Table, Columns, Context, fromColumns, toColumns
30 , Unreify, reify, unreify
26 , Unreify, reify, unreify
31 )
27 )
32−import Rel8.Table.ADT ( ADT( ADT ) )
28+import Rel8.Table.ADT ( ADT( ADT ), ADTable, fromADT, toADT )
33import Rel8.Table.Recontextualize ( Recontextualize )
29import Rel8.Table.Recontextualize ( Recontextualize )
34
30
35
31
@@ -44,11 +40,11 @@ type AHADT :: K.Context -> K.Rel8able -> Type
44newtype AHADT context t = AHADT (HADT context t)
40newtype AHADT context t = AHADT (HADT context t)
45
41
46
42
47−instance (Rel8able t, Reifiable context) =>
43+instance (ADTable t, Reifiable context) =>
48 Table (Reify context) (AHADT context t)
44 Table (Reify context) (AHADT context t)
49 where
45 where
50 type Context (AHADT context t) = Reify context
46 type Context (AHADT context t) = Reify context
51− type Columns (AHADT context t) = GColumnsADT t
47+ type Columns (AHADT context t) = GColumns (ADT t)
52 type Unreify (AHADT context t) = HADT context t
48 type Unreify (AHADT context t) = HADT context t
53
49
54 fromColumns = sfromColumnsADT contextSing
50 fromColumns = sfromColumnsADT contextSing
@@ -59,7 +55,7 @@ instance (Rel8able t, Reifiable context) =>
59
55
60instance
56instance
61 ( Reifiable context, Reifiable context'
57 ( Reifiable context, Reifiable context'
62− , Rel8able t, t ~ t'
58+ , ADTable t, t ~ t'
63 )
59 )
64 => Recontextualize
60 => Recontextualize
65 (Reify context)
61 (Reify context)
@@ -68,27 +64,27 @@ instance
68 (AHADT context' t')
64 (AHADT context' t')
69
65
70
66
71−sfromColumnsADT :: Rel8able t
67+sfromColumnsADT :: ADTable t
72 => SContext context
68 => SContext context
73− -> GColumnsADT t (Col (Reify context))
69+ -> GColumns (ADT t) (Col (Reify context))
74 -> AHADT context t
70 -> AHADT context t
75sfromColumnsADT = \case
71sfromColumnsADT = \case
76 SAggregate -> AHADT . ADT . hunreify
72 SAggregate -> AHADT . ADT . hunreify
77 SExpr -> AHADT . ADT . hunreify
73 SExpr -> AHADT . ADT . hunreify
78 SInsert -> AHADT . ADT . hunreify
74 SInsert -> AHADT . ADT . hunreify
79 SName -> AHADT . ADT . hunreify
75 SName -> AHADT . ADT . hunreify
80− SResult -> AHADT . gunreify . gfromColumnsADT
76+ SResult -> AHADT . fromADT . ADT . hunreify
81 SReify context -> AHADT . sfromColumnsADT context . hunreify
77 SReify context -> AHADT . sfromColumnsADT context . hunreify
82
78
83
79
84−stoColumnsADT :: Rel8able t
80+stoColumnsADT :: ADTable t
85 => SContext context
81 => SContext context
86 -> AHADT context t
82 -> AHADT context t
87− -> GColumnsADT t (Col (Reify context))
83+ -> GColumns (ADT t) (Col (Reify context))
88stoColumnsADT = \case
84stoColumnsADT = \case
89 SAggregate -> hreify . (\(AHADT (ADT a)) -> a)
85 SAggregate -> hreify . (\(AHADT (ADT a)) -> a)
90 SExpr -> hreify . (\(AHADT (ADT a)) -> a)
86 SExpr -> hreify . (\(AHADT (ADT a)) -> a)
91 SInsert -> hreify . (\(AHADT (ADT a)) -> a)
87 SInsert -> hreify . (\(AHADT (ADT a)) -> a)
92 SName -> hreify . (\(AHADT (ADT a)) -> a)
88 SName -> hreify . (\(AHADT (ADT a)) -> a)
93− SResult -> gtoColumnsADT . greify . (\(AHADT a) -> a)
89+ SResult -> hreify . (\(ADT a) -> a) . toADT . (\(AHADT a) -> a)
94 SReify context -> hreify . stoColumnsADT context . (\(AHADT a) -> a)
90 SReify context -> hreify . stoColumnsADT context . (\(AHADT a) -> a)
src/Rel8/Column/Lift.hs+5−5
@@ -25,7 +25,7 @@ import Rel8.Table
25 , Unreify, reify, unreify
25 , Unreify, reify, unreify
26 )
26 )
27import Rel8.Table.Rel8able ()
27import Rel8.Table.Rel8able ()
28−import Rel8.Table.HKD ( HKD( HKD ), GHKD, fromHKD, toHKD )
28+import Rel8.Table.HKD ( HKD( HKD ), HKDable, fromHKD, toHKD )
29import Rel8.Table.Recontextualize ( Recontextualize )
29import Rel8.Table.Recontextualize ( Recontextualize )
30
30
31
31
@@ -42,7 +42,7 @@ newtype ALift context a = ALift
42 }
42 }
43
43
44
44
45−instance (Reifiable context, GHKD a) =>
45+instance (Reifiable context, HKDable a) =>
46 Table (Reify context) (ALift context a)
46 Table (Reify context) (ALift context a)
47 where
47 where
48 type Context (ALift context a) = Reify context
48 type Context (ALift context a) = Reify context
@@ -55,7 +55,7 @@ instance (Reifiable context, GHKD a) =>
55 unreify _ (ALift a) = a
55 unreify _ (ALift a) = a
56
56
57
57
58−instance (Reifiable context, Reifiable context', GHKD a) =>
58+instance (Reifiable context, Reifiable context', HKDable a) =>
59 Recontextualize
59 Recontextualize
60 (Reify context)
60 (Reify context)
61 (Reify context')
61 (Reify context')
@@ -63,7 +63,7 @@ instance (Reifiable context, Reifiable context', GHKD a) =>
63 (ALift context' a)
63 (ALift context' a)
64
64
65
65
66−sfromColumnsLift :: GHKD a
66+sfromColumnsLift :: HKDable a
67 => SContext context
67 => SContext context
68 -> GColumns (HKD a) (Col (Reify context))
68 -> GColumns (HKD a) (Col (Reify context))
69 -> ALift context a
69 -> ALift context a
@@ -76,7 +76,7 @@ sfromColumnsLift = \case
76 SReify context -> ALift . sfromColumnsLift context . hunreify
76 SReify context -> ALift . sfromColumnsLift context . hunreify
77
77
78
78
79−stoColumnsLift :: GHKD a
79+stoColumnsLift :: HKDable a
80 => SContext context
80 => SContext context
81 -> ALift context a
81 -> ALift context a
82 -> GColumns (HKD a) (Col (Reify context))
82 -> GColumns (HKD a) (Col (Reify context))
src/Rel8/Generic/Rel8able.hs+20−97
@@ -14,8 +14,7 @@ module Rel8.Generic.Rel8able
14 ( KRel8able, Rel8able
14 ( KRel8able, Rel8able
15 , Algebra
15 , Algebra
16 , GRep
16 , GRep
17− , GColumns, GContext, gfromColumns, gtoColumns
17+ , GColumns, gfromColumns, gtoColumns
18− , GColumnsADT, gfromColumnsADT, gtoColumnsADT
19 , greify, gunreify
18 , greify, gunreify
20 , TUnreifyContext
19 , TUnreifyContext
21 )
20 )
@@ -33,18 +32,14 @@ import Rel8.Kind.Context ( Reifiable )
33import Rel8.FCF ( Eval, Exp )
32import Rel8.FCF ( Eval, Exp )
34import Rel8.Generic.Map ( GMap, GMappable, gmap, gunmap )
33import Rel8.Generic.Map ( GMap, GMappable, gmap, gunmap )
35import Rel8.Generic.Record ( Record(..) )
34import Rel8.Generic.Record ( Record(..) )
36−import Rel8.Generic.Table
35+import Rel8.Generic.Table ( GAlgebra )
37− ( GGTable, GGColumns, GGContext, ggfromColumns, ggtoColumns
38− , GAlgebra
39− )
40−import qualified Rel8.Generic.Table.ADT as G
36+import qualified Rel8.Generic.Table.Record as G
41−import Rel8.Kind.Algebra ( KnownAlgebra )
42import qualified Rel8.Kind.Algebra as K ( Algebra(..) )
37import qualified Rel8.Kind.Algebra as K ( Algebra(..) )
43import Rel8.Schema.Context ( Col )
38import Rel8.Schema.Context ( Col )
44import Rel8.Schema.Context.Label ( Labelable )
39import Rel8.Schema.Context.Label ( Labelable )
45import Rel8.Schema.HTable ( HTable )
40import Rel8.Schema.HTable ( HTable )
46import qualified Rel8.Schema.Kind as K
41import qualified Rel8.Schema.Kind as K
47−import Rel8.Schema.Reify ( Col( Reify ), Reify, UnwrapReify )
42+import Rel8.Schema.Reify ( Reify, UnwrapReify )
48import Rel8.Schema.Result ( Result )
43import Rel8.Schema.Result ( Result )
49import Rel8.Table
44import Rel8.Table
50 ( fromColumns, toColumns, reify, unreify
45 ( fromColumns, toColumns, reify, unreify
@@ -99,123 +94,48 @@ type KRel8able = K.Rel8able
99-- deriving ( GHC.Generics.Generic, Rel8able )
94-- deriving ( GHC.Generics.Generic, Rel8able )
100-- @
95-- @
101type Rel8able :: K.Rel8able -> Constraint
96type Rel8able :: K.Rel8able -> Constraint
102−class
103− ( HTable (GColumns t)
97+class HTable (GColumns t) => Rel8able t where
104− , HTable (GColumnsADT t)
105− , GContext t Result ~ Result
106− )
107− => Rel8able t
108− where
109− type Algebra t :: K.Algebra
110−
111− type GRep t (context :: K.Context) :: Type -> Type
112−
113 type GColumns t :: K.HTable
98 type GColumns t :: K.HTable
114
99
115− type GContext t (context :: K.Context) :: K.Context
116−
117− gfromColumns :: (Labelable context, Reifiable context, GContext t context ~ context)
100+ gfromColumns :: (Labelable context, Reifiable context)
118 => GColumns t (Col (Reify context)) -> t (Reify context)
101 => GColumns t (Col (Reify context)) -> t (Reify context)
119
102
120− gtoColumns :: (Labelable context, Reifiable context, GContext t context ~ context)
103+ gtoColumns :: (Labelable context, Reifiable context)
121 => t (Reify context) -> GColumns t (Col (Reify context))
104 => t (Reify context) -> GColumns t (Col (Reify context))
122
105
123− gfromColumnsADT :: GColumnsADT t (Col (Reify Result)) -> t (Reify Result)
124−
125− gtoColumnsADT :: t (Reify Result) -> GColumnsADT t (Col (Reify Result))
126−
127 greify :: (Labelable context, Reifiable context)
106 greify :: (Labelable context, Reifiable context)
128 => t context -> t (Reify context)
107 => t context -> t (Reify context)
129
108
130 gunreify :: (Labelable context, Reifiable context)
109 gunreify :: (Labelable context, Reifiable context)
131 => t (Reify context) -> t context
110 => t (Reify context) -> t context
132
111
133− type Algebra t = GAlgebra (GRep t (Reify Result))
134−
135− type GRep t context = Rep (Record (t context))
136−
137− type GColumns t = Eval (GGColumns (Algebra t) TColumns (GRep t (Reify Result)))
112+ type GColumns t = G.GColumns TColumns (GRep t (Reify Result))
138−
139− type GContext t context =
140− Eval (GGContext (Algebra t) TUnreifyContext (GRep t (Reify context)))
141
113
142 default gfromColumns :: forall context.
114 default gfromColumns :: forall context.
143 ( Generic (Record (t (Reify context)))
115 ( Generic (Record (t (Reify context)))
144− , GRep t (Reify context) ~ Rep (Record (t (Reify context)))
145− , KnownAlgebra (Algebra t)
146− , Eval (GGTable (Algebra t) (TTable (Reify context)) TColumns (Col (Reify context)) (GRep t (Reify context)))
116+ , G.GTable (TTable (Reify context)) TColumns (Col (Reify context)) (GRep t (Reify context))
147− , Eval (GGColumns (Algebra t) TColumns (GRep t (Reify context))) ~ GColumns t
117+ , G.GColumns TColumns (GRep t (Reify context)) ~ GColumns t
148− , Eval (GGContext (Algebra t) TUnreifyContext (GRep t (Reify context))) ~ context
149 )
118 )
150 => GColumns t (Col (Reify context)) -> t (Reify context)
119 => GColumns t (Col (Reify context)) -> t (Reify context)
151 gfromColumns =
120 gfromColumns =
152 unrecord .
121 unrecord .
153 to .
122 to .
154− ggfromColumns
155− @(Algebra t)
156− @(TTable (Reify context))
123+ G.gfromColumns @(TTable (Reify context)) @TColumns fromColumns
157− @TColumns
158− (\(Reify a) -> a)
159− Reify
160− fromColumns
161
124
162 default gtoColumns :: forall context.
125 default gtoColumns :: forall context.
163 ( Generic (Record (t (Reify context)))
126 ( Generic (Record (t (Reify context)))
164− , GRep t (Reify context) ~ Rep (Record (t (Reify context)))
165− , KnownAlgebra (Algebra t)
166− , Eval (GGTable (Algebra t) (TTable (Reify context)) TColumns (Col (Reify context)) (GRep t (Reify context)))
127+ , G.GTable (TTable (Reify context)) TColumns (Col (Reify context)) (GRep t (Reify context))
167− , Eval (GGColumns (Algebra t) TColumns (GRep t (Reify context))) ~ GColumns t
128+ , G.GColumns TColumns (GRep t (Reify context)) ~ GColumns t
168− , Eval (GGContext (Algebra t) TUnreifyContext (GRep t (Reify context))) ~ context
169 )
129 )
170 => t (Reify context) -> GColumns t (Col (Reify context))
130 => t (Reify context) -> GColumns t (Col (Reify context))
171 gtoColumns =
131 gtoColumns =
172− ggtoColumns
173− @(Algebra t)
174− @(TTable (Reify context))
132+ G.gtoColumns @(TTable (Reify context)) @TColumns toColumns .
175− @TColumns
176− (\(Reify a) -> a)
177− Reify
178− toColumns .
179− from .
180− Record
181−
182− default gfromColumnsADT ::
183− ( Generic (Record (t (Reify Result)))
184− , GRep t (Reify Result) ~ Rep (Record (t (Reify Result)))
185− , G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRep t (Reify Result))
186− )
187− => GColumnsADT t (Col (Reify Result)) -> t (Reify Result)
188− gfromColumnsADT =
189− unrecord .
190− to .
191− G.gfromColumnsADT
192− @(TTable (Reify Result))
193− @TColumns
194− (\(Reify a) -> a)
195− Reify
196− fromColumns
197−
198− default gtoColumnsADT ::
199− ( Generic (Record (t (Reify Result)))
200− , GRep t (Reify Result) ~ Rep (Record (t (Reify Result)))
201− , G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRep t (Reify Result))
202− )
203− => t (Reify Result) -> GColumnsADT t (Col (Reify Result))
204− gtoColumnsADT =
205− G.gtoColumnsADT
206− @(TTable (Reify Result))
207− @TColumns
208− (\(Reify a) -> a)
209− Reify
210− toColumns .
211 from .
133 from .
212 Record
134 Record
213
135
214 default greify :: forall context.
136 default greify :: forall context.
215 ( Generic (Record (t context))
137 ( Generic (Record (t context))
216− , GRep t context ~ Rep (Record (t context))
217 , Generic (Record (t (Reify context)))
138 , Generic (Record (t (Reify context)))
218− , GRep t (Reify context) ~ Rep (Record (t (Reify context)))
219 , GMappable (TTable (Reify context)) (GRep t (Reify context))
139 , GMappable (TTable (Reify context)) (GRep t (Reify context))
220 , GRep t context ~ GMap TUnreify (GRep t (Reify context))
140 , GRep t context ~ GMap TUnreify (GRep t (Reify context))
221 )
141 )
@@ -229,9 +149,7 @@ class
229
149
230 default gunreify :: forall context.
150 default gunreify :: forall context.
231 ( Generic (Record (t context))
151 ( Generic (Record (t context))
232− , GRep t context ~ Rep (Record (t context))
233 , Generic (Record (t (Reify context)))
152 , Generic (Record (t (Reify context)))
234− , GRep t (Reify context) ~ Rep (Record (t (Reify context)))
235 , GMappable (TTable (Reify context)) (GRep t (Reify context))
153 , GMappable (TTable (Reify context)) (GRep t (Reify context))
236 , GRep t context ~ GMap TUnreify (GRep t (Reify context))
154 , GRep t context ~ GMap TUnreify (GRep t (Reify context))
237 )
155 )
@@ -244,7 +162,12 @@ class
244 Record
162 Record
245
163
246
164
247−type GColumnsADT t = G.GColumnsADT TColumns (GRep t (Reify Result))
165+type Algebra :: K.Rel8able -> K.Algebra
166+type Algebra t = GAlgebra (GRep t (Reify Result))
167+
168+
169+type GRep :: K.Rel8able -> K.Context -> Type -> Type
170+type GRep t context = Rep (Record (t context))
248
171
249
172
250data TUnreifyContext :: Type -> Exp K.Context
173data TUnreifyContext :: Type -> Exp K.Context
src/Rel8/Generic/Rel8able/Test.hs−1
@@ -129,7 +129,6 @@ data TableSum f
129 | TableSumB
129 | TableSumB
130 | TableSumC (Column f Text)
130 | TableSumC (Column f Text)
131 deriving stock Generic
131 deriving stock Generic
132− deriving anyclass Rel8able
133
132
134
133
135data TableProduct f = TableProduct
134data TableProduct f = TableProduct
src/Rel8/Table/ADT.hs+80−15
@@ -12,6 +12,7 @@
12
12
13module Rel8.Table.ADT
13module Rel8.Table.ADT
14 ( ADT( ADT )
14 ( ADT( ADT )
15+ , ADTable, fromADT, toADT
15 , ConstructableADT
16 , ConstructableADT
16 , ConstructADT, constructADT
17 , ConstructADT, constructADT
17 , DeconstructADT, deconstructADT
18 , DeconstructADT, deconstructADT
@@ -24,7 +25,10 @@ where
24
25
25-- base
26-- base
26import Data.Kind ( Constraint, Type )
27import Data.Kind ( Constraint, Type )
28+import Data.Proxy ( Proxy( Proxy ) )
29+import Data.Type.Equality ( (:~:)( Refl ) )
30+import GHC.Generics ( Generic, Rep, from, to )
27−import Prelude ()
31+import Prelude
28
32
29-- rel8
33-- rel8
30import Rel8.Aggregate ( Aggregate )
34import Rel8.Aggregate ( Aggregate )
@@ -38,43 +42,100 @@ import Rel8.Generic.Construction
38 , GGName, ggname
42 , GGName, ggname
39 , GGAggregate, ggaggregate
43 , GGAggregate, ggaggregate
40 )
44 )
45+import Rel8.Generic.Map ( GMappable, GMap, gmap, gunmap )
46+import Rel8.Generic.Record ( GRecordable, GRecord, grecord, gunrecord )
41import Rel8.Generic.Rel8able
47import Rel8.Generic.Rel8able
42− ( Rel8able, Algebra
48+ ( Rel8able
43− , GRep, GColumns, GContext, gfromColumns, gtoColumns
49+ , GRep, GColumns, gfromColumns, gtoColumns
44− , GColumnsADT, gfromColumnsADT, gtoColumnsADT
45 , greify, gunreify
50 , greify, gunreify
46 )
51 )
52+import qualified Rel8.Generic.Table.ADT as G
47import qualified Rel8.Kind.Algebra as K
53import qualified Rel8.Kind.Algebra as K
48import Rel8.Schema.Context ( Col )
54import Rel8.Schema.Context ( Col )
55+import Rel8.Schema.HTable ( HTable )
49import Rel8.Schema.Insert ( Insert )
56import Rel8.Schema.Insert ( Insert )
50import qualified Rel8.Schema.Kind as K
57import qualified Rel8.Schema.Kind as K
51import Rel8.Schema.Name ( Name )
58import Rel8.Schema.Name ( Name )
52−import Rel8.Schema.Reify ( hreify, hunreify )
59+import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify )
53−import Rel8.Table ( Table )
60+import Rel8.Schema.Result ( Result )
61+import Rel8.Table
62+ ( Table
63+ , fromColumns, toColumns, reify, unreify
64+ , TTable, TColumns, TUnreify
65+ )
54
66
55
67
56type ADT :: K.Rel8able -> K.Rel8able
68type ADT :: K.Rel8able -> K.Rel8able
57newtype ADT t context = ADT (GColumnsADT t (Col context))
69newtype ADT t context = ADT (GColumnsADT t (Col context))
58
70
59
71
60−instance Rel8able t => Rel8able (ADT t) where
72+instance ADTable t => Rel8able (ADT t) where
61− type Algebra (ADT t) = 'K.Product
62−
63− type GRep (ADT t) context = GRep t context
64−
65 type GColumns (ADT t) = GColumnsADT t
73 type GColumns (ADT t) = GColumnsADT t
66− type GContext (ADT t) context = context
67
74
68 gfromColumns = ADT
75 gfromColumns = ADT
69 gtoColumns (ADT a) = a
76 gtoColumns (ADT a) = a
70
77
71− gfromColumnsADT = ADT
72− gtoColumnsADT (ADT a) = a
73−
74 greify (ADT a) = ADT (hreify a)
78 greify (ADT a) = ADT (hreify a)
75 gunreify (ADT a) = ADT (hunreify a)
79 gunreify (ADT a) = ADT (hunreify a)
76
80
77
81
82+instance (ADTable t, context ~ Result) => Generic (ADT t context) where
83+ type Rep (ADT t context) = Rep (t context)
84+
85+ from =
86+ gmap @(TTable (Reify Result)) (Proxy @TUnreify) (unreify Refl) .
87+ gunrecord @(Rep (t (Reify Result))) .
88+ G.gfromColumnsADT
89+ @(TTable (Reify Result))
90+ @TColumns
91+ (\(Reify a) -> a)
92+ Reify
93+ fromColumns .
94+ hreify .
95+ (\(ADT a) -> a)
96+
97+ to =
98+ ADT .
99+ hunreify .
100+ G.gtoColumnsADT
101+ @(TTable (Reify Result))
102+ @TColumns
103+ (\(Reify a) -> a)
104+ Reify
105+ toColumns .
106+ grecord @(Rep (t (Reify Result))) .
107+ gunmap @(TTable (Reify Result)) (Proxy @TUnreify) (reify Refl)
108+
109+
110+fromADT :: ADTable t => ADT t Result -> t Result
111+fromADT = to . from
112+
113+
114+toADT :: ADTable t => t Result -> ADT t Result
115+toADT = to . from
116+
117+
118+type ADTable :: K.Rel8able -> Constraint
119+class
120+ ( Generic (t Result)
121+ , HTable (GColumnsADT t)
122+ , G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (Rep (t (Reify Result))))
123+ , GRecordable (Rep (t (Reify Result)))
124+ , GMappable (TTable (Reify Result)) (Rep (t (Reify Result)))
125+ , GMap TUnreify (Rep (t (Reify Result))) ~ Rep (t Result)
126+ )
127+ => ADTable t
128+instance
129+ ( Generic (t Result)
130+ , HTable (GColumnsADT t)
131+ , G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (Rep (t (Reify Result))))
132+ , GRecordable (Rep (t (Reify Result)))
133+ , GMappable (TTable (Reify Result)) (Rep (t (Reify Result)))
134+ , GMap TUnreify (Rep (t (Reify Result))) ~ Rep (t Result)
135+ )
136+ => ADTable t
137+
138+
78type ConstructableADT :: K.Rel8able -> Constraint
139type ConstructableADT :: K.Rel8able -> Constraint
79class GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
140class GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
80instance GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
141instance GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
@@ -126,3 +187,7 @@ aggregateADT f =
126
187
127data ADTRep :: K.Rel8able -> K.Context -> Exp (Type -> Type)
188data ADTRep :: K.Rel8able -> K.Context -> Exp (Type -> Type)
128type instance Eval (ADTRep t context) = GRep t context
189type instance Eval (ADTRep t context) = GRep t context
190+
191+
192+type GColumnsADT :: K.Rel8able -> K.HTable
193+type GColumnsADT t = G.GColumnsADT TColumns (GRep t (Reify Result))
src/Rel8/Table/HKD.hs+10−64
@@ -13,7 +13,7 @@
13
13
14module Rel8.Table.HKD
14module Rel8.Table.HKD
15 ( HKD( HKD )
15 ( HKD( HKD )
16− , HKDT(..), fromHKD, toHKD, GHKD
16+ , HKDable, fromHKD, toHKD, HKDT(..)
17 , ConstructableHKD
17 , ConstructableHKD
18 , ConstructHKD, constructHKD
18 , ConstructHKD, constructHKD
19 , DeconstructHKD, deconstructHKD
19 , DeconstructHKD, deconstructHKD
@@ -33,11 +33,10 @@ import Prelude
33
33
34-- rel8
34-- rel8
35import Rel8.Aggregate ( Aggregate )
35import Rel8.Aggregate ( Aggregate )
36−import Rel8.Column ( Column )
36+import Rel8.Column ( TColumn )
37import Rel8.Expr ( Expr )
37import Rel8.Expr ( Expr )
38import Rel8.FCF ( Eval, Exp )
38import Rel8.FCF ( Eval, Exp )
39import Rel8.Kind.Algebra ( KnownAlgebra )
39import Rel8.Kind.Algebra ( KnownAlgebra )
40−import qualified Rel8.Kind.Algebra as K
41import Rel8.Generic.Construction
40import Rel8.Generic.Construction
42 ( GGConstructable
41 ( GGConstructable
43 , GGConstruct, ggconstruct
42 , GGConstruct, ggconstruct
@@ -49,9 +48,8 @@ import Rel8.Generic.Construction
49import Rel8.Generic.Map ( GMap, GMappable, gmap, gunmap )
48import Rel8.Generic.Map ( GMap, GMappable, gmap, gunmap )
50import Rel8.Generic.Record ( GRecord, GRecordable, grecord, gunrecord )
49import Rel8.Generic.Record ( GRecord, GRecordable, grecord, gunrecord )
51import Rel8.Generic.Rel8able
50import Rel8.Generic.Rel8able
52− ( Rel8able, Algebra
51+ ( Rel8able
53− , GRep, GColumns, GContext, gfromColumns, gtoColumns
52+ , GColumns, gfromColumns, gtoColumns
54− , GColumnsADT, gfromColumnsADT, gtoColumnsADT
55 , greify, gunreify
53 , greify, gunreify
56 , TUnreifyContext
54 , TUnreifyContext
57 )
55 )
@@ -59,7 +57,6 @@ import Rel8.Generic.Table
59 ( GGTable, GGColumns, GGContext, ggfromColumns, ggtoColumns
57 ( GGTable, GGColumns, GGContext, ggfromColumns, ggtoColumns
60 , GAlgebra
58 , GAlgebra
61 )
59 )
62−import qualified Rel8.Generic.Table.ADT as G
63import Rel8.Schema.Context ( Col )
60import Rel8.Schema.Context ( Col )
64import qualified Rel8.Schema.Kind as K
61import qualified Rel8.Schema.Kind as K
65import Rel8.Schema.HTable ( HTable )
62import Rel8.Schema.HTable ( HTable )
@@ -75,10 +72,6 @@ import Rel8.Table
75import Rel8.Table.Serialize ( ToExprs, fromResult, toResult )
72import Rel8.Table.Serialize ( ToExprs, fromResult, toResult )
76
73
77
74
78−data TColumn :: K.Context -> Type -> Exp Type
79−type instance Eval (TColumn f a) = Column f a
80−
81−
82type GColumnsHKD :: Type -> K.HTable
75type GColumnsHKD :: Type -> K.HTable
83type GColumnsHKD a =
76type GColumnsHKD a =
84 Eval (GGColumns (GAlgebra (Rep a)) TColumns (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
77 Eval (GGColumns (GAlgebra (Rep a)) TColumns (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
@@ -88,53 +81,12 @@ type HKD :: Type -> K.Rel8able
88newtype HKD a f = HKD (GColumnsHKD a (Col f))
81newtype HKD a f = HKD (GColumnsHKD a (Col f))
89
82
90
83
91−instance GHKD a => Rel8able (HKD a) where
84+instance HKDable a => Rel8able (HKD a) where
92− type Algebra (HKD a) = 'K.Product
93−
94− type GRep (HKD a) f = GRecord (GMap (TColumn f) (Rep a))
95−
96 type GColumns (HKD a) = GColumnsHKD a
85 type GColumns (HKD a) = GColumnsHKD a
97− type GContext (HKD a) context = context
98
86
99 gfromColumns = HKD
87 gfromColumns = HKD
100 gtoColumns (HKD a) = a
88 gtoColumns (HKD a) = a
101
89
102− gfromColumnsADT =
103− HKD .
104− ggtoColumns
105− @(GAlgebra (Rep a))
106− @(TTable (Reify Result))
107− @TColumns
108− (\(Reify a) -> a)
109− Reify
110− toColumns .
111− G.gfromColumnsADT
112− @(TTable (Reify Result))
113− @TColumns
114− @(Col (Reify Result))
115− @(GRep (HKD a) (Reify Result))
116− (\(Reify a) -> a)
117− Reify
118− fromColumns
119−
120− gtoColumnsADT =
121− G.gtoColumnsADT
122− @(TTable (Reify Result))
123− @TColumns
124− @(Col (Reify Result))
125− @(GRep (HKD a) (Reify Result))
126− (\(Reify a) -> a)
127− Reify
128− toColumns .
129− ggfromColumns
130− @(GAlgebra (Rep a))
131− @(TTable (Reify Result))
132− @TColumns
133− (\(Reify a) -> a)
134− Reify
135− fromColumns .
136− (\(HKD a) -> a)
137−
138 greify (HKD a) = HKD (hreify a)
90 greify (HKD a) = HKD (hreify a)
139 gunreify (HKD a) = HKD (hunreify a)
91 gunreify (HKD a) = HKD (hunreify a)
140
92
@@ -189,7 +141,7 @@ newtype HKDT a = HKDT
189instance
141instance
190 ( Table Expr (HKD a Expr)
142 ( Table Expr (HKD a Expr)
191 , Columns (HKD a Expr) ~ GColumns (HKD a)
143 , Columns (HKD a Expr) ~ GColumns (HKD a)
192− , GHKD a
144+ , HKDable a
193 , x ~ HKD a Expr
145 , x ~ HKD a Expr
194 )
146 )
195 => ToExprs x (HKDT a)
147 => ToExprs x (HKDT a)
@@ -198,11 +150,11 @@ instance
198 fromResult = HKDT . fromHKD . HKD
150 fromResult = HKDT . fromHKD . HKD
199
151
200
152
201−fromHKD :: GHKD a => HKD a Result -> a
153+fromHKD :: HKDable a => HKD a Result -> a
202fromHKD = to . gunmap @Top (Proxy @(TColumn Result)) id . from
154fromHKD = to . gunmap @Top (Proxy @(TColumn Result)) id . from
203
155
204
156
205−toHKD :: GHKD a => a -> HKD a Result
157+toHKD :: HKDable a => a -> HKD a Result
206toHKD = to . gmap @Top (Proxy @(TColumn Result)) id . from
158toHKD = to . gmap @Top (Proxy @(TColumn Result)) id . from
207
159
208
160
@@ -217,33 +169,27 @@ type instance Eval (Top _) = Top_
217class
169class
218 ( Generic a
170 ( Generic a
219 , HTable (GColumns (HKD a))
171 , HTable (GColumns (HKD a))
220− , HTable (GColumnsADT (HKD a))
221 , KnownAlgebra (GAlgebra (Rep a))
172 , KnownAlgebra (GAlgebra (Rep a))
222 , Eval (GGTable (GAlgebra (Rep a)) (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
173 , Eval (GGTable (GAlgebra (Rep a)) (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
223− , Eval (GGColumns (GAlgebra (Rep a)) TColumns (GRecord (GMap (TColumn (Reify Result)) (Rep a)))) ~ GColumnsHKD a
224 , Eval (GGContext (GAlgebra (Rep a)) TUnreifyContext (GRecord (GMap (TColumn (Reify Result)) (Rep a)))) ~ Result
174 , Eval (GGContext (GAlgebra (Rep a)) TUnreifyContext (GRecord (GMap (TColumn (Reify Result)) (Rep a)))) ~ Result
225− , G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (GMap (TColumn (Reify Result)) (Rep a)))
226 , GRecordable (GMap (TColumn (Reify Result)) (Rep a))
175 , GRecordable (GMap (TColumn (Reify Result)) (Rep a))
227 , GMappable Top (Rep a)
176 , GMappable Top (Rep a)
228 , GMappable (TTable (Reify Result)) (GMap (TColumn (Reify Result)) (Rep a))
177 , GMappable (TTable (Reify Result)) (GMap (TColumn (Reify Result)) (Rep a))
229 , GMap TUnreify (GMap (TColumn (Reify Result)) (Rep a)) ~ GMap (TColumn Result) (Rep a)
178 , GMap TUnreify (GMap (TColumn (Reify Result)) (Rep a)) ~ GMap (TColumn Result) (Rep a)
230 )
179 )
231− => GHKD a
180+ => HKDable a
232instance
181instance
233 ( Generic a
182 ( Generic a
234 , HTable (GColumns (HKD a))
183 , HTable (GColumns (HKD a))
235− , HTable (GColumnsADT (HKD a))
236 , KnownAlgebra (GAlgebra (Rep a))
184 , KnownAlgebra (GAlgebra (Rep a))
237 , Eval (GGTable (GAlgebra (Rep a)) (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
185 , Eval (GGTable (GAlgebra (Rep a)) (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
238− , Eval (GGColumns (GAlgebra (Rep a)) TColumns (GRecord (GMap (TColumn (Reify Result)) (Rep a)))) ~ GColumnsHKD a
239 , Eval (GGContext (GAlgebra (Rep a)) TUnreifyContext (GRecord (GMap (TColumn (Reify Result)) (Rep a)))) ~ Result
186 , Eval (GGContext (GAlgebra (Rep a)) TUnreifyContext (GRecord (GMap (TColumn (Reify Result)) (Rep a)))) ~ Result
240− , G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (GMap (TColumn (Reify Result)) (Rep a)))
241 , GRecordable (GMap (TColumn (Reify Result)) (Rep a))
187 , GRecordable (GMap (TColumn (Reify Result)) (Rep a))
242 , GMappable Top (Rep a)
188 , GMappable Top (Rep a)
243 , GMappable (TTable (Reify Result)) (GMap (TColumn (Reify Result)) (Rep a))
189 , GMappable (TTable (Reify Result)) (GMap (TColumn (Reify Result)) (Rep a))
244 , GMap TUnreify (GMap (TColumn (Reify Result)) (Rep a)) ~ GMap (TColumn Result) (Rep a)
190 , GMap TUnreify (GMap (TColumn (Reify Result)) (Rep a)) ~ GMap (TColumn Result) (Rep a)
245 )
191 )
246− => GHKD a
192+ => HKDable a
247
193
248
194
249type ConstructableHKD :: Type -> Constraint
195type ConstructableHKD :: Type -> Constraint
src/Rel8/Table/Rel8able.hs+14−35
@@ -29,8 +29,7 @@ import Rel8.Kind.Context
29 )
29 )
30import Rel8.Generic.Rel8able
30import Rel8.Generic.Rel8able
31 ( Rel8able, Algebra
31 ( Rel8able, Algebra
32− , GColumns, GContext, gfromColumns, gtoColumns
32+ , GColumns, gfromColumns, gtoColumns
33− , gfromColumnsADT, gtoColumnsADT
34 , greify, gunreify
33 , greify, gunreify
35 )
34 )
36import Rel8.Schema.Context ( Col )
35import Rel8.Schema.Context ( Col )
@@ -45,7 +44,7 @@ import Rel8.Table
45 , Unreify, reify, unreify
44 , Unreify, reify, unreify
46 )
45 )
47import Rel8.Schema.Spec.ConstrainDBType ( ConstrainDBType )
46import Rel8.Schema.Spec.ConstrainDBType ( ConstrainDBType )
48−import Rel8.Table.ADT ( ADT )
47+import Rel8.Table.ADT ( ADT( ADT ), ADTable, fromADT, toADT )
49import Rel8.Table.Eq ( EqTable, eqTable )
48import Rel8.Table.Eq ( EqTable, eqTable )
50import Rel8.Table.HKD ( HKD )
49import Rel8.Table.HKD ( HKD )
51import Rel8.Table.Ord ( OrdTable, ordTable )
50import Rel8.Table.Ord ( OrdTable, ordTable )
@@ -55,13 +54,8 @@ import Rel8.Type.Eq ( DBEq )
55import Rel8.Type.Ord ( DBOrd )
54import Rel8.Type.Ord ( DBOrd )
56
55
57
56
58−instance
59− ( Rel8able t
60− , GContext t context ~ context
61− , Labelable context
57+instance (Rel8able t, Labelable context, Reifiable context) =>
62− , Reifiable context
63− )
64− => Table context (t context)
58+ Table context (t context)
65 where
59 where
66 type Columns (t context) = GColumns t
60 type Columns (t context) = GColumns t
67 type Context (t context) = context
61 type Context (t context) = context
@@ -83,8 +77,8 @@ instance
83
77
84instance
78instance
85 ( Rel8able t
79 ( Rel8able t
86− , Labelable from, Reifiable from, GContext t from ~ from
80+ , Labelable from, Reifiable from
87− , Labelable to, Reifiable to, GContext t to ~ to
81+ , Labelable to, Reifiable to
88 , Congruent (t from) (t to)
82 , Congruent (t from) (t to)
89 )
83 )
90 => Recontextualize from to (t from) (t to)
84 => Recontextualize from to (t from) (t to)
@@ -93,7 +87,6 @@ instance
93instance
87instance
94 ( context ~ Expr
88 ( context ~ Expr
95 , Rel8able t
89 , Rel8able t
96− , GContext t context ~ context
97 , HConstrainTable (Columns (t context)) (ConstrainDBType DBEq)
90 , HConstrainTable (Columns (t context)) (ConstrainDBType DBEq)
98 )
91 )
99 => EqTable (t context)
92 => EqTable (t context)
@@ -104,7 +97,6 @@ instance
104instance
97instance
105 ( context ~ Expr
98 ( context ~ Expr
106 , Rel8able t
99 , Rel8able t
107− , GContext t context ~ context
108 , HConstrainTable (Columns (t context)) (ConstrainDBType DBEq)
100 , HConstrainTable (Columns (t context)) (ConstrainDBType DBEq)
109 , HConstrainTable (Columns (t context)) (ConstrainDBType DBOrd)
101 , HConstrainTable (Columns (t context)) (ConstrainDBType DBOrd)
110 )
102 )
@@ -135,35 +127,22 @@ type family FromExprs' t where
135
127
136
128
137type ToExprs' :: K.Algebra -> K.Rel8able -> K.Rel8able -> Constraint
129type ToExprs' :: K.Algebra -> K.Rel8able -> K.Rel8able -> Constraint
138−class
139− ( algebra ~ Algebra t
130+class (algebra ~ Algebra t, Rel8able t') =>
140− , Rel8able t'
141− , GContext t' Expr ~ Expr
142− )
143− => ToExprs' algebra t' t | algebra t -> t'
131+ ToExprs' algebra t' t | algebra t -> t'
144 where
132 where
145 fromResult' :: GColumns t' (Col Result) -> t Result
133 fromResult' :: GColumns t' (Col Result) -> t Result
146 toResult' :: t Result -> GColumns t' (Col Result)
134 toResult' :: t Result -> GColumns t' (Col Result)
147
135
148
136
149−instance
150− ( Algebra t ~ 'K.Product
137+instance (Algebra t ~ 'K.Product, Rel8able t, t ~ t') =>
151− , Rel8able t
152− , GContext t Expr ~ Expr
153− , t ~ t'
154− )
155− => ToExprs' 'K.Product t' t
138+ ToExprs' 'K.Product t' t
156 where
139 where
157 fromResult' = fromColumns
140 fromResult' = fromColumns
158 toResult' = toColumns
141 toResult' = toColumns
159
142
160
143
161−instance
162− ( Algebra t ~ 'K.Sum
144+instance (Algebra t ~ 'K.Sum, ADTable t, t' ~ ADT t) =>
163− , Rel8able t
164− , t' ~ ADT t
165− )
166− => ToExprs' 'K.Sum t' t
145+ ToExprs' 'K.Sum t' t
167 where
146 where
168− fromResult' = gunreify . gfromColumnsADT . hreify
147+ fromResult' = fromADT . ADT
169− toResult' = hunreify . gtoColumnsADT . greify
148+ toResult' = (\(ADT a) -> a) . toADT