66dc44d · rel8 · git.iko.soy

git.iko.soy/rel8

Teach Table and friends about Sum types

commit66dc44da33b69afe8e821ee323eef7dc78a17ca7 authorShane O'Brien <shane.obrien@circuithub.com> dateFri 30 Apr 2021, 15:04 (6 years ago) parent6c20afa

16 files changed+981−360

compare with master

unifiedsplit

rel8.cabal+6−2 src/Rel8.hs+2−2 src/Rel8/Generic/Reify.hs+24 src/Rel8/Schema/Generic.hs → src/Rel8/Generic/Rel8able.hs+106−24 src/Rel8/Schema/Generic/Test.hs → src/Rel8/Generic/Rel8able/Test.hs+10−2 src/Rel8/Generic/Table.hs+157−95 src/Rel8/Generic/Table/ADT.hs+225−79 src/Rel8/Generic/Table/Record.hs+206 src/Rel8/Kind/Algebra.hs+38 src/Rel8/Schema/Context/Nullify.hs+4−15 src/Rel8/Schema/Context/Result.hs+64 src/Rel8/Schema/Spec/ConstrainDBType.hs+30−5 src/Rel8/Table.hs+38−70 src/Rel8/Table/Eq.hs+18−7 src/Rel8/Table/Ord.hs+18−7 src/Rel8/Table/Serialize.hs+35−52

rel8.cabal+6−2

@@ -63,14 +63,19 @@ library

6363

6464 Rel8.FCF

6565

66+ Rel8.Kind.Algebra

6667 Rel8.Kind.Context

6768 Rel8.Kind.Labels

6869 Rel8.Kind.Necessity

6970

7071 Rel8.Generic.Map

7172 Rel8.Generic.Record

73+ Rel8.Generic.Reify

74+ Rel8.Generic.Rel8able

75+ Rel8.Generic.Rel8able.Test

7276 Rel8.Generic.Table

7377 Rel8.Generic.Table.ADT

78+ Rel8.Generic.Table.Record

7479

7580 Rel8.Order

7681

@@ -96,10 +101,9 @@ library

96101 Rel8.Schema.Context

97102 Rel8.Schema.Context.Label

98103 Rel8.Schema.Context.Nullify

104+ Rel8.Schema.Context.Result

99105 Rel8.Schema.Dict

100106 Rel8.Schema.Field

101− Rel8.Schema.Generic

102− Rel8.Schema.Generic.Test

103107 Rel8.Schema.HKD

104108 Rel8.Schema.HTable

105109 Rel8.Schema.HTable.Either

src/Rel8.hs+2−2

@@ -260,6 +260,7 @@ import Rel8.Expr.Opaleye (unsafeCastExpr)

260260import Rel8.Expr.Ord

261261import Rel8.Expr.Order

262262import Rel8.Expr.Serialize

263+import Rel8.Generic.Rel8able ( KRel8able, Rel8able )

263264import Rel8.Kind.Necessity

264265import Rel8.Order

265266import Rel8.Query

@@ -281,7 +282,6 @@ import Rel8.Query.Values

281282import Rel8.Schema.Column

282283import Rel8.Schema.Context.Label

283284import Rel8.Schema.Field

284−import Rel8.Schema.Generic

285285import Rel8.Schema.HKD

286286import Rel8.Schema.HTable

287287import Rel8.Schema.Name

@@ -294,7 +294,7 @@ import Rel8.Statement.Returning

294294import Rel8.Statement.Select

295295import Rel8.Statement.Update

296296import Rel8.Statement.View

297−import Rel8.Table hiding ( null )

297+import Rel8.Table

298298import Rel8.Table.Aggregate

299299import Rel8.Table.Alternative

300300import Rel8.Table.Bool

src/Rel8/Generic/Reify.hsnew file+24

@@ -0,0 +1,24 @@

