fab5b4e · rel8 · git.iko.soy

git.iko.soy/rel8

Implement our own HKD in terms of the existing Generic machinery

This `HKD` is a better fit for `Rel8` than `higgledy`'s `HKD`. In a very literal sense, this `HKD` is now a `Rel8able` (i.e., `Context -> Type`), whereas `higgledy`'s is `(Type -> Type) -> Type`. This meant we had to use hacks like `HKD a (Compose Aggregate Expr)` to get a `HKD` into the `Aggregate` context (and similarly for `Insert`). Now we can just do `HKD a Aggregate` and `HKD a Insert` like any other `Rel8able`. Like `higgledy`'s, our `HKD` is compatible with `generic-lens`. One feature we have that `higgledy` doesn't is the ability to support sum types. You can make a `HKD` out of an arbitrary algebraic data type (whose fields are `DBType`s). What's still missing is constructor/deconstructor machinery, but that's nearly finished, and the underlying machinery will also be used by the `ADT` `Rel8able`.

commitfab5b4e02d9244c4ce9aef9edfc1e995b61e4974 authorShane O'Brien <shane.obrien@circuithub.com> dateMon 3 May 2021, 03:46 (6 years ago) parent4bc16d3

11 files changed+281−399

compare with master

unifiedsplit

rel8.cabal+1−2 src/Rel8.hs+1 src/Rel8/Column/Lift.hs+20−60 src/Rel8/Generic/HKD.hs−224 src/Rel8/Generic/Record.hs+29−28 src/Rel8/Generic/Rel8able.hs+11−53 src/Rel8/Generic/Rel8able/Test.hs+10−4 src/Rel8/Generic/Table.hs+6−6 src/Rel8/Table.hs−2 src/Rel8/Table/HKD.hs+196−15 src/Rel8/Table/Rel8able.hs+7−5

rel8.cabal+1−2

@@ -17,7 +17,6 @@ library

1717 , casing

1818 , contravariant

1919 , hasql ^>= 1.4.5.1

20− , higgledy

2120 , opaleye ^>= 0.7.1.0

2221 , profunctors

2322 , scientific

@@ -27,6 +26,7 @@ library

2726 , these

2827 , time

2928 , uuid

29+ , lens, generic-lens

3030 default-language:

3131 Haskell2010

3232 ghc-options:

@@ -78,7 +78,6 @@ library

7878 Rel8.Kind.Labels

7979 Rel8.Kind.Necessity

8080

81− Rel8.Generic.HKD

8281 Rel8.Generic.Map

8382 Rel8.Generic.Record

8483 Rel8.Generic.Reify

src/Rel8.hs+1

@@ -246,6 +246,7 @@ module Rel8

246246 , ToExprs(..)

247247 , FromExprs

248248 , Result

249+ , HKD

249250 , HKDT(..)

250251 ) where

251252

src/Rel8/Column/Lift.hs+20−60

@@ -1,12 +1,8 @@

