git.iko.soy/rel8
on master help sign in
Make constructHKD work the same for product and sum types
commitae2ce41f862140124ee2f0b52259ab9bb52632f8 authorShane O'Brien <shane.obrien@circuithub.com> dateThu 10 Jun 2021, 19:37 (5 years ago) parentbdf2d87
3 files changed+38−30
compare with master
unifiedsplit
src/Rel8/Generic/Construction.hs+16−17 src/Rel8/Table/ADT.hs+12−7 src/Rel8/Table/HKD.hs+10−6
src/Rel8/Generic/Construction.hs+16−17
@@ -120,19 +120,17 @@ type family GGConstructable' algebra rep where
120120
121121
122122type 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
123+type 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
129126
130127
131128ggconstruct :: forall algebra rep a. GGConstructable algebra rep
132129 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr) -> a)
133− -> GGConstruct algebra rep a
134−ggconstruct gfromColumns = case algebraSing @algebra of
130+ -> GGConstruct algebra rep a -> a
131+ggconstruct gfromColumns f = case algebraSing @algebra of
135132 SProduct ->
133+ f $
136134 gtabulate @TUnreify @(Eval (rep (Reify Expr))) @a $
137135 gfromColumns .
138136 hunreify .
@@ -143,7 +141,7 @@ ggconstruct gfromColumns = case algebraSing @algebra of
143141 @(Col (Reify Expr))
144142 @(Eval (rep (Reify Expr)))
145143 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
146− SSum -> \f ->
144+ SSum ->
147145 gcindex @TUnreify @(Eval (rep (Reify Expr))) @a f $
148146 fmap (gfromColumns . hunreify) $
149147 gconstructADT
@@ -207,19 +205,20 @@ ggdeconstruct gtoColumns = case algebraSing @algebra of
207205
208206
209207type 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
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
216213
217214
218215gginsert :: forall algebra rep a. GGConstructable algebra rep
219216 => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Insert) -> a)
220217 -> GGInsert algebra rep a
221−gginsert gfromColumns = case algebraSing @algebra of
218+ -> a
219+gginsert gfromColumns f = case algebraSing @algebra of
222220 SProduct ->
221+ f $
223222 gtabulate @TUnreify @(Eval (rep (Reify Insert))) @a $
224223 gfromColumns .
225224 hunreify .
@@ -230,7 +229,7 @@ gginsert gfromColumns = case algebraSing @algebra of
230229 @(Col (Reify Insert))
231230 @(Eval (rep (Reify Insert)))
232231 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
233− SSum -> \f ->
232+ SSum ->
234233 gcindex @TUnreify @(Eval (rep (Reify Insert))) @a f $
235234 fmap (gfromColumns . hunreify) $
236235 gconstructADT
src/Rel8/Table/ADT.hs+12−7
@@ -142,11 +142,13 @@ instance GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t
142142
143143
144144type 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
146146
147147
148−constructADT :: forall t. ConstructableADT t => ConstructADT t
149−constructADT = ggconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) ADT
148+constructADT :: forall t. ConstructableADT t => ConstructADT t -> ADT t Expr
149+constructADT f =
150+ ggconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) ADT
151+ (f @(ADT t Expr))
150152
151153
152154type DeconstructADT :: K.Rel8able -> Type -> Type
@@ -155,15 +157,18 @@ type DeconstructADT t r = GGDeconstruct 'K.Sum (ADTRep t) (ADT t Expr) r
155157
156158deconstructADT :: forall t r. (ConstructableADT t, Table Expr r)
157159 => DeconstructADT t r
158−deconstructADT = ggdeconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) @r (\(ADT a) -> a)
160+deconstructADT =
161+ ggdeconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) @r (\(ADT a) -> a)
159162
160163
161164type 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
163166
164167
165−insertADT :: forall t. ConstructableADT t => InsertADT t
166−insertADT = gginsert @'K.Sum @(ADTRep t) @(ADT t Insert) ADT
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))
167172
168173
169174type NameADT :: K.Rel8able -> Type
src/Rel8/Table/HKD.hs+10−6
@@ -210,11 +210,13 @@ instance GGConstructable (GAlgebra (Rep a)) (HKDRep a) => ConstructableHKD a
210210
211211
212212type 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
214214
215215
216−constructHKD :: forall a. ConstructableHKD a => ConstructHKD a
217−constructHKD = ggconstruct @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Expr) HKD
216+constructHKD :: forall a. ConstructableHKD a => ConstructHKD a -> HKD a Expr
217+constructHKD f =
218+ ggconstruct @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Expr) HKD
219+ (f @(HKD a Expr))
218220
219221
220222type DeconstructHKD :: Type -> Type -> Type
@@ -227,11 +229,13 @@ deconstructHKD = ggdeconstruct @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Expr) @r
227229
228230
229231type 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
231233
232234
233−insertHKD :: forall a. ConstructableHKD a => InsertHKD a
234−insertHKD = gginsert @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Insert) HKD
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))
235239
236240
237241type NameHKD :: Type -> Type