1+{-# language StandaloneKindSignatures #-}

2+{-# language TypeFamilies #-}

4+module Rel8.Generic.Reify

5+ ( ARep

6+ )

7+where

9+-- base

10+import Data.Functor.Contravariant ( Contravariant, contramap )

11+import Data.Kind ( Type )

12+import Data.Void ( Void, absurd )

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

14+import Prelude

15+

16+

17+type ARep :: (Type -> Type) -> Type

18+newtype ARep rep = ARep (rep Void)

19+

20+

21+instance (Contravariant rep, Functor rep) => Generic (ARep rep) where

22+ type Rep (ARep rep) = rep

23+ from (ARep a) = fmap absurd a

24+ to = ARep . contramap absurd

src/Rel8/Schema/Generic.hs → src/Rel8/Generic/Rel8able.hsrenamed+106−24

@@ -1,3 +1,5 @@

1+{-# language AllowAmbiguousTypes #-}

2+{-# language ConstraintKinds #-}

13{-# language DataKinds #-}

24{-# language DefaultSignatures #-}

35{-# language FlexibleContexts #-}

@@ -11,9 +13,10 @@

1113

1214{-# options_ghc -fno-warn-orphans #-}

1315

14−module Rel8.Schema.Generic

15− ( Rel8able

16− , KRel8able

16+module Rel8.Generic.Rel8able

17+ ( KRel8able, Rel8able

18+ , GColumns, GContext, gfromColumns, gtoColumns, greify, gunreify

19+ , Algebra

1720 )

1821where

1922

@@ -30,27 +33,45 @@ import Rel8.Kind.Context

3033 , Reifiable, contextSing

3134 , sLabelable, sReifiable

3235 )

36+import Rel8.FCF ( Eval, Exp )

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

3438import Rel8.Generic.Record ( Record(..) )

35−import Rel8.Generic.Table ( GTable, GColumns, fromGColumns, toGColumns )

39+import Rel8.Generic.Table

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

41+ , GAlgebra

42+ )

43+import Rel8.Kind.Algebra

44+ ( SAlgebra( SProduct, SSum )

45+ , KnownAlgebra, algebraSing

46+ )

47+import qualified Rel8.Kind.Algebra as K ( Algebra(..) )

3648import Rel8.Schema.Context ( Col )

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

3850import Rel8.Schema.Dict ( Dict( Dict ) )

3951import Rel8.Schema.HTable ( HTable )

4052import qualified Rel8.Schema.Kind as K

4153import Rel8.Schema.Name ( Name )

42−import Rel8.Schema.Reify ( Reify, UnwrapReify, hreify, hunreify )

54+import Rel8.Schema.Reify

55+ ( Col( Reify ), Reify, hreify, hunreify

56+ , UnwrapReify

57+ )

58+import Rel8.Schema.Result ( Result )

4359import Rel8.Table

4460 ( Table, Columns, Context, fromColumns, toColumns

4561 , Unreify, reify, unreify

46− , TTable, TColumns, TUnreify

62+ , TTable, TColumns, TContext, TUnreify

4763 )

4864

4965

50−instance (Rel8able t, Labelable context, Reifiable context) =>

51− Table context (t context)

66+instance

67+ ( Rel8able t

68+ , GContext t context ~ context

69+ , Labelable context

70+ , Reifiable context

71+ )

72+ => Table context (t context)

5273 where

53− type Columns (t context) = GRep t

74+ type Columns (t context) = GColumns t

5475 type Context (t context) = context

5576 type Unreify (t context) = t (UnwrapReify context)

5677

@@ -115,14 +136,16 @@ type KRel8able = K.Rel8able

115136-- deriving ( GHC.Generics.Generic, Rel8able )

116137-- @

117138type Rel8able :: K.Rel8able -> Constraint

118−class HTable (GRep t) => Rel8able t where

119− type GRep t :: K.HTable

139+class HTable (GColumns t) => Rel8able t where

140+ type Algebra t :: K.Algebra

141+ type GColumns t :: K.HTable

142+ type GContext t (context :: K.Context) :: K.Context

120143

121− gfromColumns :: (Labelable context, Reifiable context)

122− => GRep t (Col (Reify context)) -> t (Reify context)

144+ gfromColumns :: (Labelable context, Reifiable context, GContext t context ~ context)

145+ => GColumns t (Col (Reify context)) -> t (Reify context)

123146

124− gtoColumns :: (Labelable context, Reifiable context)

125− => t (Reify context) -> GRep t (Col (Reify context))

147+ gtoColumns :: (Labelable context, Reifiable context, GContext t context ~ context)

148+ => t (Reify context) -> GColumns t (Col (Reify context))

126149

127150 greify :: (Labelable context, Reifiable context)

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

@@ -130,27 +153,47 @@ class HTable (GRep t) => Rel8able t where

130153 gunreify :: (Labelable context, Reifiable context)

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

132155

133− type GRep t = GColumns TColumns (Rep (Record (t (Reify Name))))

156+ type Algebra t = GAlgebra (Rep (Record (t (Reify Name))))

157+ type GColumns t = Eval (GGColumns (Algebra t) TColumns (Rep (Record (t (Reify Name)))))

158+ type GContext t context = Eval (GGContext (Algebra t) TUnreifyContext (Rep (Record (t (Reify context)))))

134159

135160 default gfromColumns :: forall context.

136161 ( Generic (Record (t (Reify context)))

137− , GColumns TColumns (Rep (Record (t (Reify context)))) ~ GRep t

138− , GTable (TTable (Reify context)) TColumns (Col (Reify context)) (Rep (Record (t (Reify context))))

162+ , KnownAlgebra (Algebra t)

163+ , Eval (GGTable (Algebra t) (TTable (Reify context)) TColumns (Col (Reify context)) (Rep (Record (t (Reify context)))))

164+ , Eval (GGColumns (Algebra t) TColumns (Rep (Record (t (Reify context))))) ~ GColumns t

165+ , Constraints t context

139166 )

140− => GRep t (Col (Reify context)) -> t (Reify context)

167+ => GColumns t (Col (Reify context)) -> t (Reify context)

141168 gfromColumns =

142169 unrecord .

143170 to .

144− fromGColumns @(TTable (Reify context)) @TColumns fromColumns

171+ ggfromColumns

172+ @(Algebra t)

173+ @(TTable (Reify context))

174+ @TColumns

175+ @TContext

176+ (fromContext @t @context)

177+ (toContext @t @context)

178+ fromColumns

145179

146180 default gtoColumns :: forall context.

147181 ( Generic (Record (t (Reify context)))

148− , GColumns TColumns (Rep (Record (t (Reify context)))) ~ GRep t

149− , GTable (TTable (Reify context)) TColumns (Col (Reify context)) (Rep (Record (t (Reify context))))

182+ , KnownAlgebra (Algebra t)

183+ , Eval (GGTable (Algebra t) (TTable (Reify context)) TColumns (Col (Reify context)) (Rep (Record (t (Reify context)))))

184+ , Eval (GGColumns (Algebra t) TColumns (Rep (Record (t (Reify context))))) ~ GColumns t

185+ , Constraints t context

150186 )

151− => t (Reify context) -> GRep t (Col (Reify context))

187+ => t (Reify context) -> GColumns t (Col (Reify context))

152188 gtoColumns =

153− toGColumns @(TTable (Reify context)) @TColumns toColumns .

189+ ggtoColumns

190+ @(Algebra t)

191+ @(TTable (Reify context))

192+ @TColumns

193+ @TContext

194+ (fromContext @t @context)

195+ (toContext @t @context)

196+ toColumns .

154197 from .

155198 Record

156199

@@ -181,3 +224,42 @@ class HTable (GRep t) => Rel8able t where

181224 gmap @(TTable (Reify context)) (Proxy @TUnreify) (unreify Refl) .

182225 from .

183226 Record

227+

228+

229+data TUnreifyContext :: Type -> Exp K.Context

230+type instance Eval (TUnreifyContext a) = UnwrapReify (Eval (TContext a))

231+

232+

233+type Constraints :: K.Rel8able -> K.Context -> Constraint

234+type Constraints t context = Constraints' (Algebra t) t context

235+

236+

237+type Constraints' :: K.Algebra -> K.Rel8able -> K.Context -> Constraint

238+type family Constraints' algebra t context where

239+ Constraints' 'K.Product t context =

240+ ( Eval (GGContext 'K.Product TContext (Rep (Record (t (Reify context))))) ~

241+ Reify context

242+ )

243+ Constraints' 'K.Sum _ context = context ~ Result

244+

245+

246+fromContext :: forall t context spec.

247+ ( KnownAlgebra (Algebra t)

248+ , Constraints t context

249+ )

250+ => Col (Reify context) spec

251+ -> Col (Eval (GGContext (Algebra t) TContext (Rep (Record (t (Reify context)))))) spec

252+fromContext = case algebraSing @(Algebra t) of

253+ SProduct -> id

254+ SSum -> \(Reify a) -> a

255+

256+

257+toContext :: forall t context spec.

258+ ( KnownAlgebra (Algebra t)

259+ , Constraints t context

260+ )

261+ => Col (Eval (GGContext (Algebra t) TContext (Rep (Record (t (Reify context)))))) spec

262+ -> Col (Reify context) spec

263+toContext = case algebraSing @(Algebra t) of

264+ SProduct -> id

265+ SSum -> Reify

src/Rel8/Schema/Generic/Test.hs → src/Rel8/Generic/Rel8able/Test.hsrenamed+10−2

@@ -10,8 +10,8 @@

1010

1111{-# options_ghc -O0 #-}

1212

13−module Rel8.Schema.Generic.Test

14− ( module Rel8.Schema.Generic.Test

13+module Rel8.Generic.Rel8able.Test

14+ ( module Rel8.Generic.Rel8able.Test

1515 )

1616where

1717

@@ -116,3 +116,11 @@ data NonRecord f = NonRecord

116116 (Column f Char)

117117 deriving stock Generic

118118 deriving anyclass Rel8able

119+

120+

121+data TableSum f

122+ = TableSumA (Column f Bool) (Column f Text)

123+ | TableSumB

124+ | TableSumC (Column f Text)

125+ deriving stock Generic

126+ deriving anyclass Rel8able

src/Rel8/Generic/Table.hs+157−95

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

11{-# language AllowAmbiguousTypes #-}

22{-# language DataKinds #-}

3+{-# language FlexibleContexts #-}

34{-# language FlexibleInstances #-}

45{-# language MultiParamTypeClasses #-}

5−{-# language PolyKinds #-}

66{-# language RankNTypes #-}

77{-# language ScopedTypeVariables #-}

88{-# language StandaloneKindSignatures #-}

@@ -12,115 +12,177 @@

1212{-# language UndecidableInstances #-}

1313

1414module Rel8.Generic.Table

15− ( GTable, GColumns, GContext, fromGColumns, toGColumns, gtable

15+ ( GGTable, GGColumns, GGContext, ggfromColumns, ggtoColumns, ggtable

16+ , GGToExprs, ggfromResult, ggtoResult

17+ , GAlgebra

1618 )

1719where

1820

1921-- base

2022import Data.Kind ( Constraint, Type )

21−import Data.Proxy ( Proxy( Proxy ) )

22−import GHC.Generics

23− ( (:*:)( (:*:) ), K1( K1 ), M1( M1 )

24− , C, D, S

25− , Meta( MetaSel )

26− )

27−import GHC.TypeLits ( KnownSymbol )

28−import Prelude hiding ( null )

23+import GHC.Generics ( (:+:), (:*:), K1, M1, U1, V1 )

24+import Prelude ()

2925

3026-- rel8

3127import Rel8.FCF ( Eval, Exp )

32−import Rel8.Schema.Context.Label ( HLabelable, hlabeler, hunlabeler )

33−import Rel8.Schema.HTable ( HTable )

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

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

28+import Rel8.Generic.Table.ADT

29+ ( GTableADT, GColumnsADT, gfromColumnsADT, gtoColumnsADT, gtableADT

30+ , GToExprsADT, gtoResultADT, gfromResultADT

31+ )

32+import Rel8.Generic.Table.Record

33+ ( GTable, GColumns, GContext, gfromColumns, gtoColumns, gtable

34+ , GToExprs, gtoResult, gfromResult

35+ )

36+import Rel8.Kind.Algebra

37+ ( Algebra( Product, Sum )

38+ , SAlgebra( SProduct, SSum )

39+ , KnownAlgebra, algebraSing

40+ )

41+import Rel8.Schema.Context ( Col )

3642import qualified Rel8.Schema.Kind as K

43+import Rel8.Schema.Null ( Nullify )

44+import Rel8.Schema.Spec ( Spec( Spec ), SSpec )

45+import Rel8.Schema.Result ( Result )

46+

47+

48+data GGTable

49+ :: Algebra

50+ -> (Type -> Exp Constraint)

51+ -> (Type -> Exp K.HTable)

52+ -> K.HContext

53+ -> (Type -> Type)

54+ -> Exp Constraint

55+

3756

57+type instance Eval (GGTable 'Product _Table _Columns context rep) =

58+ GTable _Table _Columns context rep

3859

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

40−type family GColumns _Columns rep where

41− GColumns _Columns (M1 D _ rep) = GColumns _Columns rep

42− GColumns _Columns (M1 C _ rep) = GColumns _Columns rep

43− GColumns _Columns (rep1 :*: rep2) =

44− HProduct (GColumns _Columns rep1) (GColumns _Columns rep2)

45− GColumns _Columns (M1 S ('MetaSel ('Just label) _ _ _) (K1 _ a)) =

46− HLabel label (Eval (_Columns a))

4760

61+type instance Eval (GGTable 'Sum _Table _Columns context rep) =

62+ GTableADT _Table _Columns context rep

4863

49−type GContext :: (Type -> Exp a) -> (Type -> Type) -> a

50−type family GContext _Context rep where

51− GContext _Context (M1 _ _ rep) = GContext _Context rep

52− GContext _Context (rep1 :*: _rep2) = GContext _Context rep1

53− GContext _Context (K1 _ a) = Eval (_Context a)

64+

65+data GGToExprs

66+ :: Algebra

67+ -> (Type -> Type -> Exp Constraint)

68+ -> (Type -> Exp K.HTable)

69+ -> (Type -> Type)

70+ -> (Type -> Type)

71+ -> Exp Constraint

72+

73+

74+type instance Eval (GGToExprs 'Product _ToExprs _Columns exprs rep) =

75+ GToExprs _ToExprs _Columns exprs rep

5476

5577

56−type GTable

57− :: (Type -> Exp Constraint)

78+type instance Eval (GGToExprs 'Sum _ToExprs _Columns exprs rep) =

79+ GToExprsADT _ToExprs _Columns exprs rep

80+

81+

82+data GGColumns

83+ :: Algebra

5884 -> (Type -> Exp K.HTable)

59− -> K.HContext -> (Type -> Type) -> Constraint

60−class GTable _Table _Columns context rep

61− where

62− fromGColumns :: ()

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

64− -> GColumns _Columns rep context

65− -> rep x

66−

67− toGColumns :: ()

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

69− -> rep x

70− -> GColumns _Columns rep context

71−

72− gtable :: ()

73− => (forall a. Eval (_Table a) => Proxy a -> Eval (_Columns a) context)

74− -> GColumns _Columns rep context

75−

76−

77−instance GTable _Table _Columns context rep =>

78− GTable _Table _Columns context (M1 D c rep)

79− where

80− fromGColumns fromColumns =

81− M1 . fromGColumns @_Table @_Columns @context @rep fromColumns

82− toGColumns toColumns (M1 a) =

83− toGColumns @_Table @_Columns @context @rep toColumns a

84− gtable = gtable @_Table @_Columns @context @rep

85−

86−

87−instance GTable _Table _Columns context rep =>

88− GTable _Table _Columns context (M1 C c rep)

89− where

90− fromGColumns fromColumns =

91− M1 . fromGColumns @_Table @_Columns @context @rep fromColumns

92− toGColumns toColumns (M1 a) =

93− toGColumns @_Table @_Columns @context @rep toColumns a

94− gtable = gtable @_Table @_Columns @context @rep

95−

96−

97−instance

98− ( GTable _Table _Columns context rep1

99− , GTable _Table _Columns context rep2

85+ -> (Type -> Type)

86+ -> Exp K.HTable

87+

88+

89+type instance Eval (GGColumns 'Product _Columns rep) = GColumns _Columns rep

90+

91+

92+type instance Eval (GGColumns 'Sum _Columns rep) = GColumnsADT _Columns rep

93+

94+

95+data GGContext

96+ :: Algebra

97+ -> (Type -> Exp K.Context)

98+ -> (Type -> Type)

99+ -> Exp K.Context

100+

101+

102+type instance Eval (GGContext 'Product _Context rep) = GContext _Context rep

103+

104+

105+type instance Eval (GGContext 'Sum _Context _rep) = Result

106+

107+

108+type GAlgebra :: (Type -> Type) -> Algebra

109+type family GAlgebra rep where

110+ GAlgebra (M1 _ _ rep) = GAlgebra rep

111+ GAlgebra V1 = 'Sum

112+ GAlgebra (_ :+: _) = 'Sum

113+ GAlgebra U1 = 'Sum

114+ GAlgebra (_ :*: _) = 'Product

115+ GAlgebra (K1 _ _) = 'Product

116+

117+

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

119+ ( KnownAlgebra algebra

120+ , Eval (GGTable algebra _Table _Columns context rep)

121+ )

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

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

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

125+ -> Eval (GGColumns algebra _Columns rep) context

126+ -> rep x

127+ggfromColumns = case algebraSing @algebra of

128+ SProduct -> \_ _ -> gfromColumns @_Table @_Columns

129+ SSum -> gfromColumnsADT @_Table @_Columns

130+

131+

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

133+ ( KnownAlgebra algebra

134+ , Eval (GGTable algebra _Table _Columns context rep)

135+ )

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

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

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

139+ -> rep x

140+ -> Eval (GGColumns algebra _Columns rep) context

141+ggtoColumns = case algebraSing @algebra of

142+ SProduct -> \_ _ -> gtoColumns @_Table @_Columns

143+ SSum -> gtoColumnsADT @_Table @_Columns

144+

145+

146+ggtable :: forall algebra _Table _Columns rep context.

147+ ( KnownAlgebra algebra

148+ , Eval (GGTable algebra _Table _Columns context rep)

149+ )

150+ => (forall a proxy. Eval (_Table a) => proxy a -> Eval (_Columns a) context)

151+ -> (forall a labels necessity. ()

152+ => SSpec ('Spec labels necessity a)

153+ -> context ('Spec labels necessity a)

154+ -> context ('Spec labels necessity (Nullify a)))

155+ -> Eval (GGColumns algebra _Columns rep) context

156+ggtable = case algebraSing @algebra of

157+ SProduct -> \table _ -> gtable @_Table @_Columns @_ @rep table

158+ SSum -> gtableADT @_Table @_Columns @_ @rep

159+

160+

161+ggfromResult :: forall algebra _ToExprs _Columns exprs rep x.

162+ ( KnownAlgebra algebra

163+ , Eval (GGToExprs algebra _ToExprs _Columns exprs rep)

100164 )

101− => GTable _Table _Columns context (rep1 :*: rep2)

102− where

103− fromGColumns fromColumns (HProduct a b) =

104− fromGColumns @_Table @_Columns @context @rep1 fromColumns a :*:

105− fromGColumns @_Table @_Columns @context @rep2 fromColumns b

106− toGColumns toColumns (a :*: b) = HProduct

107− (toGColumns @_Table @_Columns @context @rep1 toColumns a)

108− (toGColumns @_Table @_Columns @context @rep2 toColumns b)

109− gtable table = HProduct

110− (gtable @_Table @_Columns @context @rep1 table)

111− (gtable @_Table @_Columns @context @rep2 table)

112−

113−

114−instance

115− ( HTable (Eval (_Columns a))

116− , Eval (_Table a)

117− , HLabelable context

118− , KnownSymbol label

119− , meta ~ 'MetaSel ('Just label) _su _ss _ds

120− , k1 ~ K1 i a

165+ => (forall expr a proxy. Eval (_ToExprs expr a)

166+ => proxy expr

167+ -> Eval (_Columns expr) (Col Result)

168+ -> a)

169+ -> Eval (GGColumns algebra _Columns exprs) (Col Result)

170+ -> rep x

171+ggfromResult = case algebraSing @algebra of

172+ SProduct -> gfromResult @_ToExprs @_Columns @exprs

173+ SSum -> gfromResultADT @_ToExprs @_Columns @exprs

174+

175+

176+ggtoResult :: forall algebra _ToExprs _Columns exprs rep x.

177+ ( KnownAlgebra algebra

178+ , Eval (GGToExprs algebra _ToExprs _Columns exprs rep)

121179 )

122− => GTable _Table _Columns context (M1 S meta k1)

123− where

124− fromGColumns fromColumns = M1 . K1 . fromColumns . hunlabel hunlabeler

125− toGColumns toColumns (M1 (K1 a)) = hlabel hlabeler (toColumns a)

126− gtable table = hlabel hlabeler (table (Proxy @a))

180+ => (forall expr a proxy. Eval (_ToExprs expr a)

181+ => proxy expr

182+ -> a

183+ -> Eval (_Columns expr) (Col Result))

184+ -> rep x

185+ -> Eval (GGColumns algebra _Columns exprs) (Col Result)

186+ggtoResult = case algebraSing @algebra of

187+ SProduct -> gtoResult @_ToExprs @_Columns @exprs

188+ SSum -> gtoResultADT @_ToExprs @_Columns @exprs

src/Rel8/Generic/Table/ADT.hs+225−79

@@ -1,8 +1,10 @@

11{-# language AllowAmbiguousTypes #-}

22{-# language DataKinds #-}

3+{-# language FlexibleContexts #-}

34{-# language FlexibleInstances #-}

45{-# language LambdaCase #-}

56{-# language MultiParamTypeClasses #-}

7+{-# language PolyKinds #-}

68{-# language RankNTypes #-}

79{-# language ScopedTypeVariables #-}

810{-# language StandaloneKindSignatures #-}

@@ -12,8 +14,8 @@

1214{-# language UndecidableInstances #-}

1315

1416module Rel8.Generic.Table.ADT

15− ( GADTTable (fromGADTColumns, toGADTColumns)

16− , GADTColumns

17+ ( GTableADT, GColumnsADT, gfromColumnsADT, gtoColumnsADT, gtableADT

18+ , GToExprsADT, gfromResultADT, gtoResultADT

1719 )

1820where

1921

@@ -30,156 +32,295 @@ import Prelude hiding ( null )

3032

3133-- rel8

3234import Rel8.FCF ( Eval, Exp )

33−import Rel8.Generic.Table ( GTable, GColumns, fromGColumns, toGColumns )

35+import Rel8.Generic.Table.Record

36+ ( GTable, GColumns, gtable

37+ , GToExprs, gfromResult, gtoResult

38+ )

3439import Rel8.Schema.Context ( Col( Result ) )

35−import Rel8.Schema.Context.Label ( labeler, unlabeler )

36−import Rel8.Schema.HTable ( HTable )

40+import Rel8.Schema.Context.Label ( HLabelable, hlabeler, labeler, unlabeler )

41+import Rel8.Schema.Context.Result ( null, nullifier, unnullifier )

42+import Rel8.Schema.HTable ( HTable, hmap )

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

3844import Rel8.Schema.HTable.Nullify ( HNullify, hnulls, hnullify, hunnullify )

3945import Rel8.Schema.HTable.Product ( HProduct( HProduct ) )

4046import Rel8.Schema.HTable.Type ( HType( HType ) )

4147import qualified Rel8.Schema.Kind as K

48+import Rel8.Schema.Null ( Nullify )

49+import Rel8.Schema.Spec ( Spec( Spec ), SSpec )

4250import Rel8.Schema.Result ( Result )

43−import Rel8.Table ( null, nullifier, unnullifier )

4451import Rel8.Type.Tag ( Tag( Tag ) )

4552

4653-- text

4754import Data.Text ( pack )

4855

4956

50−type GADTColumns

57+type GColumnsADT

5158 :: (Type -> Exp K.HTable)

5259 -> (Type -> Type) -> K.HTable

53−type family GADTColumns _Columns rep where

54− GADTColumns _Columns (M1 D _ rep) =

55− GADTColumns' _Columns (HLabel "tag" (HType Tag)) rep

60+type family GColumnsADT _Columns rep where

61+ GColumnsADT _Columns (M1 D _ rep) =

62+ GColumnsADT' _Columns (HLabel "tag" (HType Tag)) rep

5663

5764

58−type GADTColumns'

65+type GColumnsADT'

5966 :: (Type -> Exp K.HTable)

6067 -> K.HTable -> (Type -> Type) -> K.HTable

61−type family GADTColumns' _Columns htable rep where

62− GADTColumns' _Columns htable (a :+: b) =

63− GADTColumns' _Columns (GADTColumns' _Columns htable a) b

64− GADTColumns' _Columns htable (M1 C ('MetaCons _ _ _) U1) = htable

65− GADTColumns' _Columns htable (M1 C ('MetaCons label _ _) rep) =

68+type family GColumnsADT' _Columns htable rep where

69+ GColumnsADT' _Columns htable (a :+: b) =

70+ GColumnsADT' _Columns (GColumnsADT' _Columns htable a) b

71+ GColumnsADT' _Columns htable (M1 C ('MetaCons _ _ _) U1) = htable

72+ GColumnsADT' _Columns htable (M1 C ('MetaCons label _ _) rep) =

6673 HProduct htable (HLabel label (HNullify (GColumns _Columns rep)))

6774

6875

69−type GADTTable

76+type GTableADT

7077 :: (Type -> Exp Constraint)

7178 -> (Type -> Exp K.HTable)

72− -> (Type -> Type) -> Constraint

73−class GADTTable _Table _Columns rep where

74− fromGADTColumns :: ()

75− => (forall a. Eval (_Table a) => Eval (_Columns a) (Col Result) -> a)

76− -> GADTColumns _Columns rep (Col Result)

79+ -> K.HContext -> (Type -> Type) -> Constraint

80+class GTableADT _Table _Columns context rep where

81+ gfromColumnsADT :: ()

82+ => (forall spec. context spec -> Col Result spec)

83+ -> (forall spec. Col Result spec -> context spec)

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

85+ -> GColumnsADT _Columns rep context

7786 -> rep x

7887

79− toGADTColumns :: ()

80− => (forall a. Eval (_Table a) => a -> Eval (_Columns a) (Col Result))

88+ gtoColumnsADT :: ()

89+ => (forall spec. context spec -> Col Result spec)

90+ -> (forall spec. Col Result spec -> context spec)

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

8192 -> rep x

82− -> GADTColumns _Columns rep (Col Result)

93+ -> GColumnsADT _Columns rep context

94+

95+ gtableADT :: ()

96+ => (forall a proxy. Eval (_Table a) => proxy a -> Eval (_Columns a) context)

97+ -> (forall a labels necessity. ()

98+ => SSpec ('Spec labels necessity a)

99+ -> context ('Spec labels necessity a)

100+ -> context ('Spec labels necessity (Nullify a)))

101+ -> GColumnsADT _Columns rep context

83102

84103

85104instance

86105 ( htable ~ HLabel "tag" (HType Tag)

87− , GADTTable' _Table _Columns htable rep

106+ , HTable (GColumnsADT _Columns (M1 D meta rep))

107+ , Eval (_Table (htable context))

108+ , Eval (_Columns (htable context)) ~ htable

109+ , GTableADT' _Table _Columns htable context rep

110+ , GToExprsADT' (Const _Table) _Columns htable rep rep

88111 )

89− => GADTTable _Table _Columns (M1 D meta rep)

112+ => GTableADT _Table _Columns context (M1 D meta rep)

90113 where

91− fromGADTColumns fromColumns columns =

92− case fromGADTColumns' @_Table @_Columns fromColumns tag columns of

114+ gfromColumnsADT fromContext toContext fromColumns =

115+ gfromResultADT @(Const _Table) @_Columns @(M1 D meta rep) @(M1 D meta rep)

116+ (const (fromColumns . hmap toContext)) .

117+ hmap fromContext

118+

119+ gtoColumnsADT fromContext toContext toColumns =

120+ hmap toContext .

121+ gtoResultADT @(Const _Table) @_Columns @(M1 D meta rep) @(M1 D meta rep)

122+ (const (hmap fromContext . toColumns))

123+

124+ gtableADT table hnullifier =

125+ gtableADT' @_Table @_Columns @htable @context @rep table hnullifier htable

126+ where

127+ htable = table (Proxy @(htable context))

128+

129+

130+type GTableADT'

131+ :: (Type -> Exp Constraint)

132+ -> (Type -> Exp K.HTable)

133+ -> K.HTable -> K.HContext -> (Type -> Type) -> Constraint

134+class GTableADT' _Table _Columns htable context rep where

135+ gtableADT' :: ()

136+ => (forall a proxy. Eval (_Table a) => proxy a -> Eval (_Columns a) context)

137+ -> (forall a labels necessity. ()

138+ => SSpec ('Spec labels necessity a)

139+ -> context ('Spec labels necessity a)

140+ -> context ('Spec labels necessity (Nullify a)))

141+ -> htable context

142+ -> GColumnsADT' _Columns htable rep context

143+

144+

145+instance

146+ ( htable' ~ GColumnsADT' _Columns htable a

147+ , GTableADT' _Table _Columns htable context a

148+ , GTableADT' _Table _Columns htable' context b

149+ )

150+ => GTableADT' _Table _Columns htable context (a :+: b)

151+ where

152+ gtableADT' table hnullifier =

153+ gtableADT' @_Table @_Columns @_ @_ @b table hnullifier .

154+ gtableADT' @_Table @_Columns @_ @_ @a table hnullifier

155+

156+

157+instance meta ~ 'MetaCons label _fixity _isRecord =>

158+ GTableADT' _Table _Columns htable context (M1 C meta U1)

159+ where

160+ gtableADT' _ _ = id

161+

162+

163+instance {-# OVERLAPPABLE #-}

164+ ( HTable (GColumns _Columns rep)

165+ , GTable _Table _Columns context rep

166+ , HLabelable context

167+ , meta ~ 'MetaCons label _fixity _isRecord

168+ , KnownSymbol label

169+ , GColumnsADT' _Columns htable (M1 C ('MetaCons label _fixity _isRecord) rep) ~

170+ HProduct htable (HLabel label (HNullify (GColumns _Columns rep)))

171+ )

172+ => GTableADT' _Table _Columns htable context (M1 C meta rep)

173+ where

174+ gtableADT' table hnullifier htable =

175+ HProduct htable $

176+ hlabel hlabeler $

177+ hnullify hnullifier $

178+ gtable @_Table @_Columns @_ @rep table

179+

180+

181+type GToExprsADT

182+ :: (Type -> Type -> Exp Constraint)

183+ -> (Type -> Exp K.HTable)

184+ -> (Type -> Type) -> (Type -> Type) -> Constraint

185+class GToExprsADT _ToExprs _Columns exprs rep where

186+ gfromResultADT :: ()

187+ => (forall expr a proxy.

188+ ( Eval (_ToExprs expr a)

189+ , HTable (Eval (_Columns expr))

190+ )

191+ => proxy expr

192+ -> Eval (_Columns expr) (Col Result)

193+ -> a)

194+ -> GColumnsADT _Columns exprs (Col Result)

195+ -> rep x

196+

197+ gtoResultADT :: ()

198+ => (forall expr a proxy.

199+ ( Eval (_ToExprs expr a)

200+ , HTable (Eval (_Columns expr))

201+ )

202+ => proxy expr

203+ -> a

204+ -> Eval (_Columns expr) (Col Result))

205+ -> rep x

206+ -> GColumnsADT _Columns exprs (Col Result)

207+

208+

209+instance

210+ ( htable ~ HLabel "tag" (HType Tag)

211+ , GToExprsADT' _ToExprs _Columns htable exprs rep

212+ )

213+ => GToExprsADT _ToExprs _Columns (M1 D meta exprs) (M1 D meta rep)

214+ where

215+ gfromResultADT fromResult columns =

216+ case gfromResultADT' @_ToExprs @_Columns @_ @exprs fromResult tag columns of

93217 Just rep -> M1 rep

94218 _ -> error "ADT.fromColumns: mismatch between tag and data"

95219 where

96220 tag = (\(HType (Result a)) -> a) . hunlabel @_ @"tag" unlabeler

97221

98− toGADTColumns toColumns (M1 rep) =

99− toGADTColumns' @_Table @_Columns toColumns tag (Just rep)

222+ gtoResultADT toResult (M1 rep) =

223+ gtoResultADT' @_ToExprs @_Columns @_ @exprs toResult tag (Just rep)

100224 where

101225 tag = hlabel @_ @"tag" labeler . HType . Result

102226

103227

104−type GADTTable'

105− :: (Type -> Exp Constraint)

228+type GToExprsADT'

229+ :: (Type -> Type -> Exp Constraint)

106230 -> (Type -> Exp K.HTable)

107− -> K.HTable -> (Type -> Type) -> Constraint

108−class GADTTable' _Table _Columns htable rep where

109− fromGADTColumns' :: ()

110− => (forall a. Eval (_Table a) => Eval (_Columns a) (Col Result) -> a)

231+ -> K.HTable -> (Type -> Type) -> (Type -> Type) -> Constraint

232+class GToExprsADT' _ToExprs _Columns htable exprs rep where

233+ gfromResultADT' :: ()

234+ => (forall expr a proxy.

235+ ( Eval (_ToExprs expr a)

236+ , HTable (Eval (_Columns expr))

237+ )

238+ => proxy expr

239+ -> Eval (_Columns expr) (Col Result)

240+ -> a)

111241 -> (htable (Col Result) -> Tag)

112− -> GADTColumns' _Columns htable rep (Col Result)

242+ -> GColumnsADT' _Columns htable exprs (Col Result)

113243 -> Maybe (rep x)

114244

115− toGADTColumns' :: ()

116− => (forall a. Eval (_Table a) => a -> Eval (_Columns a) (Col Result))

245+ gtoResultADT' :: ()

246+ => (forall expr a proxy.

247+ ( Eval (_ToExprs expr a)

248+ , HTable (Eval (_Columns expr))

249+ )

250+ => proxy expr

251+ -> a

252+ -> Eval (_Columns expr) (Col Result))

117253 -> (Tag -> htable (Col Result))

118254 -> Maybe (rep x)

119− -> GADTColumns' _Columns htable rep (Col Result)

255+ -> GColumnsADT' _Columns htable exprs (Col Result)

120256

121− extract :: GADTColumns' _Columns htable rep context -> htable context

257+ extract :: GColumnsADT' _Columns htable exprs context -> htable context

122258

123259

124260instance

125− ( htable' ~ GADTColumns' _Columns htable a

126− , GADTTable' _Table _Columns htable a

127− , GADTTable' _Table _Columns htable' b

261+ ( htable' ~ GColumnsADT' _Columns htable a

262+ , GToExprsADT' _ToExprs _Columns htable a rep1

263+ , GToExprsADT' _ToExprs _Columns htable' b rep2

128264 )

129− => GADTTable' _Table _Columns htable (a :+: b)

265+ => GToExprsADT' _ToExprs _Columns htable (a :+: b) (rep1 :+: rep2)

130266 where

131− fromGADTColumns' fromColumns f columns =

267+ gfromResultADT' fromResult f columns =

132268 case ma of

133269 Just a -> Just (L1 a)

134270 Nothing -> R1 <$>

135− fromGADTColumns' @_Table @_Columns @_ @b

136− fromColumns

137− (f . extract @_Table @_Columns @_ @a)

271+ gfromResultADT' @_ToExprs @_Columns @_ @b @rep2

272+ fromResult

273+ (f . extract @_ToExprs @_Columns @_ @a @rep1)

138274 columns

139275 where

140276 ma =

141− fromGADTColumns' @_Table @_Columns @_ @a

142− fromColumns

277+ gfromResultADT' @_ToExprs @_Columns @_ @a @rep1

278+ fromResult

143279 f

144− (extract @_Table @_Columns @_ @b columns)

280+ (extract @_ToExprs @_Columns @_ @b @rep2 columns)

145281

146− toGADTColumns' toColumns tag = \case

282+ gtoResultADT' toResult tag = \case

147283 Just (L1 a) ->

148− toGADTColumns' @_Table @_Columns @_ @b

149− toColumns

150− (\_ -> toGADTColumns' @_Table @_Columns @_ @a

151− toColumns

284+ gtoResultADT' @_ToExprs @_Columns @_ @b @rep2

285+ toResult

286+ (\_ -> gtoResultADT' @_ToExprs @_Columns @_ @a @rep1

287+ toResult

152288 tag

153289 (Just a))

154290 Nothing

155291 Just (R1 b) ->

156− toGADTColumns' @_Table @_Columns @_ @b

157− toColumns

292+ gtoResultADT' @_ToExprs @_Columns @_ @b @rep2

293+ toResult

158294 (\tag' ->

159− toGADTColumns' @_Table @_Columns @_ @a

160− toColumns

295+ gtoResultADT' @_ToExprs @_Columns @_ @a @rep1

296+ toResult

161297 (\_ -> tag tag')

162298 Nothing)

163299 (Just b)

164300 Nothing ->

165− toGADTColumns' @_Table @_Columns @_ @b

166− toColumns

167− (\_ -> toGADTColumns' @_Table @_Columns @_ @a toColumns tag Nothing)

301+ gtoResultADT' @_ToExprs @_Columns @_ @b @rep2

302+ toResult

303+ (\_ -> gtoResultADT' @_ToExprs @_Columns @_ @a @rep1 toResult tag Nothing)

168304 Nothing

169305

170− extract = extract @_Table @_Columns @_ @a . extract @_Table @_Columns @_ @b

306+ extract =

307+ extract @_ToExprs @_Columns @_ @a @rep1 .

308+ extract @_ToExprs @_Columns @_ @b @rep2

171309

172310

173−instance KnownSymbol label =>

174− GADTTable' _Table _Columns htable (M1 C ('MetaCons label _fixity _isRecord) U1)

311+instance

312+ ( meta ~ 'MetaCons label _fixity _isRecord

313+ , KnownSymbol label

314+ )

315+ => GToExprsADT' _ToExprs _Columns htable (M1 C meta U1) (M1 C meta U1)

175316 where

176− fromGADTColumns' _ tag columns

317+ gfromResultADT' _ tag columns

177318 | tag columns == tag' = Just (M1 U1)

178319 | otherwise = Nothing

179320 where

180321 tag' = Tag $ pack $ symbolVal (Proxy @label)

181322

182− toGADTColumns' _ tag _ = tag tag'

323+ gtoResultADT' _ tag _ = tag tag'

183324 where

184325 tag' = Tag $ pack $ symbolVal (Proxy @label)

185326

@@ -187,29 +328,34 @@ instance KnownSymbol label =>

187328

188329

189330instance {-# OVERLAPPABLE #-}

190− ( HTable (GColumns _Columns rep)

191− , GTable _Table _Columns (Col Result) rep

331+ ( HTable (GColumns _Columns exprs)

332+ , GToExprs _ToExprs _Columns exprs rep

333+ , meta ~ 'MetaCons label _fixity _isRecord

192334 , KnownSymbol label

193− , GADTColumns' _Columns htable (M1 C ('MetaCons label _fixity _isRecord) rep) ~

194− HProduct htable (HLabel label (HNullify (GColumns _Columns rep)))

335+ , GColumnsADT' _Columns htable (M1 C meta exprs) ~

336+ HProduct htable (HLabel label (HNullify (GColumns _Columns exprs)))

195337 )

196− => GADTTable' _Table _Columns htable (M1 C ('MetaCons label _fixity _isRecord) rep)

338+ => GToExprsADT' _ToExprs _Columns htable (M1 C meta exprs) (M1 C meta rep)

197339 where

198− fromGADTColumns' fromColumns tag (HProduct a b)

340+ gfromResultADT' fromResult tag (HProduct a b)

199341 | tag a == tag' =

200− M1 . fromGColumns @_Table @_Columns fromColumns <$>

342+ M1 . gfromResult @_ToExprs @_Columns @exprs fromResult <$>

201343 hunnullify unnullifier (hunlabel unlabeler b)

202344 | otherwise = Nothing

203345 where

204346 tag' = Tag $ pack $ symbolVal (Proxy @label)

205347

206− toGADTColumns' toColumns tag = \case

348+ gtoResultADT' toResult tag = \case

207349 Nothing -> HProduct (tag tag') (hlabel labeler (hnulls null))

208350 Just (M1 rep) -> HProduct (tag tag') $

209351 hlabel labeler $

210352 hnullify nullifier $

211− toGColumns @_Table @_Columns toColumns rep

353+ gtoResult @_ToExprs @_Columns @exprs toResult rep

212354 where

213355 tag' = Tag $ pack $ symbolVal (Proxy @label)

214356

215357 extract (HProduct a _) = a

358+

359+

360+data Const :: (a -> Exp Constraint) -> a -> a -> Exp Constraint

361+type instance Eval (Const f x a) = (Eval (f a), x ~ a)

src/Rel8/Generic/Table/Record.hsnew file+206

@@ -0,0 +1,206 @@

1+{-# language AllowAmbiguousTypes #-}

2+{-# language DataKinds #-}

3+{-# language FlexibleContexts #-}

4+{-# language FlexibleInstances #-}

5+{-# language MultiParamTypeClasses #-}

6+{-# language PolyKinds #-}

7+{-# language RankNTypes #-}

8+{-# language ScopedTypeVariables #-}

9+{-# language StandaloneKindSignatures #-}

10+{-# language TypeApplications #-}

11+{-# language TypeFamilies #-}

12+{-# language TypeOperators #-}

13+{-# language UndecidableInstances #-}

14+

15+module Rel8.Generic.Table.Record

16+ ( GTable, GColumns, GContext, gfromColumns, gtoColumns, gtable

17+ , GToExprs, gfromResult, gtoResult

18+ )

19+where

20+

21+-- base

22+import Data.Kind ( Constraint, Type )

23+import Data.Proxy ( Proxy( Proxy ) )

24+import GHC.Generics

25+ ( (:*:)( (:*:) ), K1( K1 ), M1( M1 )

26+ , C, D, S

27+ , Meta( MetaSel )

28+ )

29+import GHC.TypeLits ( KnownSymbol )

30+import Prelude hiding ( null )

31+

32+-- rel8

33+import Rel8.FCF ( Eval, Exp )

34+import Rel8.Schema.Context ( Col )

35+import Rel8.Schema.Context.Label ( HLabelable, hlabeler, hunlabeler )

36+import Rel8.Schema.HTable ( HTable )

37+import Rel8.Schema.HTable.Label ( HLabel, hlabel, hunlabel )

38+import Rel8.Schema.HTable.Product ( HProduct(..) )

39+import qualified Rel8.Schema.Kind as K

40+import Rel8.Schema.Result ( Result )

41+

42+

43+type GColumns :: (Type -> Exp K.HTable) -> (Type -> Type) -> K.HTable

44+type family GColumns _Columns rep where

45+ GColumns _Columns (M1 D _ rep) = GColumns _Columns rep

46+ GColumns _Columns (M1 C _ rep) = GColumns _Columns rep

47+ GColumns _Columns (rep1 :*: rep2) =

48+ HProduct (GColumns _Columns rep1) (GColumns _Columns rep2)

49+ GColumns _Columns (M1 S ('MetaSel ('Just label) _ _ _) (K1 _ a)) =

50+ HLabel label (Eval (_Columns a))

51+

52+

53+type GContext :: (Type -> Exp K.Context) -> (Type -> Type) -> K.Context

54+type family GContext _Context rep where

55+ GContext _Context (M1 _ _ rep) = GContext _Context rep

56+ GContext _Context (rep1 :*: _rep2) = GContext _Context rep1

57+ GContext _Context (K1 _ a) = Eval (_Context a)

58+

59+

60+type GTable

61+ :: (Type -> Exp Constraint)

62+ -> (Type -> Exp K.HTable)

63+ -> K.HContext -> (Type -> Type) -> Constraint

64+class GTable _Table _Columns context rep

65+ where

66+ gfromColumns :: ()

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

68+ -> GColumns _Columns rep context

69+ -> rep x

70+

71+ gtoColumns :: ()

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

73+ -> rep x

74+ -> GColumns _Columns rep context

75+

76+ gtable :: ()

77+ => (forall a proxy. Eval (_Table a) => proxy a -> Eval (_Columns a) context)

78+ -> GColumns _Columns rep context

79+

80+

81+instance GTable _Table _Columns context rep =>

82+ GTable _Table _Columns context (M1 D c rep)

83+ where

84+ gfromColumns fromColumns =

85+ M1 . gfromColumns @_Table @_Columns @context @rep fromColumns

86+ gtoColumns toColumns (M1 a) =

87+ gtoColumns @_Table @_Columns @context @rep toColumns a

88+ gtable = gtable @_Table @_Columns @context @rep

89+

90+

91+instance GTable _Table _Columns context rep =>

92+ GTable _Table _Columns context (M1 C c rep)

93+ where

94+ gfromColumns fromColumns =

95+ M1 . gfromColumns @_Table @_Columns @context @rep fromColumns

96+ gtoColumns toColumns (M1 a) =

97+ gtoColumns @_Table @_Columns @context @rep toColumns a

98+ gtable = gtable @_Table @_Columns @context @rep

99+

100+

101+instance

102+ ( GTable _Table _Columns context rep1

103+ , GTable _Table _Columns context rep2

104+ )

105+ => GTable _Table _Columns context (rep1 :*: rep2)

106+ where

107+ gfromColumns fromColumns (HProduct a b) =

108+ gfromColumns @_Table @_Columns @context @rep1 fromColumns a :*:

109+ gfromColumns @_Table @_Columns @context @rep2 fromColumns b

110+ gtoColumns toColumns (a :*: b) = HProduct

111+ (gtoColumns @_Table @_Columns @context @rep1 toColumns a)

112+ (gtoColumns @_Table @_Columns @context @rep2 toColumns b)

113+ gtable table = HProduct

114+ (gtable @_Table @_Columns @context @rep1 table)

115+ (gtable @_Table @_Columns @context @rep2 table)

116+

117+

118+instance

119+ ( HTable (Eval (_Columns a))

120+ , Eval (_Table a)

121+ , HLabelable context

122+ , KnownSymbol label

123+ , meta ~ 'MetaSel ('Just label) _su _ss _ds

124+ , k1 ~ K1 i a

125+ )

126+ => GTable _Table _Columns context (M1 S meta k1)

127+ where

128+ gfromColumns fromColumns = M1 . K1 . fromColumns . hunlabel hunlabeler

129+ gtoColumns toColumns (M1 (K1 a)) = hlabel hlabeler (toColumns a)

130+ gtable table = hlabel hlabeler (table (Proxy @a))

131+

132+

133+type GToExprs

134+ :: (Type -> Type -> Exp Constraint)

135+ -> (Type -> Exp K.HTable)

136+ -> (Type -> Type) -> (Type -> Type) -> Constraint

137+class GToExprs _ToExprs _Columns exprs rep where

138+ gfromResult :: ()

139+ => (forall expr a proxy.

140+ ( Eval (_ToExprs expr a)

141+ , HTable (Eval (_Columns expr))

142+ )

143+ => proxy expr

144+ -> Eval (_Columns expr) (Col Result)

145+ -> a)

146+ -> GColumns _Columns exprs (Col Result)

147+ -> rep x

148+ gtoResult :: ()

149+ => (forall expr a proxy.

150+ ( Eval (_ToExprs expr a)

151+ , HTable (Eval (_Columns expr))

152+ )

153+ => proxy expr

154+ -> a

155+ -> Eval (_Columns expr) (Col Result))

156+ -> rep x

157+ -> GColumns _Columns exprs (Col Result)

158+

159+

160+instance GToExprs _ToExprs _Columns exprs rep =>

161+ GToExprs _ToExprs _Columns (M1 D c exprs) (M1 D c rep)

162+ where

163+ gfromResult fromResult =

164+ M1 . gfromResult @_ToExprs @_Columns @exprs fromResult

165+ gtoResult toResult (M1 a) =

166+ gtoResult @_ToExprs @_Columns @exprs toResult a

167+

168+

169+instance GToExprs _ToExprs _Columns exprs rep =>

170+ GToExprs _ToExprs _Columns (M1 C c exprs) (M1 C c rep)

171+ where

172+ gfromResult fromResult =

173+ M1 . gfromResult @_ToExprs @_Columns @exprs fromResult

174+ gtoResult toResult (M1 a) =

175+ gtoResult @_ToExprs @_Columns @exprs toResult a

176+

177+

178+instance

179+ ( GToExprs _ToExprs _Columns exprs1 rep1

180+ , GToExprs _ToExprs _Columns exprs2 rep2

181+ )

182+ => GToExprs _ToExprs _Columns (exprs1 :*: exprs2) (rep1 :*: rep2)

183+ where

184+ gfromResult fromResult (HProduct a b) =

185+ gfromResult @_ToExprs @_Columns @exprs1 fromResult a :*:

186+ gfromResult @_ToExprs @_Columns @exprs2 fromResult b

187+ gtoResult toResult (a :*: b) =

188+ HProduct

189+ (gtoResult @_ToExprs @_Columns @exprs1 toResult a)

190+ (gtoResult @_ToExprs @_Columns @exprs2 toResult b)

191+

192+

193+instance

194+ ( Eval (_ToExprs exprs a)

195+ , HTable (Eval (_Columns exprs))

196+ , KnownSymbol label

197+ , meta ~ 'MetaSel ('Just label) _su _ss _ds

198+ , k1 ~ K1 i exprs

199+ , k1' ~ K1 i a

200+ )

201+ => GToExprs _ToExprs _Columns (M1 S meta k1) (M1 S meta k1')

202+ where

203+ gfromResult fromResult =

204+ M1 . K1 . fromResult (Proxy @exprs) . hunlabel hunlabeler

205+ gtoResult toResult (M1 (K1 a)) =

206+ hlabel hlabeler (toResult (Proxy @exprs) a)

src/Rel8/Kind/Algebra.hsnew file+38

@@ -0,0 +1,38 @@

1+{-# language DataKinds #-}

2+{-# language FlexibleContexts #-}

3+{-# language GADTs #-}

4+{-# language StandaloneKindSignatures #-}

6+module Rel8.Kind.Algebra

7+ ( Algebra( Product, Sum )

8+ , SAlgebra( SProduct, SSum )

9+ , KnownAlgebra( algebraSing )

10+ )

11+where

12+

13+-- base

14+import Data.Kind ( Constraint, Type )

15+import Prelude ()

16+

17+

18+type Algebra :: Type

19+data Algebra = Product | Sum

20+

21+

22+type SAlgebra :: Algebra -> Type

23+data SAlgebra algebra where

24+ SProduct :: SAlgebra 'Product

25+ SSum :: SAlgebra 'Sum

26+

27+

28+type KnownAlgebra :: Algebra -> Constraint

29+class KnownAlgebra algebra where

30+ algebraSing :: SAlgebra algebra

31+

32+

33+instance KnownAlgebra 'Product where

34+ algebraSing = SProduct

35+

36+

37+instance KnownAlgebra 'Sum where

38+ algebraSing = SSum

src/Rel8/Schema/Context/Nullify.hs+4−15

@@ -40,10 +40,8 @@ import Rel8.Schema.Name ( Name( Name ), Col(..) )

4040import Rel8.Schema.Null ( Nullify, Nullity( Null, NotNull ), Sql )

4141import Rel8.Schema.Dict ( Dict( Dict ) )

4242import Rel8.Schema.Spec ( Spec( Spec ), SSpec(..) )

43−import Rel8.Schema.Spec.ConstrainDBType

44− ( ConstrainDBType

45− , dbTypeDict, dbTypeNullity, fromNullityDict

46− )

43+import Rel8.Schema.Spec.ConstrainDBType ( ConstrainDBType )

44+import qualified Rel8.Schema.Spec.ConstrainDBType as ConstrainDBType

4745import Rel8.Table.Tag ( Tag(..), Taggable, fromAggregate, fromExpr, fromName )

4846

4947

@@ -181,17 +179,8 @@ instance HNullifiable (Dict (ConstrainDBType constraint)) where

181179

182180 hencodeTag _ = Dict

183181 hdecodeTag = mempty

184−

185− hnullifier _ _ SSpec {} dict = case dbTypeDict dict of

186− Dict -> case dbTypeNullity dict of

187− Null -> Dict

188− NotNull -> Dict

189−

190− hunnullifier SSpec {nullity} dict = case dbTypeDict dict of

191− Dict -> case nullity of

192− Null -> Dict

193− NotNull -> case dbTypeNullity dict of

194− Null -> fromNullityDict nullity Dict

182+ hnullifier _ _ = ConstrainDBType.nullifier

183+ hunnullifier = ConstrainDBType.unnullifier

195184

196185

197186type DefaultConstrainTag :: Type -> Constraint

src/Rel8/Schema/Context/Result.hsnew file+64

@@ -0,0 +1,64 @@

1+{-# language DataKinds #-}

2+{-# language NamedFieldPuns #-}

3+{-# language TypeFamilies #-}

4+{-# language UndecidableInstances #-}

6+module Rel8.Schema.Context.Result

7+ ( relabel

8+ , null, nullifier, unnullifier

9+ , vectorizer, unvectorizer

10+ )

11+where

12+

13+-- base

14+import Prelude hiding ( null )

15+

16+-- rel8

17+import Rel8.Schema.Context ( Col(..) )

18+import Rel8.Schema.HTable.Identity ( HIdentity(..) )

19+import Rel8.Schema.Null ( Nullify, Nullity( Null, NotNull ) )

20+import Rel8.Schema.Result ( Result )

21+import Rel8.Schema.Spec ( Spec( Spec ), SSpec(..) )

22+

23+

24+relabel :: ()

25+ => HIdentity ('Spec labels necessity a) (Col Result)

26+ -> HIdentity ('Spec relabels necessity a) (Col Result)

27+relabel (HIdentity (Result a)) = HIdentity (Result a)

28+

29+

30+null :: Col Result ('Spec labels necessity (Maybe a))

31+null = Result Nothing

32+

33+

34+nullifier :: ()

35+ => SSpec ('Spec labels necessity a)

36+ -> Col Result ('Spec labels necessity a)

37+ -> Col Result ('Spec labels necessity (Nullify a))

38+nullifier SSpec {nullity} (Result a) = Result $ case nullity of

39+ Null -> a

40+ NotNull -> Just a

41+

42+

43+unnullifier :: ()

44+ => SSpec ('Spec labels necessity a)

45+ -> Col Result ('Spec labels necessity (Nullify a))

46+ -> Maybe (Col Result ('Spec labels necessity a))

47+unnullifier SSpec {nullity} (Result a) =

48+ case nullity of

49+ Null -> pure $ Result a

50+ NotNull -> Result <$> a

51+

52+

53+vectorizer :: Functor f

54+ => SSpec ('Spec labels necessity a)

55+ -> f (Col Result ('Spec labels necessity a))

56+ -> Col Result ('Spec labels necessity (f a))

57+vectorizer _ = Result . fmap (\(Result a) -> a)

58+

59+

60+unvectorizer :: Functor f

61+ => SSpec ('Spec labels necessity a)

62+ -> Col Result ('Spec labels necessity (f a))

63+ -> f (Col Result ('Spec labels necessity a))

64+unvectorizer _ (Result results) = Result <$> results

src/Rel8/Schema/Spec/ConstrainDBType.hs+30−5

@@ -2,6 +2,7 @@

22{-# language DataKinds #-}

33{-# language FlexibleInstances #-}

44{-# language MultiParamTypeClasses #-}

5+{-# language NamedFieldPuns #-}

56{-# language QuantifiedConstraints #-}

67{-# language StandaloneKindSignatures #-}

78{-# language TypeFamilies #-}

@@ -9,9 +10,8 @@

910

1011module Rel8.Schema.Spec.ConstrainDBType

1112 ( ConstrainDBType

12− , dbTypeNullity

13− , dbTypeDict

14− , fromNullityDict

13+ , dbTypeNullity, dbTypeDict

14+ , nullifier, unnullifier

1515 )

1616where

1717

@@ -21,8 +21,12 @@ import Prelude

2121

2222-- rel8

2323import Rel8.Schema.Dict ( Dict( Dict ) )

24−import Rel8.Schema.Null ( Unnullify, Nullity( Null, NotNull ), Sql, nullable )

25−import Rel8.Schema.Spec ( Spec( Spec ) )

24+import Rel8.Schema.Null

25+ ( Nullify, Unnullify

26+ , Nullity( Null, NotNull )

27+ , Sql, nullable

28+ )

29+import Rel8.Schema.Spec ( Spec( Spec ), SSpec( SSpec, nullity ) )

2630

2731

2832type ConstrainDBType :: (Type -> Constraint) -> Spec -> Constraint

@@ -62,3 +66,24 @@ dbTypeDict = step2 . step1

6266fromNullityDict :: Nullity a -> Dict c (Unnullify a) -> Dict (ConstrainDBType c) ('Spec l n a)

6367fromNullityDict Null Dict = Dict

6468fromNullityDict NotNull Dict = Dict

69+

70+

71+nullifier :: ()

72+ => SSpec ('Spec labels necessity a)

73+ -> Dict (ConstrainDBType c) ('Spec labels necessity a)

74+ -> Dict (ConstrainDBType c) ('Spec labels necessity (Nullify a))

75+nullifier SSpec {} dict = case dbTypeDict dict of

76+ Dict -> case dbTypeNullity dict of

77+ Null -> Dict

78+ NotNull -> Dict

79+

80+

81+unnullifier :: ()

82+ => SSpec ('Spec labels necessity a)

83+ -> Dict (ConstrainDBType c) ('Spec labels necessity (Nullify a))

84+ -> Dict (ConstrainDBType c) ('Spec labels necessity a)

85+unnullifier SSpec {nullity} dict = case dbTypeDict dict of

86+ Dict -> case nullity of

87+ Null -> Dict

88+ NotNull -> case dbTypeNullity dict of

89+ Null -> fromNullityDict nullity Dict

src/Rel8/Table.hs+38−70

@@ -18,7 +18,6 @@ module Rel8.Table

1818 ( Table (Columns, Context, Unreify, toColumns, fromColumns, reify, unreify)

1919 , Congruent

2020 , TTable, TColumns, TContext, TUnreify

21− , null, nullifier, unnullifier

2221 )

2322where

2423

@@ -34,13 +33,21 @@ import Prelude hiding ( null )

3433

3534-- rel8

3635import Rel8.FCF ( Eval, Exp )

36+import Rel8.Kind.Algebra ( KnownAlgebra )

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

3838import Rel8.Generic.Table

39− ( GTable, GColumns, GContext, fromGColumns, toGColumns

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

40+ , GAlgebra

4041 )

4142import Rel8.Generic.Record ( Record(..) )

43+import Rel8.Generic.Reify ( ARep )

4244import Rel8.Schema.Context ( Col(..) )

4345import Rel8.Schema.Context.Label ( Labelable, labeler, unlabeler )

46+import Rel8.Schema.Context.Result

47+ ( relabel

48+ , null, nullifier, unnullifier

49+ , vectorizer, unvectorizer

50+ )

4451import Rel8.Schema.HTable ( HTable )

4552import Rel8.Schema.HTable.Either ( HEitherTable(..) )

4653import Rel8.Schema.HTable.Identity ( HIdentity(..) )

@@ -53,14 +60,14 @@ import Rel8.Schema.HTable.These ( HTheseTable(..) )

5360import Rel8.Schema.HTable.Type ( HType( HType ) )

5461import Rel8.Schema.HTable.Vectorize ( hvectorize, hunvectorize )

5562import qualified Rel8.Schema.Kind as K

56−import Rel8.Schema.Null ( Nullify, Nullity( Null, NotNull ), Sql )

63+import Rel8.Schema.Null ( Sql )

5764import Rel8.Schema.Reify

5865 ( Reify, Col( Reify ), hreify, hunreify

5966 , UnwrapReify

6067 , notReify

6168 )

6269import Rel8.Schema.Result ( Result )

63−import Rel8.Schema.Spec ( Spec( Spec ), SSpec(..), KnownSpec )

70+import Rel8.Schema.Spec ( KnownSpec )

6471import Rel8.Type ( DBType )

6572import Rel8.Type.Tag ( EitherTag( IsLeft, IsRight ), MaybeTag( IsJust ) )

6673

@@ -96,31 +103,49 @@ class (HTable (Columns a), context ~ Context a) => Table context a | a -> contex

96103 reify :: context :~: Reify ctx -> Unreify a -> a

97104 unreify :: context :~: Reify ctx -> a -> Unreify a

98105

99− type Columns a = GColumns TColumns (Rep (Record a))

100− type Context a = GContext TContext (Rep (Record a))

106+ type Columns a = Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))

107+ type Context a = Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record a)))

101108 type Unreify a = DefaultUnreify a

102109

103110 default toColumns ::

104111 ( Generic (Record a)

105− , GTable (TTable context) TColumns (Col context) (Rep (Record a))

106− , Columns a ~ GColumns TColumns (Rep (Record a))

112+ , KnownAlgebra (GAlgebra (Rep (Record a)))

113+ , Eval (GGTable (GAlgebra (Rep (Record a))) (TTable context) TColumns (Col context) (Rep (Record a)))

114+ , Columns a ~ Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))

115+ , Context a ~ Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record a)))

107116 )

108117 => a -> Columns a (Col context)

109118 toColumns =

110− toGColumns @(TTable context) @TColumns toColumns .

119+ ggtoColumns

120+ @(GAlgebra (Rep (Record a)))

121+ @(TTable context)

122+ @TColumns

123+ @TContext

124+ id

125+ id

126+ toColumns .

111127 from .

112128 Record

113129

114130 default fromColumns ::

115131 ( Generic (Record a)

116− , GTable (TTable context) TColumns (Col context) (Rep (Record a))

117− , Columns a ~ GColumns TColumns (Rep (Record a))

132+ , KnownAlgebra (GAlgebra (Rep (Record a)))

133+ , Eval (GGTable (GAlgebra (Rep (Record a))) (TTable context) TColumns (Col context) (Rep (Record a)))

134+ , Columns a ~ Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))

135+ , Context a ~ Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record a)))

118136 )

119137 => Columns a (Col context) -> a

120138 fromColumns =

121139 unrecord .

122140 to .

123− fromGColumns @(TTable context) @TColumns fromColumns

141+ ggfromColumns

142+ @(GAlgebra (Rep (Record a)))

143+ @(TTable context)

144+ @TColumns

145+ @TContext

146+ id

147+ id

148+ fromColumns

124149

125150 default reify ::

126151 ( Generic (Record a)

@@ -180,6 +205,7 @@ type family DefaultUnreify a where

180205 DefaultUnreify (t a b c) = t (Unreify a) (Unreify b) (Unreify c)

181206 DefaultUnreify (t a b) = t (Unreify a) (Unreify b)

182207 DefaultUnreify (t a) = t (Unreify a)

208+ DefaultUnreify a = ARep (GMap TUnreify (Rep a))

183209

184210

185211-- | Any 'HTable' is also a 'Table'.

@@ -242,9 +268,6 @@ instance (Table Result a, Table Result b) => Table Result (Either a b) where

242268 where

243269 err = error "Either.fromColumns: mismatch between tag and data"

244270

245− reify = notReify

246− unreify = notReify

247−

248271

249272instance Table Result a => Table Result [a] where

250273 type Columns [a] = HListTable (Columns a)

@@ -253,9 +276,6 @@ instance Table Result a => Table Result [a] where

253276 toColumns = hvectorize vectorizer . fmap toColumns

254277 fromColumns = fmap fromColumns . hunvectorize unvectorizer

255278

256− reify = notReify

257− unreify = notReify

258−

259279

260280instance Table Result a => Table Result (Maybe a) where

261281 type Columns (Maybe a) = HMaybeTable (Columns a)

@@ -277,9 +297,6 @@ instance Table Result a => Table Result (Maybe a) where

277297 Nothing -> error "Maybe.fromColumns: mismatch between tag and data"

278298 Just just -> fromColumns just

279299

280− reify = notReify

281− unreify = notReify

282−

283300

284301instance Table Result a => Table Result (NonEmpty a) where

285302 type Columns (NonEmpty a) = HNonEmptyTable (Columns a)

@@ -288,9 +305,6 @@ instance Table Result a => Table Result (NonEmpty a) where

288305 toColumns = hvectorize vectorizer . fmap toColumns

289306 fromColumns = fmap fromColumns . hunvectorize unvectorizer

290307

291− reify = notReify

292− unreify = notReify

293−

294308

295309instance (Table Result a, Table Result b) => Table Result (These a b) where

296310 type Columns (These a b) = HTheseTable (Columns a) (Columns b)

@@ -328,9 +342,6 @@ instance (Table Result a, Table Result b) => Table Result (These a b) where

328342 , hjust = hlabel labeler (hunlabel unlabeler hthere)

329343 }

330344

331− reify = notReify

332− unreify = notReify

333−

334345

335346instance (Table context a, Table context b, Labelable context)

336347 => Table context (a, b)

@@ -377,46 +388,3 @@ instance

377388type Congruent :: Type -> Type -> Constraint

378389class Columns a ~ Columns b => Congruent a b

379390instance Columns a ~ Columns b => Congruent a b

380−

381−

382−null :: Col Result ('Spec labels necessity (Maybe a))

383−null = Result Nothing

384−

385−

386−nullifier :: ()

387− => SSpec ('Spec labels necessity a)

388− -> Col Result ('Spec labels necessity a)

389− -> Col Result ('Spec labels necessity (Nullify a))

390−nullifier SSpec {nullity} (Result a) = Result $ case nullity of

391− Null -> a

392− NotNull -> Just a

393−

394−

395−unnullifier :: ()

396− => SSpec ('Spec labels necessity a)

397− -> Col Result ('Spec labels necessity (Nullify a))

398− -> Maybe (Col Result ('Spec labels necessity a))

399−unnullifier SSpec {nullity} (Result a) =

400− case nullity of

401− Null -> pure $ Result a

402− NotNull -> Result <$> a

403−

404−

405−vectorizer :: Functor f

406− => SSpec ('Spec labels necessity a)

407− -> f (Col Result ('Spec labels necessity a))

408− -> Col Result ('Spec labels necessity (f a))

409−vectorizer _ = Result . fmap (\(Result a) -> a)

410−

411−

412−unvectorizer :: Functor f

413− => SSpec ('Spec labels necessity a)

414− -> Col Result ('Spec labels necessity (f a))

415− -> f (Col Result ('Spec labels necessity a))

416−unvectorizer _ (Result results) = Result <$> results

417−

418−

419−relabel :: ()

420− => HIdentity ('Spec labels necessity a) (Col Result)

421− -> HIdentity ('Spec relabels necessity a) (Col Result)

422−relabel (HIdentity (Result a)) = HIdentity (Result a)

src/Rel8/Table/Eq.hs+18−7

@@ -24,7 +24,6 @@ import Data.Foldable ( foldl' )

2424import Data.Functor.Const ( Const( Const ), getConst )

2525import Data.Kind ( Constraint, Type )

2626import Data.List.NonEmpty ( NonEmpty( (:|) ) )

27−import Data.Proxy ( Proxy )

2827import GHC.Generics ( Rep )

2928import Prelude

3029

@@ -34,7 +33,11 @@ import Rel8.Expr.Bool ( (||.), (&&.) )

3433import Rel8.Expr.Eq ( (==.), (/=.) )

3534import Rel8.FCF ( Eval, Exp )

3635import Rel8.Generic.Record ( Record )

37−import Rel8.Generic.Table ( GTable, GColumns, gtable )

36+import Rel8.Generic.Table

37+ ( GGTable, GGColumns, ggtable

38+ , GAlgebra

39+ )

40+import Rel8.Kind.Algebra ( KnownAlgebra )

3841import Rel8.Schema.Dict ( Dict( Dict ) )

3942import Rel8.Schema.HTable

4043 ( HTable, HConstrainTable

@@ -43,7 +46,7 @@ import Rel8.Schema.HTable

4346import Rel8.Schema.HTable.Type ( HType(..) )

4447import Rel8.Schema.Kind ( Context )

4548import Rel8.Schema.Null ( Sql )

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

49+import Rel8.Schema.Spec.ConstrainDBType ( ConstrainDBType, nullifier )

4750import Rel8.Table ( Table, Columns, toColumns, TColumns )

4851import Rel8.Type.Eq ( DBEq )

4952

@@ -56,13 +59,21 @@ class Table Expr a => EqTable a where

5659 eqTable :: Columns a (Dict (ConstrainDBType DBEq))

5760

5861 default eqTable ::

59− ( GTable TEqTable TColumns (Dict (ConstrainDBType DBEq)) (Rep (Record a))

60− , Columns a ~ GColumns TColumns (Rep (Record a))

62+ ( KnownAlgebra (GAlgebra (Rep (Record a)))

63+ , Eval (GGTable (GAlgebra (Rep (Record a))) TEqTable TColumns (Dict (ConstrainDBType DBEq)) (Rep (Record a)))

64+ , Columns a ~ Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))

6165 )

6266 => Columns a (Dict (ConstrainDBType DBEq))

63− eqTable = gtable @TEqTable @TColumns @_ @(Rep (Record a)) table

67+ eqTable =

68+ ggtable

69+ @(GAlgebra (Rep (Record a)))

70+ @TEqTable

71+ @TColumns

72+ @(Rep (Record a))

73+ table

74+ nullifier

6475 where

65− table (_ :: Proxy x) = eqTable @x

76+ table (_ :: proxy x) = eqTable @x

6677

6778

6879data TEqTable :: Type -> Exp Constraint

src/Rel8/Table/Ord.hs+18−7

@@ -21,7 +21,6 @@ where

2121-- base

2222import Data.Functor.Const ( Const( Const ), getConst )

2323import Data.Kind ( Constraint, Type )

24−import Data.Proxy ( Proxy )

2524import GHC.Generics ( Rep )

2625import Prelude hiding ( seq )

2726

@@ -32,7 +31,11 @@ import Rel8.Expr.Eq ( (==.) )

3231import Rel8.Expr.Ord ( (<.), (>.) )

3332import Rel8.FCF ( Eval, Exp )

3433import Rel8.Generic.Record ( Record )

35−import Rel8.Generic.Table ( GTable, GColumns, gtable )

34+import Rel8.Generic.Table

35+ ( GGTable, GGColumns, ggtable

36+ , GAlgebra

37+ )

38+import Rel8.Kind.Algebra ( KnownAlgebra )

3639import Rel8.Schema.Dict ( Dict( Dict ) )

3740import Rel8.Schema.HTable

3841 ( HTable, HConstrainTable

@@ -41,7 +44,7 @@ import Rel8.Schema.HTable

4144import Rel8.Schema.HTable.Type ( HType(..) )

4245import Rel8.Schema.Kind ( Context )

4346import Rel8.Schema.Null (Sql)

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

47+import Rel8.Schema.Spec.ConstrainDBType ( ConstrainDBType, nullifier )

4548import Rel8.Table ( Table, Columns, toColumns, TColumns )

4649import Rel8.Table.Bool ( bool )

4750import Rel8.Table.Eq ( EqTable )

@@ -57,13 +60,21 @@ class EqTable a => OrdTable a where

5760 ordTable :: Columns a (Dict (ConstrainDBType DBOrd))

5861

5962 default ordTable ::

60− ( GTable TOrdTable TColumns (Dict (ConstrainDBType DBOrd)) (Rep (Record a))

61− , Columns a ~ GColumns TColumns (Rep (Record a))

63+ ( KnownAlgebra (GAlgebra (Rep (Record a)))

64+ , Eval (GGTable (GAlgebra (Rep (Record a))) TOrdTable TColumns (Dict (ConstrainDBType DBOrd)) (Rep (Record a)))

65+ , Columns a ~ Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))

6266 )

6367 => Columns a (Dict (ConstrainDBType DBOrd))

64− ordTable = gtable @TOrdTable @TColumns @_ @(Rep (Record a)) table

68+ ordTable =

69+ ggtable

70+ @(GAlgebra (Rep (Record a)))

71+ @TOrdTable

72+ @TColumns

73+ @(Rep (Record a))

74+ table

75+ nullifier

6576 where

66− table (_ :: Proxy x) = ordTable @x

77+ table (_ :: proxy x) = ordTable @x

6778

6879

6980data TOrdTable :: Type -> Exp Constraint

src/Rel8/Table/Serialize.hs+35−52

@@ -25,11 +25,7 @@ where

2525import Data.Bifunctor ( bimap )

2626import Data.Kind ( Constraint, Type )

2727import Data.List.NonEmpty ( NonEmpty )

28−import GHC.Generics

29− ( Generic, Rep, from, to

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

31− )

32−import GHC.TypeLits ( KnownSymbol )

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

3329import Prelude

3430

3531-- hasql

@@ -38,13 +34,15 @@ import qualified Hasql.Decoders as Hasql

3834-- rel8

3935import Rel8.Expr ( Expr, Col(..) )

4036import Rel8.Expr.Serialize ( slitExpr, sparseValue )

37+import Rel8.FCF ( Eval, Exp )

4138import Rel8.Generic.Record ( Record(..) )

42−import Rel8.Generic.Table ( GColumns )

39+import Rel8.Generic.Table

40+ ( GGToExprs, GGColumns, ggfromResult, ggtoResult

41+ , GAlgebra

42+ )

43+import Rel8.Kind.Algebra ( KnownAlgebra )

4344import Rel8.Schema.Context ( Col(..) )

44−import Rel8.Schema.Context.Label ( labeler, unlabeler )

4545import Rel8.Schema.HTable ( HTable, htabulate, htabulateA, hfield, hspecs )

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

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

4846import Rel8.Schema.HTable.Type ( HType(..) )

4947import Rel8.Schema.Null ( NotNull, Sql )

5048import Rel8.Schema.Result ( Result )

@@ -72,56 +70,41 @@ class Table Expr exprs => ToExprs exprs a where

7270

7371 default fromResult ::

7472 ( Generic (Record a)

75− , GToExprs (Rep (Record exprs)) (Rep (Record a))

76− , Columns exprs ~ GColumns TColumns (Rep (Record exprs))

73+ , KnownAlgebra (GAlgebra (Rep (Record exprs)))

74+ , Eval (GGToExprs (GAlgebra (Rep (Record exprs))) TToExprs TColumns (Rep (Record exprs)) (Rep (Record a)))

75+ , Columns exprs ~ Eval (GGColumns (GAlgebra (Rep (Record exprs))) TColumns (Rep (Record exprs)))

7776 )

7877 => Columns exprs (Col Result) -> a

79− fromResult = unrecord . to . gfromResult @(Rep (Record exprs))

78+ fromResult =

79+ unrecord .

80+ to .

81+ ggfromResult

82+ @(GAlgebra (Rep (Record exprs)))

83+ @TToExprs

84+ @TColumns

85+ @(Rep (Record exprs))

86+ (\(_ :: proxy expr) -> fromResult @expr)

8087

8188 default toResult ::

8289 ( Generic (Record a)

83− , GToExprs (Rep (Record exprs)) (Rep (Record a))

84− , Columns exprs ~ GColumns TColumns (Rep (Record exprs))

90+ , KnownAlgebra (GAlgebra (Rep (Record exprs)))

91+ , Eval (GGToExprs (GAlgebra (Rep (Record exprs))) TToExprs TColumns (Rep (Record exprs)) (Rep (Record a)))

92+ , Columns exprs ~ Eval (GGColumns (GAlgebra (Rep (Record exprs))) TColumns (Rep (Record exprs)))

8593 )

8694 => a -> Columns exprs (Col Result)

87− toResult = gtoResult @(Rep (Record exprs)) . from . Record

88−

89−

90−type GToExprs :: (Type -> Type) -> (Type -> Type) -> Constraint

91−class GToExprs exprs rep where

92− gfromResult :: GColumns TColumns exprs (Col Result) -> rep x

93− gtoResult :: rep x -> GColumns TColumns exprs (Col Result)

94−

95−

96−instance GToExprs exprs rep => GToExprs (M1 D c exprs) (M1 D c rep) where

97− gfromResult = M1 . gfromResult @exprs

98− gtoResult (M1 a) = gtoResult @exprs a

99−

100−

101−instance GToExprs exprs rep => GToExprs (M1 C c exprs) (M1 C c rep) where

102− gfromResult = M1 . gfromResult @exprs

103− gtoResult (M1 a) = gtoResult @exprs a

104−

105−

106−instance (GToExprs exprs1 rep1, GToExprs exprs2 rep2) =>

107− GToExprs (exprs1 :*: exprs2) (rep1 :*: rep2)

108− where

109− gfromResult (HProduct a b) = gfromResult @exprs1 a :*: gfromResult @exprs2 b

110− gtoResult (a :*: b) = HProduct (gtoResult @exprs1 a) (gtoResult @exprs2 b)

111−

112−

113−instance

114− ( ToExprs exprs a

115− , KnownSymbol label

116− , GColumns TColumns (M1 S meta k1) ~ HLabel label (Columns exprs)

117− , meta ~ 'MetaSel ('Just label) _su _ss _ds

118− , k1 ~ K1 i exprs

119− , k1' ~ K1 i a

120− )

121− => GToExprs (M1 S meta k1) (M1 S meta k1')

122− where

123− gfromResult = M1 . K1 . fromResult @exprs . hunlabel unlabeler

124− gtoResult (M1 (K1 a)) = hlabel labeler (toResult @exprs a)

95+ toResult =

96+ ggtoResult

97+ @(GAlgebra (Rep (Record exprs)))

98+ @TToExprs

99+ @TColumns

100+ @(Rep (Record exprs))

101+ (\(_ :: proxy expr) -> toResult @expr) .

102+ from .

103+ Record

104+

105+

106+data TToExprs :: Type -> Type -> Exp Constraint

107+type instance Eval (TToExprs exprs a) = ToExprs exprs a

125108

126109

127110instance {-# OVERLAPPABLE #-} (Sql DBType a, x ~ Expr a) => ToExprs x a where