11{-# language DataKinds #-}

2−{-# language FlexibleContexts #-}

32{-# language LambdaCase #-}

43{-# language MultiParamTypeClasses #-}

5−{-# language ScopedTypeVariables #-}

64{-# language StandaloneKindSignatures #-}

7−{-# language TypeApplications #-}

85{-# language TypeFamilies #-}

9−{-# language UndecidableInstances #-}

106

117module Rel8.Column.Lift

128 ( Lift, ALift(..)

@@ -14,41 +10,30 @@ module Rel8.Column.Lift

1410where

1511

1612-- base

17−import Data.Functor.Compose ( Compose(..) )

18−import Data.Functor.Identity ( Identity(..), runIdentity )

1913import Data.Kind ( Type )

20−import GHC.Generics ( Rep )

2114import Prelude

2215

23−-- higgledy

24−import Data.Generic.HKD ( Construct, HKD(..), construct, deconstruct )

25−

2616-- rel8

27−import Rel8.Aggregate ( Col(..), Aggregate )

28−import Rel8.Expr ( Expr )

29−import Rel8.Generic.HKD ( GTable, GColumns, gfromColumns, gtoColumns )

17+import Rel8.Generic.Rel8able ( GColumns )

3018import Rel8.Kind.Context ( Reifiable(..), SContext(..) )

31−import Rel8.Schema.HTable.Type ( HType( HType ) )

32−import Rel8.Schema.Insert ( Insert, Col(..) )

19+import Rel8.Schema.Context ( Col )

3320import qualified Rel8.Schema.Kind as K

34−import Rel8.Schema.Name ( Name(..) )

3521import Rel8.Schema.Reify ( Reify, hreify, hunreify )

3622import Rel8.Schema.Result ( Result )

3723import Rel8.Table

3824 ( Table, Columns, Context, fromColumns, toColumns

3925 , Unreify, reify, unreify

4026 )

27+import Rel8.Table.Rel8able ()

28+import Rel8.Table.HKD ( HKD( HKD ), GHKD, fromHKD, toHKD )

4129import Rel8.Table.Recontextualize ( Recontextualize )

4230

4331

4432type Lift :: K.Context -> Type -> Type

4533type family Lift context a where

4634 Lift (Reify context) a = ALift context a

47− Lift Aggregate a = HKD a (Compose Aggregate Expr)

48− Lift Expr a = HKD a Expr

49− Lift Insert a = HKD a Expr

50− Lift Name a = HKD a Name

5135 Lift Result a = a

36+ Lift context a = HKD a context

5237

5338

5439type ALift :: K.Context -> Type -> Type

@@ -57,15 +42,11 @@ newtype ALift context a = ALift

5742 }

5843

5944

60−instance

61− ( Reifiable context

62− , GTable (Rep a)

63− , Construct Identity a

64− )

65− => Table (Reify context) (ALift context a)

45+instance (Reifiable context, GHKD a) =>

46+ Table (Reify context) (ALift context a)

6647 where

6748 type Context (ALift context a) = Reify context

68− type Columns (ALift context a) = GColumns (Rep a)

49+ type Columns (ALift context a) = GColumns (HKD a)

6950 type Unreify (ALift context a) = Lift context a

7051

7152 fromColumns = sfromColumnsLift contextSing

@@ -74,56 +55,35 @@ instance

7455 unreify _ (ALift a) = a

7556

7657

77−instance

78− ( Reifiable context

79− , Reifiable context'

80− , GTable (Rep a)

81− , Construct Identity a

82− )

83− => Recontextualize

58+instance (Reifiable context, Reifiable context', GHKD a) =>

59+ Recontextualize

8460 (Reify context)

8561 (Reify context')

8662 (ALift context a)

8763 (ALift context' a)

8864

8965

90−sfromColumnsLift :: forall a context. (GTable (Rep a), Construct Identity a)

66+sfromColumnsLift :: GHKD a

9167 => SContext context

92− -> GColumns (Rep a) (Col (Reify context))

68+ -> GColumns (HKD a) (Col (Reify context))

9369 -> ALift context a

9470sfromColumnsLift = \case

95− SAggregate ->

96− ALift .

97− HKD .

98− gfromColumns (\(HType (Aggregation a)) -> Compose a) .

99− hunreify

71+ SAggregate -> ALift . fromColumns . hunreify

10072 SExpr -> ALift . fromColumns . hunreify

101− SInsert ->

102− ALift .

103− HKD .

104− gfromColumns (\(HType (RequiredInsert a)) -> a) .

105− hunreify

73+ SInsert -> ALift . fromColumns . hunreify

10674 SName -> ALift . fromColumns . hunreify

107− SResult -> ALift . runIdentity . construct . fromColumns . hunreify

75+ SResult -> ALift . fromHKD . HKD . hunreify

10876 SReify context -> ALift . sfromColumnsLift context . hunreify

10977

11078

111−stoColumnsLift :: forall a context. (GTable (Rep a), Construct Identity a)

79+stoColumnsLift :: GHKD a

11280 => SContext context

11381 -> ALift context a

114− -> GColumns (Rep a) (Col (Reify context))

82+ -> GColumns (HKD a) (Col (Reify context))

11583stoColumnsLift = \case

116− SAggregate ->

117− hreify .

118− gtoColumns (\(Compose a) -> HType (Aggregation a)) .

119− runHKD .

120− unALift

84+ SAggregate -> hreify . toColumns . unALift

12185 SExpr -> hreify . toColumns . unALift

122− SInsert ->

123− hreify .

124− gtoColumns (HType . RequiredInsert) .

125− runHKD .

126− unALift

86+ SInsert -> hreify . toColumns . unALift

12787 SName -> hreify . toColumns . unALift

128− SResult -> hreify . toColumns . deconstruct @Identity . unALift

88+ SResult -> hreify . (\(HKD a) -> a) . toHKD . unALift

12989 SReify context -> hreify . stoColumnsLift context . unALift

src/Rel8/Generic/HKD.hsdeleted−224

@@ -1,224 +0,0 @@

1−{-# language DataKinds #-}

2−{-# language FlexibleContexts #-}

3−{-# language FlexibleInstances #-}

4−{-# language FunctionalDependencies #-}

5−{-# language QuantifiedConstraints #-}

6−{-# language RankNTypes #-}

7−{-# language ScopedTypeVariables #-}

8−{-# language StandaloneKindSignatures #-}

9−{-# language TypeApplications #-}

10−{-# language TypeFamilies #-}

11−{-# language TypeOperators #-}

12−{-# language UndecidableInstances #-}

13−{-# language UndecidableSuperClasses #-}

14−

15−{-# options -Wno-orphans #-}

16−

17−module Rel8.Generic.HKD

18− ( GTable, GColumns, gfromColumns, gtoColumns

19− )

20−where

21−

22−-- base

23−import Data.Kind ( Constraint, Type )

24−import GHC.Generics

25− ( (:*:)( (:*:) ), K1( K1 ), M1( M1 ), C, D, S, Meta( MetaSel )

26− , Rep

27− )

28−import GHC.TypeLits ( KnownSymbol )

29−import Prelude

30−

31−-- higgledy

32−import Data.Generic.HKD ( HKD(..), GHKD_ )

33−

34−-- rel8

35−import Rel8.Aggregate ( Col(..) )

36−import Rel8.Expr ( Expr )

37−import Rel8.Schema.Context.Label

38− ( Labelable

39− , HLabelable, hlabeler, hunlabeler

40− )

41−import Rel8.Schema.Dict ( Dict( Dict ) )

42−import Rel8.Schema.HTable ( HTable, HConstrainTable, hdicts )

43−import Rel8.Schema.HTable.Label ( HLabel, hlabel, hunlabel )

44−import Rel8.Schema.HTable.Product ( HProduct( HProduct ) )

45−import Rel8.Schema.HTable.Type ( HType )

46−import qualified Rel8.Schema.Kind as K

47−import Rel8.Schema.Null ( Sql )

48−import Rel8.Schema.Reify ( NotReify, notReify )

49−import Rel8.Schema.Spec.ConstrainDBType ( ConstrainDBType )

50−import Rel8.Table

51− ( Table, Columns, Context, fromColumns, toColumns

52− , reify, unreify

53− )

54−import Rel8.Table.Eq ( EqTable, eqTable )

55−import Rel8.Table.Ord ( OrdTable, ordTable )

56−import Rel8.Table.Recontextualize ( Recontextualize )

57−import Rel8.Type ( DBType )

58−import Rel8.Type.Eq ( DBEq )

59−import Rel8.Type.Ord ( DBOrd )

60−

61−

62−type Column1Helper :: K.Context -> (Type -> Type) -> Type -> Constraint

63−class

64− ( Table context (f a)

65− , Context1 f ~ context

66− , Context (f a) ~ context

67− , Columns (f a) ~ HType a

68− )

69− => Column1Helper context f a | f -> context

70−instance

71− ( Table context (f a)

72− , Context1 f ~ context

73− , Context (f a) ~ context

74− , Columns (f a) ~ HType a

75− )

76− => Column1Helper context f a

77−

78−

79−type Column1 :: K.Context -> (Type -> Type) -> Constraint

80−class

81− ( forall a. Sql DBType a => Column1Helper context f a

82− , Context1 f ~ context

83− )

84− => Column1 context f | f -> context

85−instance

86− ( forall a. Sql DBType a => Column1Helper context f a

87− , Context1 f ~ context

88− )

89− => Column1 context f

90−

91−

92−type Context1 :: (Type -> Type) -> K.Context

93−type Context1 f = Context (f Bool)

94−

95−

96−toColumn1 :: forall a f context. (Column1 context f, Sql DBType a)

97− => f a -> HType a (Col context)

98−toColumn1 = case Dict @(Column1Helper context f) @a of

99− Dict -> toColumns

100−

101−

102−fromColumn1 :: forall a f context. (Column1 context f, Sql DBType a)

103− => HType a (Col context) -> f a

104−fromColumn1 = case Dict @(Column1Helper context f) @a of

105− Dict -> fromColumns

106−

107−

108−type Recontextualize1

109− :: K.Context

110− -> K.Context

111− -> (Type -> Type)

112− -> (Type -> Type)

113− -> Constraint

114−class Recontextualize context context' (f Bool) (f' Bool) =>

115− Recontextualize1 context context' f f'

116−instance Recontextualize context context' (f Bool) (f' Bool) =>

117− Recontextualize1 context context' f f'

118−

119−

120−class HTable (GColumns rep) => GTable rep where

121− gtoColumns :: HLabelable context

122− => (forall a. Sql DBType a => f a -> HType a context)

123− -> GHKD_ f rep x

124− -> GColumns rep context

125− gfromColumns :: HLabelable context

126− => (forall a. Sql DBType a => HType a context -> f a)

127− -> GColumns rep context

128− -> GHKD_ f rep x

129−

130−

131−instance GTable rep => GTable (M1 D c rep) where

132− gtoColumns f (M1 a) = gtoColumns f a

133− {-# INLINABLE gtoColumns #-}

134−

135− gfromColumns f = M1 . gfromColumns f

136− {-# INLINABLE gfromColumns #-}

137−

138−

139−instance GTable rep => GTable (M1 C c rep) where

140− gtoColumns f (M1 a) = gtoColumns f a

141− {-# INLINABLE gtoColumns #-}

142−

143− gfromColumns f = M1 . gfromColumns f

144− {-# INLINABLE gfromColumns #-}

145−

146−

147−instance (KnownSymbol name, Sql DBType a) =>

148− GTable (M1 S ('MetaSel ('Just name) _su _ss _ds) (K1 i a))

149− where

150− gtoColumns f (M1 (K1 a)) = hlabel hlabeler (f a)

151− {-# INLINABLE gtoColumns #-}

152−

153− gfromColumns f a = M1 (K1 (f (hunlabel hunlabeler a)))

154− {-# INLINABLE gfromColumns #-}

155−

156−

157−instance (GTable f, GTable g) => GTable (f :*: g) where

158− gtoColumns f (x :*: y) = HProduct (gtoColumns f x) (gtoColumns f y)

159− {-# INLINABLE gtoColumns #-}

160−

161− gfromColumns f (HProduct x y) = gfromColumns f x :*: gfromColumns f y

162− {-# INLINABLE gfromColumns #-}

163−

164−

165−type GColumns :: (Type -> Type) -> K.HTable

166−type family GColumns rep where

167− GColumns (M1 D _ f) = GColumns f

168− GColumns (M1 C _ f) = GColumns f

169− GColumns (M1 S ('MetaSel ('Just name) _ _ _) (K1 _ a)) =

170− HLabel name (HType a)

171− GColumns (f :*: g) = HProduct (GColumns f) (GColumns g)

172−

173−

174−instance

175− ( GTable (Rep a)

176− , Column1 context f

177− , Labelable context

178− , NotReify context

179− )

180− => Table context (HKD a f)

181− where

182− type Columns (HKD a f) = GColumns (Rep a)

183− type Context (HKD a f) = Context1 f

184−

185− toColumns = gtoColumns toColumn1 . runHKD

186− fromColumns = HKD . gfromColumns fromColumn1

187− reify = notReify

188− unreify = notReify

189−

190−

191−instance

192− ( GTable (Rep a)

193− , f ~ Expr

194− , HConstrainTable (GColumns (Rep a)) (ConstrainDBType DBEq)

195− )

196− => EqTable (HKD a f)

197− where

198− eqTable = hdicts @(GColumns (Rep a)) @(ConstrainDBType DBEq)

199−

200−

201−instance

202− ( GTable (Rep a)

203− , f ~ Expr

204− , HConstrainTable (GColumns (Rep a)) (ConstrainDBType DBEq)

205− , HConstrainTable (GColumns (Rep a)) (ConstrainDBType DBOrd)

206− )

207− => OrdTable (HKD a f)

208− where

209− ordTable = hdicts @(GColumns (Rep a)) @(ConstrainDBType DBOrd)

210−

211−

212−instance

213− ( a ~ a'

214− , GTable (Rep a)

215− , NotReify context, NotReify context'

216− , Recontextualize1 context context' f f'

217− , Column1 context f, Labelable context

218− , Column1 context' f', Labelable context'

219− )

220− => Recontextualize

221− context

222− context'

223− (HKD a f)

224− (HKD a' f')

src/Rel8/Generic/Record.hs+29−28

@@ -12,6 +12,7 @@

1212

1313module Rel8.Generic.Record

1414 ( Record(..)

15+ , GRecordable, GRecord, grecord, gunrecord

1516 )

1617where

1718

@@ -26,13 +27,13 @@ import GHC.TypeLits ( type (+), AppendSymbol, Div, Mod, Nat, Symbol )

2627import Prelude hiding ( Show )

2728

2829

29−type Recordize :: (Type -> Type) -> Type -> Type

30−type family Recordize rep where

31− Recordize (M1 D meta rep) = M1 D meta (Recordize rep)

32− Recordize (l :+: r) = Recordize l :+: Recordize r

33− Recordize (M1 C ('MetaCons name fixity 'False) rep) =

30+type GRecord :: (Type -> Type) -> Type -> Type

31+type family GRecord rep where

32+ GRecord (M1 D meta rep) = M1 D meta (GRecord rep)

33+ GRecord (l :+: r) = GRecord l :+: GRecord r

34+ GRecord (M1 C ('MetaCons name fixity 'False) rep) =

3435 M1 C ('MetaCons name fixity 'True) (Snd (Count 0 rep))

35− Recordize rep = rep

36+ GRecord rep = rep

3637

3738

3839type Count :: Nat -> (Type -> Type) -> (Nat, Type -> Type)

@@ -83,34 +84,34 @@ type family Snd tuple where

8384 Snd '(_a, b) = b

8485

8586

86−type Recordizable :: (Type -> Type) -> Constraint

87−class Recordizable rep where

88− recordize :: rep x -> Recordize rep x

89− unrecordize :: Recordize rep x -> rep x

87+type GRecordable :: (Type -> Type) -> Constraint

88+class GRecordable rep where

89+ grecord :: rep x -> GRecord rep x

90+ gunrecord :: GRecord rep x -> rep x

9091

9192

92−instance Recordizable rep => Recordizable (M1 D meta rep) where

93− recordize (M1 a) = M1 (recordize a)

94− unrecordize (M1 a) = M1 (unrecordize a)

93+instance GRecordable rep => GRecordable (M1 D meta rep) where

94+ grecord (M1 a) = M1 (grecord a)

95+ gunrecord (M1 a) = M1 (gunrecord a)

9596

9697

97−instance (Recordizable l, Recordizable r) => Recordizable (l :+: r) where

98− recordize (L1 a) = L1 (recordize a)

99− recordize (R1 a) = R1 (recordize a)

100− unrecordize (L1 a) = L1 (unrecordize a)

101− unrecordize (R1 a) = R1 (unrecordize a)

98+instance (GRecordable l, GRecordable r) => GRecordable (l :+: r) where

99+ grecord (L1 a) = L1 (grecord a)

100+ grecord (R1 a) = R1 (grecord a)

101+ gunrecord (L1 a) = L1 (gunrecord a)

102+ gunrecord (R1 a) = R1 (gunrecord a)

102103

103104

104105instance Countable 0 rep =>

105− Recordizable (M1 C ('MetaCons name fixity 'False) rep)

106+ GRecordable (M1 C ('MetaCons name fixity 'False) rep)

106107 where

107− recordize (M1 a) = M1 (count @0 a)

108− unrecordize (M1 a) = M1 (uncount @0 a)

108+ grecord (M1 a) = M1 (count @0 a)

109+ gunrecord (M1 a) = M1 (uncount @0 a)

109110

110111

111−instance {-# OVERLAPPABLE #-} Recordize rep ~ rep => Recordizable rep where

112− recordize = id

113− unrecordize = id

112+instance {-# OVERLAPPABLE #-} GRecord rep ~ rep => GRecordable rep where

113+ grecord = id

114+ gunrecord = id

114115

115116

116117type Countable :: Nat -> (Type -> Type) -> Constraint

@@ -145,8 +146,8 @@ newtype Record a = Record

145146 }

146147

147148

148−instance (Generic a, Recordizable (Rep a)) => Generic (Record a) where

149− type Rep (Record a) = Recordize (Rep a)

149+instance (Generic a, GRecordable (Rep a)) => Generic (Record a) where

150+ type Rep (Record a) = GRecord (Rep a)

150151

151− from (Record a) = recordize (from a)

152− to = Record . to . unrecordize

152+ from (Record a) = grecord (from a)

153+ to = Record . to . gunrecord

src/Rel8/Generic/Rel8able.hs+11−53

@@ -1,5 +1,4 @@

11{-# language AllowAmbiguousTypes #-}

2−{-# language ConstraintKinds #-}

32{-# language DataKinds #-}

43{-# language DefaultSignatures #-}

54{-# language FlexibleContexts #-}

@@ -18,6 +17,7 @@ module Rel8.Generic.Rel8able

1817 , GColumns, GContext, gfromColumns, gtoColumns

1918 , GColumnsADT, gfromColumnsADT, gtoColumnsADT

2019 , greify, gunreify

20+ , TUnreifyContext

2121 )

2222where

2323

@@ -38,16 +38,12 @@ import Rel8.Generic.Table

3838 , GAlgebra

3939 )

4040import qualified Rel8.Generic.Table.ADT as G

41−import Rel8.Kind.Algebra

42− ( SAlgebra( SProduct, SSum )

43− , KnownAlgebra, algebraSing

44− )

41+import Rel8.Kind.Algebra ( KnownAlgebra )

4542import qualified Rel8.Kind.Algebra as K ( Algebra(..) )

4643import Rel8.Schema.Context ( Col )

4744import Rel8.Schema.Context.Label ( Labelable )

4845import Rel8.Schema.HTable ( HTable )

4946import qualified Rel8.Schema.Kind as K

50−import Rel8.Schema.Name ( Name )

5147import Rel8.Schema.Reify ( Col( Reify ), Reify, UnwrapReify )

5248import Rel8.Schema.Result ( Result )

5349import Rel8.Table

@@ -134,11 +130,11 @@ class

134130 gunreify :: (Labelable context, Reifiable context)

135131 => t (Reify context) -> t context

136132

137− type Algebra t = GAlgebra (GRep t (Reify Name))

133+ type Algebra t = GAlgebra (GRep t (Reify Result))

138134

139135 type GRep t context = Rep (Record (t context))

140136

141− type GColumns t = Eval (GGColumns (Algebra t) TColumns (GRep t (Reify Name)))

137+ type GColumns t = Eval (GGColumns (Algebra t) TColumns (GRep t (Reify Result)))

142138

143139 type GContext t context =

144140 Eval (GGContext (Algebra t) TUnreifyContext (GRep t (Reify context)))

@@ -149,7 +145,7 @@ class

149145 , KnownAlgebra (Algebra t)

150146 , Eval (GGTable (Algebra t) (TTable (Reify context)) TColumns (Col (Reify context)) (GRep t (Reify context)))

151147 , Eval (GGColumns (Algebra t) TColumns (GRep t (Reify context))) ~ GColumns t

152− , Constraints t context

148+ , Eval (GGContext (Algebra t) TUnreifyContext (GRep t (Reify context))) ~ context

153149 )

154150 => GColumns t (Col (Reify context)) -> t (Reify context)

155151 gfromColumns =

@@ -159,9 +155,8 @@ class

159155 @(Algebra t)

160156 @(TTable (Reify context))

161157 @TColumns

162− @TContext

163− (fromContext @t @context)

164− (toContext @t @context)

158+ (\(Reify a) -> a)

159+ Reify

165160 fromColumns

166161

167162 default gtoColumns :: forall context.

@@ -170,7 +165,7 @@ class

170165 , KnownAlgebra (Algebra t)

171166 , Eval (GGTable (Algebra t) (TTable (Reify context)) TColumns (Col (Reify context)) (GRep t (Reify context)))

172167 , Eval (GGColumns (Algebra t) TColumns (GRep t (Reify context))) ~ GColumns t

173− , Constraints t context

168+ , Eval (GGContext (Algebra t) TUnreifyContext (GRep t (Reify context))) ~ context

174169 )

175170 => t (Reify context) -> GColumns t (Col (Reify context))

176171 gtoColumns =

@@ -178,9 +173,8 @@ class

178173 @(Algebra t)

179174 @(TTable (Reify context))

180175 @TColumns

181− @TContext

182− (fromContext @t @context)

183− (toContext @t @context)

176+ (\(Reify a) -> a)

177+ Reify

184178 toColumns .

185179 from .

186180 Record

@@ -189,7 +183,6 @@ class

189183 ( Generic (Record (t (Reify Result)))

190184 , GRep t (Reify Result) ~ Rep (Record (t (Reify Result)))

191185 , G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRep t (Reify Result))

192− , G.GColumnsADT TColumns (GRep t (Reify Result)) ~ GColumnsADT t

193186 )

194187 => GColumnsADT t (Col (Reify Result)) -> t (Reify Result)

195188 gfromColumnsADT =

@@ -206,7 +199,6 @@ class

206199 ( Generic (Record (t (Reify Result)))

207200 , GRep t (Reify Result) ~ Rep (Record (t (Reify Result)))

208201 , G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRep t (Reify Result))

209− , G.GColumnsADT TColumns (GRep t (Reify Result)) ~ GColumnsADT t

210202 )

211203 => t (Reify Result) -> GColumnsADT t (Col (Reify Result))

212204 gtoColumnsADT =

@@ -252,42 +244,8 @@ class

252244 Record

253245

254246

255−type GColumnsADT t = G.GColumnsADT TColumns (GRep t (Reify Name))

247+type GColumnsADT t = G.GColumnsADT TColumns (GRep t (Reify Result))

256248

257249

258250data TUnreifyContext :: Type -> Exp K.Context

259251type instance Eval (TUnreifyContext a) = UnwrapReify (Eval (TContext a))

260−

261−

262−type Constraints :: K.Rel8able -> K.Context -> Constraint

263−type Constraints t context = Constraints' (Algebra t) t context

264−

265−

266−type Constraints' :: K.Algebra -> K.Rel8able -> K.Context -> Constraint

267−type family Constraints' algebra t context where

268− Constraints' 'K.Product t context =

269− Eval (GGContext 'K.Product TContext (GRep t (Reify context))) ~

270− Reify context

271− Constraints' 'K.Sum _ context = context ~ Result

272−

273−

274−fromContext :: forall t context spec.

275− ( KnownAlgebra (Algebra t)

276− , Constraints t context

277− )

278− => Col (Reify context) spec

279− -> Col (Eval (GGContext (Algebra t) TContext (GRep t (Reify context)))) spec

280−fromContext = case algebraSing @(Algebra t) of

281− SProduct -> id

282− SSum -> \(Reify a) -> a

283−

284−

285−toContext :: forall t context spec.

286− ( KnownAlgebra (Algebra t)

287− , Constraints t context

288− )

289− => Col (Eval (GGContext (Algebra t) TContext (GRep t (Reify context)))) spec

290− -> Col (Reify context) spec

291−toContext = case algebraSing @(Algebra t) of

292− SProduct -> id

293− SSum -> Reify

src/Rel8/Generic/Rel8able/Test.hs+10−4

@@ -19,9 +19,6 @@ where

1919import GHC.Generics ( Generic )

2020import Prelude

2121

22−-- higgledy

23−import Data.Generic.HKD ( HKD )

24−

2522-- rel8

2623import Rel8

2724

@@ -96,8 +93,17 @@ deriving via HKDT S3Object

9693 instance x ~ HKD S3Object Expr => ToExprs x S3Object

9794

9895

99−newtype HKDTest f = HKDTest

96+data HKDSum = HKDSumA Text | HKDSumB Bool Char

97+ deriving stock Generic

98+

99+

100+deriving via HKDT HKDSum

101+ instance x ~ HKD HKDSum Expr => ToExprs x HKDSum

102+

103+

104+data HKDTest f = HKDTest

100105 { s3Object :: Lift f S3Object

106+ , hkdSum :: Lift f HKDSum

101107 }

102108 deriving stock Generic

103109 deriving anyclass Rel8able

src/Rel8/Generic/Table.hs+6−6

@@ -115,12 +115,12 @@ type family GAlgebra rep where

115115 GAlgebra (K1 _ _) = 'Product

116116

117117

118−ggfromColumns :: forall algebra _Table _Columns _Context rep context x.

118+ggfromColumns :: forall algebra _Table _Columns rep context x.

119119 ( KnownAlgebra algebra

120120 , Eval (GGTable algebra _Table _Columns context rep)

121121 )

122− => (forall spec. context spec -> Col (Eval (GGContext algebra _Context rep)) spec)

123− -> (forall spec. Col (Eval (GGContext algebra _Context rep)) spec -> context spec)

122+ => (forall spec. algebra ~ 'Sum => context spec -> Col Result spec)

123+ -> (forall spec. algebra ~ 'Sum => Col Result spec -> context spec)

124124 -> (forall a. Eval (_Table a) => Eval (_Columns a) context -> a)

125125 -> Eval (GGColumns algebra _Columns rep) context

126126 -> rep x

@@ -129,12 +129,12 @@ ggfromColumns = case algebraSing @algebra of

129129 SSum -> gfromColumnsADT @_Table @_Columns

130130

131131

132−ggtoColumns :: forall algebra _Table _Columns _Context rep context x.

132+ggtoColumns :: forall algebra _Table _Columns rep context x.

133133 ( KnownAlgebra algebra

134134 , Eval (GGTable algebra _Table _Columns context rep)

135135 )

136− => (forall spec. context spec -> Col (Eval (GGContext algebra _Context rep)) spec)

137− -> (forall spec. Col (Eval (GGContext algebra _Context rep)) spec -> context spec)

136+ => (forall spec. algebra ~ 'Sum => context spec -> Col Result spec)

137+ -> (forall spec. algebra ~ 'Sum => Col Result spec -> context spec)

138138 -> (forall a. Eval (_Table a) => a -> Eval (_Columns a) context)

139139 -> rep x

140140 -> Eval (GGColumns algebra _Columns rep) context

src/Rel8/Table.hs−2

@@ -119,7 +119,6 @@ class (HTable (Columns a), context ~ Context a) => Table context a | a -> contex

119119 @(GAlgebra (Rep (Record a)))

120120 @(TTable context)

121121 @TColumns

122− @TContext

123122 id

124123 id

125124 toColumns .

@@ -141,7 +140,6 @@ class (HTable (Columns a), context ~ Context a) => Table context a | a -> contex

141140 @(GAlgebra (Rep (Record a)))

142141 @(TTable context)

143142 @TColumns

144− @TContext

145143 id

146144 id

147145 fromColumns

src/Rel8/Table/HKD.hs+196−15

@@ -1,29 +1,164 @@

1+{-# language DataKinds #-}

2+{-# language FlexibleContexts #-}

13{-# language FlexibleInstances #-}

24{-# language MultiParamTypeClasses #-}

5+{-# language ScopedTypeVariables #-}

36{-# language StandaloneKindSignatures #-}

47{-# language TypeApplications #-}

58{-# language TypeFamilies #-}

69{-# language UndecidableInstances #-}

10+{-# language UndecidableSuperClasses #-}

711

812module Rel8.Table.HKD

9− ( HKDT(..)

13+ ( HKD( HKD ), HKDT(..)

14+ , fromHKD, toHKD

15+ , GHKD

1016 )

1117where

1218

1319-- base

14−import Data.Functor.Identity ( Identity(..), runIdentity )

15−import Data.Kind ( Type )

16−import GHC.Generics ( Rep )

20+import Data.Kind ( Constraint, Type )

21+import Data.Proxy ( Proxy( Proxy ) )

22+import Data.Type.Equality ( (:~:)( Refl ) )

23+import GHC.Generics ( Generic, Rep, from, to )

1724import Prelude

1825

19−-- higgledy

20−import Data.Generic.HKD ( Construct, HKD(..), construct, deconstruct )

21−

2226-- rel8

27+import Rel8.Column ( Column )

2328import Rel8.Expr ( Expr )

24−import Rel8.Generic.HKD ( GTable )

25−import Rel8.Table ( fromColumns, toColumns )

26−import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )

29+import Rel8.FCF ( Eval, Exp )

30+import Rel8.Kind.Algebra ( KnownAlgebra )

31+import qualified Rel8.Kind.Algebra as K

32+import Rel8.Generic.Map ( GMap, GMappable, gmap, gunmap )

33+import Rel8.Generic.Record ( GRecord, GRecordable, grecord, gunrecord )

34+import Rel8.Generic.Rel8able

35+ ( Rel8able, Algebra

36+ , GRep, GColumns, GContext, gfromColumns, gtoColumns

37+ , GColumnsADT, gfromColumnsADT, gtoColumnsADT

38+ , greify, gunreify

39+ , TUnreifyContext

40+ )

41+import Rel8.Generic.Table

42+ ( GGTable, GGColumns, GGContext, ggfromColumns, ggtoColumns

43+ , GAlgebra

44+ )

45+import qualified Rel8.Generic.Table.ADT as G

46+import Rel8.Schema.Context ( Col )

47+import qualified Rel8.Schema.Kind as K

48+import Rel8.Schema.HTable ( HTable )

49+import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify )

50+import Rel8.Schema.Result ( Result )

51+import Rel8.Table

52+ ( Table, Columns

53+ , fromColumns, toColumns, reify, unreify

54+ , TTable, TColumns, TUnreify

55+ )

56+import Rel8.Table.Serialize ( ToExprs, fromResult, toResult )

57+

58+

59+data TColumn :: K.Context -> Type -> Exp Type

60+type instance Eval (TColumn f a) = Column f a

61+

62+

63+type GColumnsHKD :: Type -> K.HTable

64+type GColumnsHKD a =

65+ Eval (GGColumns (GAlgebra (Rep a)) TColumns (GRecord (GMap (TColumn (Reify Result)) (Rep a))))

66+

67+

68+type HKD :: Type -> K.Rel8able

69+newtype HKD a f = HKD (GColumnsHKD a (Col f))

70+

71+

72+instance GHKD a => Rel8able (HKD a) where

73+ type Algebra (HKD a) = 'K.Product

74+

75+ type GRep (HKD a) f = GRecord (GMap (TColumn f) (Rep a))

76+

77+ type GColumns (HKD a) = GColumnsHKD a

78+ type GContext (HKD a) context = context

79+

80+ gfromColumns = HKD

81+ gtoColumns (HKD a) = a

82+

83+ gfromColumnsADT =

84+ HKD .

85+ ggtoColumns

86+ @(GAlgebra (Rep a))

87+ @(TTable (Reify Result))

88+ @TColumns

89+ (\(Reify a) -> a)

90+ Reify

91+ toColumns .

92+ G.gfromColumnsADT

93+ @(TTable (Reify Result))

94+ @TColumns

95+ @(Col (Reify Result))

96+ @(GRep (HKD a) (Reify Result))

97+ (\(Reify a) -> a)

98+ Reify

99+ fromColumns

100+

101+ gtoColumnsADT =

102+ G.gtoColumnsADT

103+ @(TTable (Reify Result))

104+ @TColumns

105+ @(Col (Reify Result))

106+ @(GRep (HKD a) (Reify Result))

107+ (\(Reify a) -> a)

108+ Reify

109+ toColumns .

110+ ggfromColumns

111+ @(GAlgebra (Rep a))

112+ @(TTable (Reify Result))

113+ @TColumns

114+ (\(Reify a) -> a)

115+ Reify

116+ fromColumns .

117+ (\(HKD a) -> a)

118+

119+ greify (HKD a) = HKD (hreify a)

120+ gunreify (HKD a) = HKD (hunreify a)

121+

122+

123+instance

124+ ( KnownAlgebra (GAlgebra (Rep a))

125+ , HTable (GColumnsHKD a)

126+ , Eval (GGTable (GAlgebra (Rep a)) (TTable (Reify f)) TColumns (Col (Reify f)) (GRecord (GMap (TColumn (Reify f)) (Rep a))))

127+ , Eval (GGColumns (GAlgebra (Rep a)) TColumns (GRecord (GMap (TColumn (Reify f)) (Rep a)))) ~ GColumnsHKD a

128+ , Eval (GGContext (GAlgebra (Rep a)) TUnreifyContext (GRecord (GMap (TColumn (Reify f)) (Rep a)))) ~ f

129+ , GRecordable (GMap (TColumn (Reify f)) (Rep a))

130+ , GMappable (TTable (Reify f)) (GMap (TColumn (Reify f)) (Rep a))

131+ , GMap TUnreify (GMap (TColumn (Reify f)) (Rep a)) ~ GMap (TColumn f) (Rep a)

132+ )

133+ => Generic (HKD a f)

134+ where

135+ type Rep (HKD a f) = GMap (TColumn f) (Rep a)

136+

137+ from =

138+ gmap @(TTable (Reify f)) (Proxy @TUnreify) (unreify Refl) .

139+ gunrecord @(GMap (TColumn (Reify f)) (Rep a)) .

140+ ggfromColumns

141+ @(GAlgebra (Rep a))

142+ @(TTable (Reify f))

143+ @TColumns

144+ (\(Reify a) -> a)

145+ Reify

146+ fromColumns .

147+ hreify .

148+ (\(HKD a) -> a)

149+

150+ to =

151+ HKD .

152+ hunreify .

153+ ggtoColumns

154+ @(GAlgebra (Rep a))

155+ @(TTable (Reify f))

156+ @TColumns

157+ (\(Reify a) -> a)

158+ Reify

159+ toColumns .

160+ grecord @(GMap (TColumn (Reify f)) (Rep a)) .

161+ gunmap @(TTable (Reify f)) (Proxy @TUnreify) (reify Refl)

27162

28163

29164type HKDT :: Type -> Type

@@ -32,11 +167,57 @@ newtype HKDT a = HKDT

32167 }

33168

34169

35−instance (GTable (Rep a), Construct Identity a, x ~ HKD a Expr) =>

36− ToExprs x (HKDT a)

170+instance

171+ ( Table Expr (HKD a Expr)

172+ , Columns (HKD a Expr) ~ GColumns (HKD a)

173+ , GHKD a

174+ , x ~ HKD a Expr

175+ )

176+ => ToExprs x (HKDT a)

37177 where

38− toResult = toColumns . deconstruct @Identity . unHKDT

39− fromResult = HKDT . runIdentity . construct . fromColumns

178+ toResult = (\(HKD a) -> a) . toHKD . (\(HKDT a) -> a)

179+ fromResult = HKDT . fromHKD . HKD

40180

41181

42−type instance FromExprs (HKD a Expr) = a

182+fromHKD :: GHKD a => HKD a Result -> a

183+fromHKD = to . gunmap @Top (Proxy @(TColumn Result)) id . from

184+

185+

186+toHKD :: GHKD a => a -> HKD a Result

187+toHKD = to . gmap @Top (Proxy @(TColumn Result)) id . from

188+

189+

190+data Top :: Type -> Exp Constraint

191+type instance Eval (Top _) = ()

192+

193+

194+class

195+ ( Generic a

196+ , HTable (GColumns (HKD a))

197+ , HTable (GColumnsADT (HKD a))

198+ , KnownAlgebra (GAlgebra (Rep a))

199+ , Eval (GGTable (GAlgebra (Rep a)) (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (GMap (TColumn (Reify Result)) (Rep a))))

200+ , Eval (GGColumns (GAlgebra (Rep a)) TColumns (GRecord (GMap (TColumn (Reify Result)) (Rep a)))) ~ GColumnsHKD a

201+ , Eval (GGContext (GAlgebra (Rep a)) TUnreifyContext (GRecord (GMap (TColumn (Reify Result)) (Rep a)))) ~ Result

202+ , G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (GMap (TColumn (Reify Result)) (Rep a)))

203+ , GRecordable (GMap (TColumn (Reify Result)) (Rep a))

204+ , GMappable Top (Rep a)

205+ , GMappable (TTable (Reify Result)) (GMap (TColumn (Reify Result)) (Rep a))

206+ , GMap TUnreify (GMap (TColumn (Reify Result)) (Rep a)) ~ GMap (TColumn Result) (Rep a)

207+ )

208+ => GHKD a

209+instance

210+ ( Generic a

211+ , HTable (GColumns (HKD a))

212+ , HTable (GColumnsADT (HKD a))

213+ , KnownAlgebra (GAlgebra (Rep a))

214+ , Eval (GGTable (GAlgebra (Rep a)) (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (GMap (TColumn (Reify Result)) (Rep a))))

215+ , Eval (GGColumns (GAlgebra (Rep a)) TColumns (GRecord (GMap (TColumn (Reify Result)) (Rep a)))) ~ GColumnsHKD a

216+ , Eval (GGContext (GAlgebra (Rep a)) TUnreifyContext (GRecord (GMap (TColumn (Reify Result)) (Rep a)))) ~ Result

217+ , G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (GMap (TColumn (Reify Result)) (Rep a)))

218+ , GRecordable (GMap (TColumn (Reify Result)) (Rep a))

219+ , GMappable Top (Rep a)

220+ , GMappable (TTable (Reify Result)) (GMap (TColumn (Reify Result)) (Rep a))

221+ , GMap TUnreify (GMap (TColumn (Reify Result)) (Rep a)) ~ GMap (TColumn Result) (Rep a)

222+ )

223+ => GHKD a

src/Rel8/Table/Rel8able.hs+7−5

@@ -15,7 +15,7 @@ module Rel8.Table.Rel8able

1515where

1616

1717-- base

18−import Data.Kind ( Constraint )

18+import Data.Kind ( Constraint, Type )

1919import Data.Type.Equality ( (:~:)( Refl ) )

2020import Prelude

2121

@@ -47,6 +47,7 @@ import Rel8.Table

4747import Rel8.Schema.Spec.ConstrainDBType ( ConstrainDBType )

4848import Rel8.Table.ADT ( ADT )

4949import Rel8.Table.Eq ( EqTable, eqTable )

50+import Rel8.Table.HKD ( HKD )

5051import Rel8.Table.Ord ( OrdTable, ordTable )

5152import Rel8.Table.Recontextualize ( Recontextualize )

5253import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )

@@ -112,7 +113,7 @@ instance

112113 ordTable = hdicts @(Columns (t context)) @(ConstrainDBType DBOrd)

113114

114115

115−type instance FromExprs (t Expr) = FromExprs' t Result

116+type instance FromExprs (t Expr) = FromExprs' t

116117

117118

118119instance

@@ -126,10 +127,11 @@ instance

126127 toResult = toResult' @(Algebra t) @t'

127128

128129

129−type FromExprs' :: K.Rel8able -> K.Rel8able

130+type FromExprs' :: K.Rel8able -> Type

130131type family FromExprs' t where

131− FromExprs' (ADT t) = t

132− FromExprs' t = t

132+ FromExprs' (ADT t) = t Result

133+ FromExprs' (HKD a) = a

134+ FromExprs' t = t Result

133135

134136

135137type ToExprs' :: K.Algebra -> K.Rel8able -> K.Rel8able -> Constraint