git.iko.soy/rel8
on master help sign in
Make constructHKD work the same for product and sum types
ae2ce41Shane O'Brien
src/Rel8/Generic/Construction.hs+16−17
compare with master
unifiedsplit
@@ -120,19 +120,17 @@ type family GGConstructable' algebra rep where
120
120
121
121
122type GGConstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
122type GGConstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
123−type family GGConstruct algebra rep a where
123+type family GGConstruct algebra rep r where
124− GGConstruct 'K.Product rep a = GConstruct TUnreify (Eval (rep (Reify Expr))) a
124+ GGConstruct 'K.Product rep r = GConstruct TUnreify (Eval (rep (Reify Expr))) r -> r
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
125+ GGConstruct 'K.Sum rep r = GConstructADT TUnreify (Eval (rep (Reify Expr))) r r
128− GConstructADT TUnreify (Eval (rep (Reify Expr))) a a -> a
129
126
130
127
131ggconstruct :: forall algebra rep a. GGConstructable algebra rep
128ggconstruct :: forall algebra rep a. GGConstructable algebra rep
132 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr) -> a)
129 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr) -> a)
133− -> GGConstruct algebra rep a
130+ -> GGConstruct algebra rep a -> a
134−ggconstruct gfromColumns = case algebraSing @algebra of
131+ggconstruct gfromColumns f = case algebraSing @algebra of
135 SProduct ->
132 SProduct ->
133+ f $
136 gtabulate @TUnreify @(Eval (rep (Reify Expr))) @a $
134 gtabulate @TUnreify @(Eval (rep (Reify Expr))) @a $
137 gfromColumns .
135 gfromColumns .
138 hunreify .
136 hunreify .
@@ -143,7 +141,7 @@ ggconstruct gfromColumns = case algebraSing @algebra of
143 @(Col (Reify Expr))
141 @(Col (Reify Expr))
144 @(Eval (rep (Reify Expr)))
142 @(Eval (rep (Reify Expr)))
145 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
143 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
146− SSum -> \f ->
144+ SSum ->
147 gcindex @TUnreify @(Eval (rep (Reify Expr))) @a f $
145 gcindex @TUnreify @(Eval (rep (Reify Expr))) @a f $
148 fmap (gfromColumns . hunreify) $
146 fmap (gfromColumns . hunreify) $
149 gconstructADT
147 gconstructADT
@@ -207,19 +205,20 @@ ggdeconstruct gtoColumns = case algebraSing @algebra of
207
205
208
206
209type GGInsert :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
207type GGInsert :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
210−type family GGInsert algebra rep a where
208+type family GGInsert algebra rep r where
209+ GGInsert 'K.Product rep r =
211− GGInsert 'K.Product rep a = GConstruct TUnreify (Eval (rep (Reify Insert))) a
210+ GConstruct TUnreify (Eval (rep (Reify Insert))) r -> r
212− GGInsert 'K.Sum rep a =
211+ GGInsert 'K.Sum rep r =
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
212+ GConstructADT TUnreify (Eval (rep (Reify Insert))) r r
215− GConstructADT TUnreify (Eval (rep (Reify Insert))) a a -> a
216
213
217
214
218gginsert :: forall algebra rep a. GGConstructable algebra rep
215gginsert :: forall algebra rep a. GGConstructable algebra rep
219 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Insert) -> a)
216 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Insert) -> a)
220 -> GGInsert algebra rep a
217 -> GGInsert algebra rep a
218+ -> a
221−gginsert gfromColumns = case algebraSing @algebra of
219+gginsert gfromColumns f = case algebraSing @algebra of
222 SProduct ->
220 SProduct ->
221+ f $
223 gtabulate @TUnreify @(Eval (rep (Reify Insert))) @a $
222 gtabulate @TUnreify @(Eval (rep (Reify Insert))) @a $
224 gfromColumns .
223 gfromColumns .
225 hunreify .
224 hunreify .
@@ -230,7 +229,7 @@ gginsert gfromColumns = case algebraSing @algebra of
230 @(Col (Reify Insert))
229 @(Col (Reify Insert))
231 @(Eval (rep (Reify Insert)))
230 @(Eval (rep (Reify Insert)))
232 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
231 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
233− SSum -> \f ->
232+ SSum ->
234 gcindex @TUnreify @(Eval (rep (Reify Insert))) @a f $
233 gcindex @TUnreify @(Eval (rep (Reify Insert))) @a f $
235 fmap (gfromColumns . hunreify) $
234 fmap (gfromColumns . hunreify) $
236 gconstructADT
235 gconstructADT
src/Rel8/Table/ADT.hs+12−7
@@ -142,11 +142,13 @@ instance GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
142
142
143
143
144type ConstructADT :: K.Rel8able -> Type
144type ConstructADT :: K.Rel8able -> Type
145−type ConstructADT t = GGConstruct 'K.Sum (ADTRep t) (ADT t Expr)
145+type ConstructADT t = forall r. GGConstruct 'K.Sum (ADTRep t) r
146
146
147
147
148−constructADT :: forall t. ConstructableADT t => ConstructADT t
148+constructADT :: forall t. ConstructableADT t => ConstructADT t -> ADT t Expr
149+constructADT f =
149−constructADT = ggconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) ADT
150+ ggconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) ADT
151+ (f @(ADT t Expr))
150
152
151
153
152type DeconstructADT :: K.Rel8able -> Type -> Type
154type DeconstructADT :: K.Rel8able -> Type -> Type
@@ -155,15 +157,18 @@ type DeconstructADT t r = GGDeconstruct 'K.Sum (ADTRep t) (ADT t Expr) r
155
157
156deconstructADT :: forall t r. (ConstructableADT t, Table Expr r)
158deconstructADT :: forall t r. (ConstructableADT t, Table Expr r)
157 => DeconstructADT t r
159 => DeconstructADT t r
160+deconstructADT =
158−deconstructADT = ggdeconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) @r (\(ADT a) -> a)
161+ ggdeconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) @r (\(ADT a) -> a)
159
162
160
163
161type InsertADT :: K.Rel8able -> Type
164type InsertADT :: K.Rel8able -> Type
162−type InsertADT t = GGInsert 'K.Sum (ADTRep t) (ADT t Insert)
165+type InsertADT t = forall r. GGInsert 'K.Sum (ADTRep t) r
163
166
164
167
165−insertADT :: forall t. ConstructableADT t => InsertADT t
168+insertADT :: forall t. ConstructableADT t => InsertADT t -> ADT t Insert
169+insertADT f =
166−insertADT = gginsert @'K.Sum @(ADTRep t) @(ADT t Insert) ADT
170+ gginsert @'K.Sum @(ADTRep t) @(ADT t Insert) ADT
171+ (f @(ADT t Insert))
167
172
168
173
169type NameADT :: K.Rel8able -> Type
174type NameADT :: K.Rel8able -> Type
src/Rel8/Table/HKD.hs+10−6
@@ -210,11 +210,13 @@ instance GGConstructable (GAlgebra (Rep a)) (HKDRep a) => ConstructableHKD a
210
210
211
211
212type ConstructHKD :: Type -> Type
212type ConstructHKD :: Type -> Type
213−type ConstructHKD a = GGConstruct (GAlgebra (Rep a)) (HKDRep a) (HKD a Expr)
213+type ConstructHKD a = forall r. GGConstruct (GAlgebra (Rep a)) (HKDRep a) r
214
214
215
215
216−constructHKD :: forall a. ConstructableHKD a => ConstructHKD a
216+constructHKD :: forall a. ConstructableHKD a => ConstructHKD a -> HKD a Expr
217+constructHKD f =
217−constructHKD = ggconstruct @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Expr) HKD
218+ ggconstruct @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Expr) HKD
219+ (f @(HKD a Expr))
218
220
219
221
220type DeconstructHKD :: Type -> Type -> Type
222type DeconstructHKD :: Type -> Type -> Type
@@ -227,11 +229,13 @@ deconstructHKD = ggdeconstruct @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Expr) @r
227
229
228
230
229type InsertHKD :: Type -> Type
231type InsertHKD :: Type -> Type
230−type InsertHKD a = GGInsert (GAlgebra (Rep a)) (HKDRep a) (HKD a Insert)
232+type InsertHKD a = forall r. GGInsert (GAlgebra (Rep a)) (HKDRep a) r
231
233
232
234
233−insertHKD :: forall a. ConstructableHKD a => InsertHKD a
235+insertHKD :: forall a. ConstructableHKD a => InsertHKD a -> HKD a Insert
236+insertHKD f =
234−insertHKD = gginsert @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Insert) HKD
237+ gginsert @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Insert) HKD
238+ (f @(HKD a Insert))
235
239
236
240
237type NameHKD :: Type -> Type
241type NameHKD :: Type -> Type