@@ -1,7 +1,9 @@
1+{-# language AllowAmbiguousTypes #-}
12{-# language DataKinds #-}
23{-# language FlexibleContexts #-}
34{-# language FlexibleInstances #-}
45{-# language MultiParamTypeClasses #-}
6+{-# language RankNTypes #-}
57{-# language ScopedTypeVariables #-}
68{-# language StandaloneKindSignatures #-}
79{-# language TypeApplications #-}
@@ -10,9 +12,15 @@
1012{-# language UndecidableSuperClasses #-}
1113
1214module Rel8.Table.HKD
13− ( HKD( HKD ), HKDT(..)
14− , fromHKD, toHKD
15− , GHKD
15+ ( HKD( HKD )
16+ , HKDT(..), fromHKD, toHKD, GHKD
17+ , ConstructableHKD
18+ , ConstructHKD, constructHKD
19+ , DeconstructHKD, deconstructHKD
20+ , InsertHKD, insertHKD
21+ , NameHKD, nameHKD
22+ , AggregateHKD, aggregateHKD
23+ , HKDRep
1624 )
1725where
1826
@@ -24,11 +32,20 @@ import GHC.Generics ( Generic, Rep, from, to )
2432import Prelude
2533
2634-- rel8
35+import Rel8.Aggregate ( Aggregate )
2736import Rel8.Column ( Column )
2837import Rel8.Expr ( Expr )
2938import Rel8.FCF ( Eval, Exp )
3039import Rel8.Kind.Algebra ( KnownAlgebra )
3140import qualified Rel8.Kind.Algebra as K
41+import Rel8.Generic.Construction
42+ ( GGConstructable
43+ , GGConstruct, ggconstruct
44+ , GGDeconstruct, ggdeconstruct
45+ , GGInsert, gginsert
46+ , GGName, ggname
47+ , GGAggregate, ggaggregate
48+ )
3249import Rel8.Generic.Map ( GMap, GMappable, gmap, gunmap )
3350import Rel8.Generic.Record ( GRecord, GRecordable, grecord, gunrecord )
3451import Rel8.Generic.Rel8able
@@ -46,6 +63,8 @@ import qualified Rel8.Generic.Table.ADT as G
4663import Rel8.Schema.Context ( Col )
4764import qualified Rel8.Schema.Kind as K
4865import Rel8.Schema.HTable ( HTable )
66+import Rel8.Schema.Insert ( Insert )
67+import Rel8.Schema.Name ( Name )
4968import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify )
5069import Rel8.Schema.Result ( Result )
5170import Rel8.Table
@@ -221,3 +240,57 @@ instance
221240 , GMap TUnreify (GMap (TColumn (Reify Result)) (Rep a)) ~ GMap (TColumn Result) (Rep a)
222241 )
223242 => GHKD a
243+
244+
245+type ConstructableHKD :: Type -> Constraint
246+class GGConstructable (GAlgebra (Rep a)) (HKDRep a) => ConstructableHKD a
247+instance GGConstructable (GAlgebra (Rep a)) (HKDRep a) => ConstructableHKD a
248+
249+
250+type ConstructHKD :: Type -> Type
251+type ConstructHKD a = GGConstruct (GAlgebra (Rep a)) (HKDRep a) (HKD a Expr)
252+
253+
254+constructHKD :: forall a. ConstructableHKD a => ConstructHKD a
255+constructHKD = ggconstruct @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Expr) HKD
256+
257+
258+type DeconstructHKD :: Type -> Type -> Type
259+type DeconstructHKD a r = GGDeconstruct (GAlgebra (Rep a)) (HKDRep a) (HKD a Expr) r
260+
261+
262+deconstructHKD :: forall a r. (ConstructableHKD a, Table Expr r)
263+ => DeconstructHKD a r
264+deconstructHKD = ggdeconstruct @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Expr) @r (\(HKD a) -> a)
265+
266+
267+type InsertHKD :: Type -> Type
268+type InsertHKD a = GGInsert (GAlgebra (Rep a)) (HKDRep a) (HKD a Insert)
269+
270+
271+insertHKD :: forall a. ConstructableHKD a => InsertHKD a
272+insertHKD = gginsert @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Insert) HKD
273+
274+
275+type NameHKD :: Type -> Type
276+type NameHKD a = GGName (GAlgebra (Rep a)) (HKDRep a) (HKD a Name)
277+
278+
279+nameHKD :: forall a. ConstructableHKD a => NameHKD a
280+nameHKD = ggname @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Name) HKD
281+
282+
283+type AggregateHKD :: Type -> Type
284+type AggregateHKD a = forall r. GGAggregate (GAlgebra (Rep a)) (HKDRep a) r
285+
286+
287+aggregateHKD :: forall a. ConstructableHKD a
288+ => AggregateHKD a -> HKD a Expr -> Aggregate (HKD a Expr)
289+aggregateHKD f =
290+ ggaggregate @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Expr) HKD (\(HKD a) -> a)
291+ (f @(Aggregate (HKD a Expr)))
292+
293+
294+data HKDRep :: Type -> K.Context -> Exp (Type -> Type)
295+type instance Eval (HKDRep a context) =
296+ GRecord (GMap (TColumn context) (Rep a))