66dc44d · rel8 · git.iko.soy

git.iko.soy/rel8

on master help sign in

Teach Table and friends about Sum types

66dc44dShane O'Brien6 years ago

rel8.cabal+6−2

compare with master

unifiedsplit

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

64 Rel8.FCF

66+ Rel8.Kind.Algebra

66 Rel8.Kind.Context

67 Rel8.Kind.Context

67 Rel8.Kind.Labels

68 Rel8.Kind.Labels

68 Rel8.Kind.Necessity

69 Rel8.Kind.Necessity

70 Rel8.Generic.Map

71 Rel8.Generic.Map

71 Rel8.Generic.Record

72 Rel8.Generic.Record

73+ Rel8.Generic.Reify

74+ Rel8.Generic.Rel8able

75+ Rel8.Generic.Rel8able.Test

72 Rel8.Generic.Table

76 Rel8.Generic.Table

73 Rel8.Generic.Table.ADT

77 Rel8.Generic.Table.ADT

78+ Rel8.Generic.Table.Record

75 Rel8.Order

80 Rel8.Order

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

96 Rel8.Schema.Context

101 Rel8.Schema.Context

97 Rel8.Schema.Context.Label

102 Rel8.Schema.Context.Label

98 Rel8.Schema.Context.Nullify

103 Rel8.Schema.Context.Nullify

104+ Rel8.Schema.Context.Result

99 Rel8.Schema.Dict

105 Rel8.Schema.Dict

100 Rel8.Schema.Field

106 Rel8.Schema.Field

101− Rel8.Schema.Generic

102− Rel8.Schema.Generic.Test

103 Rel8.Schema.HKD

107 Rel8.Schema.HKD

104 Rel8.Schema.HTable

108 Rel8.Schema.HTable

105 Rel8.Schema.HTable.Either

109 Rel8.Schema.HTable.Either

src/Rel8.hs+2−2

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

260import Rel8.Expr.Ord

261import Rel8.Expr.Order

262import Rel8.Expr.Serialize

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

263import Rel8.Kind.Necessity

264import Rel8.Kind.Necessity

264import Rel8.Order

265import Rel8.Order

265import Rel8.Query

266import Rel8.Query

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

281import Rel8.Schema.Column

282import Rel8.Schema.Column

282import Rel8.Schema.Context.Label

283import Rel8.Schema.Context.Label

283import Rel8.Schema.Field

284import Rel8.Schema.Field

284−import Rel8.Schema.Generic

285import Rel8.Schema.HKD

286import Rel8.Schema.HTable

287import Rel8.Schema.Name

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

294import Rel8.Statement.Select

295import Rel8.Statement.Update

296import Rel8.Statement.View

297−import Rel8.Table hiding ( null )

297+import Rel8.Table

298import Rel8.Table.Aggregate

299import Rel8.Table.Alternative

300import 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 #-}

1{-# language DataKinds #-}

3{-# language DataKinds #-}

2{-# language DefaultSignatures #-}

4{-# language DefaultSignatures #-}

3{-# language FlexibleContexts #-}

5{-# language FlexibleContexts #-}

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

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

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

14−module Rel8.Schema.Generic

16+module Rel8.Generic.Rel8able

15− ( Rel8able

16− , KRel8able

17+ ( KRel8able, Rel8able

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

19+ , Algebra

17 )

20 )

18where

21where

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

30 , Reifiable, contextSing

33 , Reifiable, contextSing

31 , sLabelable, sReifiable

34 , sLabelable, sReifiable

32 )

35 )

36+import Rel8.FCF ( Eval, Exp )

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

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

34import Rel8.Generic.Record ( Record(..) )

38import 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(..) )

36import Rel8.Schema.Context ( Col )

48import Rel8.Schema.Context ( Col )

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

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

38import Rel8.Schema.Dict ( Dict( Dict ) )

50import Rel8.Schema.Dict ( Dict( Dict ) )

39import Rel8.Schema.HTable ( HTable )

51import Rel8.Schema.HTable ( HTable )

40import qualified Rel8.Schema.Kind as K

52import qualified Rel8.Schema.Kind as K

41import Rel8.Schema.Name ( Name )

53import 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 )

43import Rel8.Table

59import Rel8.Table

44 ( Table, Columns, Context, fromColumns, toColumns

60 ( Table, Columns, Context, fromColumns, toColumns

45 , Unreify, reify, unreify

61 , Unreify, reify, unreify

46− , TTable, TColumns, TUnreify

62+ , TTable, TColumns, TContext, TUnreify

47 )

63 )

66+instance

67+ ( Rel8able t

68+ , GContext t context ~ context

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

69+ , Labelable context

70+ , Reifiable context

71+ )

51− Table context (t context)

72+ => Table context (t context)

52 where

73 where

53− type Columns (t context) = GRep t

74+ type Columns (t context) = GColumns t

54 type Context (t context) = context

75 type Context (t context) = context

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

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

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

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

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

116-- @

137-- @

117type Rel8able :: K.Rel8able -> Constraint

138type Rel8able :: K.Rel8able -> Constraint

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

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

119− type GRep t :: K.HTable

140+ type Algebra t :: K.Algebra

141+ type GColumns t :: K.HTable

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

120

143

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

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

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

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

123

146

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

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

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

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

126

149

127 greify :: (Labelable context, Reifiable context)

150 greify :: (Labelable context, Reifiable context)

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

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

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

130 gunreify :: (Labelable context, Reifiable context)

153 gunreify :: (Labelable context, Reifiable context)

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

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

132

155

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

133− type GRep t = GColumns TColumns (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)))))

134

159

135 default gfromColumns :: forall context.

160 default gfromColumns :: forall context.

136 ( Generic (Record (t (Reify context)))

161 ( Generic (Record (t (Reify context)))

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

162+ , KnownAlgebra (Algebra t)

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

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

139 )

166 )

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

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

141 gfromColumns =

168 gfromColumns =

142 unrecord .

169 unrecord .

143 to .

170 to .

171+ ggfromColumns

172+ @(Algebra t)

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

173+ @(TTable (Reify context))

174+ @TColumns

175+ @TContext

176+ (fromContext @t @context)

177+ (toContext @t @context)

178+ fromColumns

145

179

146 default gtoColumns :: forall context.

180 default gtoColumns :: forall context.

147 ( Generic (Record (t (Reify context)))

181 ( Generic (Record (t (Reify context)))

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

182+ , KnownAlgebra (Algebra t)

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

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

150 )

186 )

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

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

152 gtoColumns =

188 gtoColumns =

189+ ggtoColumns

190+ @(Algebra t)

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

191+ @(TTable (Reify context))

192+ @TColumns

193+ @TContext

194+ (fromContext @t @context)

195+ (toContext @t @context)

196+ toColumns .

154 from .

197 from .

155 Record

198 Record

156

199

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

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

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

182 from .

225 from .

183 Record

226 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 @@

11{-# options_ghc -O0 #-}

13−module Rel8.Schema.Generic.Test

13+module Rel8.Generic.Rel8able.Test

14− ( module Rel8.Schema.Generic.Test

14+ ( module Rel8.Generic.Rel8able.Test

15 )

16where

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

116 (Column f Char)

117 deriving stock Generic

118 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 @@

1{-# language AllowAmbiguousTypes #-}

2{-# language DataKinds #-}

3+{-# language FlexibleContexts #-}

3{-# language FlexibleInstances #-}

4{-# language FlexibleInstances #-}

4{-# language MultiParamTypeClasses #-}

5{-# language MultiParamTypeClasses #-}

5−{-# language PolyKinds #-}

6{-# language RankNTypes #-}

7{-# language ScopedTypeVariables #-}

8{-# language StandaloneKindSignatures #-}

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

12{-# language UndecidableInstances #-}

14module Rel8.Generic.Table

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

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

16+ , GGToExprs, ggfromResult, ggtoResult

17+ , GAlgebra

16 )

18 )

17where

19where

19-- base

21-- base

20import Data.Kind ( Constraint, Type )

22import Data.Kind ( Constraint, Type )

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

22−import GHC.Generics

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

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

24− , C, D, S

25− , Meta( MetaSel )

26− )

27−import GHC.TypeLits ( KnownSymbol )

28−import Prelude hiding ( null )

24+import Prelude ()

30-- rel8

26-- rel8

31import Rel8.FCF ( Eval, Exp )

27import Rel8.FCF ( Eval, Exp )

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

28+import Rel8.Generic.Table.ADT

33−import Rel8.Schema.HTable ( HTable )

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

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

30+ , GToExprsADT, gtoResultADT, gfromResultADT

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

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 )

36import qualified Rel8.Schema.Kind as K

42import 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+

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

58+ GTable _Table _Columns context rep

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))

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

62+ GTableADT _Table _Columns context rep

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

64+

50−type family GContext _Context rep where

65+data GGToExprs

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

66+ :: Algebra

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

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

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

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

56−type GTable

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

57− :: (Type -> Exp Constraint)

79+ GToExprsADT _ToExprs _Columns exprs rep

80+

81+

82+data GGColumns

83+ :: Algebra

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

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

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

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+

60−class GTable _Table _Columns context rep

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

61− where

133+ ( KnownAlgebra algebra

62− fromGColumns :: ()

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

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

135+ )

64− -> GColumns _Columns rep context

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

65− -> rep x

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

66−

67− toGColumns :: ()

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

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

69− -> rep x

139+ -> rep x

70− -> GColumns _Columns rep context

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

71−

141+ggtoColumns = case algebraSing @algebra of

72− gtable :: ()

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

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

143+ SSum -> gtoColumnsADT @_Table @_Columns

144+

145+

74− -> GColumns _Columns rep context

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

75−

147+ ( KnownAlgebra algebra

76−

77−instance GTable _Table _Columns context rep =>

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

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

79− where

149+ )

80− fromGColumns fromColumns =

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

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

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

82− toGColumns toColumns (M1 a) =

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

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

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

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

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

85−

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

86−

156+ggtable = case algebraSing @algebra of

87−instance GTable _Table _Columns context rep =>

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

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

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

95−

159+

96−

160+

97−instance

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

98− ( GTable _Table _Columns context rep1

162+ ( KnownAlgebra algebra

99− , GTable _Table _Columns context rep2

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

100 )

164 )

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

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

102− where

166+ => proxy expr

103− fromGColumns fromColumns (HProduct a b) =

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

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

168+ -> a)

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

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

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

170+ -> rep x

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

171+ggfromResult = case algebraSing @algebra of

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

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

109− gtable table = HProduct

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

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

174+

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

175+

112−

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

113−

177+ ( KnownAlgebra algebra

114−instance

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

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

121 )

179 )

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

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

123− where

181+ => proxy expr

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

182+ -> a

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

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

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

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 @@

1{-# language AllowAmbiguousTypes #-}

2{-# language DataKinds #-}

3+{-# language FlexibleContexts #-}

3{-# language FlexibleInstances #-}

4{-# language FlexibleInstances #-}

4{-# language LambdaCase #-}

5{-# language LambdaCase #-}

5{-# language MultiParamTypeClasses #-}

6{-# language MultiParamTypeClasses #-}

7+{-# language PolyKinds #-}

6{-# language RankNTypes #-}

8{-# language RankNTypes #-}

7{-# language ScopedTypeVariables #-}

9{-# language ScopedTypeVariables #-}

8{-# language StandaloneKindSignatures #-}

10{-# language StandaloneKindSignatures #-}

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

12{-# language UndecidableInstances #-}

14{-# language UndecidableInstances #-}

14module Rel8.Generic.Table.ADT

16module Rel8.Generic.Table.ADT

15− ( GADTTable (fromGADTColumns, toGADTColumns)

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

16− , GADTColumns

18+ , GToExprsADT, gfromResultADT, gtoResultADT

17 )

19 )

18where

20where

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

31-- rel8

33-- rel8

32import Rel8.FCF ( Eval, Exp )

34import 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+ )

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

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

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

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

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

36−import Rel8.Schema.HTable ( HTable )

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

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

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

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

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

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

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

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

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

41import qualified Rel8.Schema.Kind as K

47import qualified Rel8.Schema.Kind as K

48+import Rel8.Schema.Null ( Nullify )

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

42import Rel8.Schema.Result ( Result )

50import Rel8.Schema.Result ( Result )

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

44import Rel8.Type.Tag ( Tag( Tag ) )

51import Rel8.Type.Tag ( Tag( Tag ) )

46-- text

53-- text

47import Data.Text ( pack )

54import Data.Text ( pack )

50−type GADTColumns

57+type GColumnsADT

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

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

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

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

53−type family GADTColumns _Columns rep where

60+type family GColumnsADT _Columns rep where

54− GADTColumns _Columns (M1 D _ rep) =

61+ GColumnsADT _Columns (M1 D _ rep) =

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

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

58−type GADTColumns'

65+type GColumnsADT'

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

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

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

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

61−type family GADTColumns' _Columns htable rep where

68+type family GColumnsADT' _Columns htable rep where

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

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

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

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

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

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

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

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

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

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

69−type GADTTable

76+type GTableADT

70 :: (Type -> Exp Constraint)

77 :: (Type -> Exp Constraint)

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

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

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

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

73−class GADTTable _Table _Columns rep where

80+class GTableADT _Table _Columns context rep where

74− fromGADTColumns :: ()

81+ gfromColumnsADT :: ()

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

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

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

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

76− -> GADTColumns _Columns rep (Col Result)

85+ -> GColumnsADT _Columns rep context

77 -> rep x

86 -> rep x

79− toGADTColumns :: ()

88+ gtoColumnsADT :: ()

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

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

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

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

81 -> rep x

92 -> 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

102

103

85instance

104instance

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

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

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

107+ , Eval (_Table (htable context))

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

87− , GADTTable' _Table _Columns htable rep

109+ , GTableADT' _Table _Columns htable context rep

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

88 )

111 )

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

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

90 where

113 where

91− fromGADTColumns fromColumns columns =

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 =

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

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

93 Just rep -> M1 rep

217 Just rep -> M1 rep

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

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

95 where

219 where

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

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

221

98− toGADTColumns toColumns (M1 rep) =

222+ gtoResultADT toResult (M1 rep) =

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

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

100 where

224 where

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

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

102

226

103

227

104−type GADTTable'

228+type GToExprsADT'

105− :: (Type -> Exp Constraint)

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

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

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

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

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

108−class GADTTable' _Table _Columns htable rep where

232+class GToExprsADT' _ToExprs _Columns htable exprs rep where

109− fromGADTColumns' :: ()

233+ gfromResultADT' :: ()

234+ => (forall expr a proxy.

235+ ( Eval (_ToExprs expr a)

236+ , HTable (Eval (_Columns expr))

237+ )

238+ => proxy expr

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

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

240+ -> a)

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

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

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

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

113 -> Maybe (rep x)

243 -> Maybe (rep x)

114

244

115− toGADTColumns' :: ()

245+ gtoResultADT' :: ()

246+ => (forall expr a proxy.

247+ ( Eval (_ToExprs expr a)

248+ , HTable (Eval (_Columns expr))

249+ )

250+ => proxy expr

251+ -> a

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

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

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

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

118 -> Maybe (rep x)

254 -> Maybe (rep x)

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

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

120

256

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

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

122

258

123

259

124instance

260instance

125− ( htable' ~ GADTColumns' _Columns htable a

261+ ( htable' ~ GColumnsADT' _Columns htable a

126− , GADTTable' _Table _Columns htable a

262+ , GToExprsADT' _ToExprs _Columns htable a rep1

127− , GADTTable' _Table _Columns htable' b

263+ , GToExprsADT' _ToExprs _Columns htable' b rep2

128 )

264 )

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

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

130 where

266 where

131− fromGADTColumns' fromColumns f columns =

267+ gfromResultADT' fromResult f columns =

132 case ma of

268 case ma of

133 Just a -> Just (L1 a)

269 Just a -> Just (L1 a)

134 Nothing -> R1 <$>

270 Nothing -> R1 <$>

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

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

136− fromColumns

272+ fromResult

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

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

138 columns

274 columns

139 where

275 where

140 ma =

276 ma =

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

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

142− fromColumns

278+ fromResult

143 f

279 f

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

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

145

281

146− toGADTColumns' toColumns tag = \case

282+ gtoResultADT' toResult tag = \case

147 Just (L1 a) ->

283 Just (L1 a) ->

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

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

149− toColumns

285+ toResult

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

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

151− toColumns

287+ toResult

152 tag

288 tag

153 (Just a))

289 (Just a))

154 Nothing

290 Nothing

155 Just (R1 b) ->

291 Just (R1 b) ->

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

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

157− toColumns

293+ toResult

158 (\tag' ->

294 (\tag' ->

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

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

160− toColumns

296+ toResult

161 (\_ -> tag tag')

297 (\_ -> tag tag')

162 Nothing)

298 Nothing)

163 (Just b)

299 (Just b)

164 Nothing ->

300 Nothing ->

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

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

166− toColumns

302+ toResult

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

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

168 Nothing

304 Nothing

169

305

306+ extract =

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

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

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

171

309

172

310

311+instance

312+ ( meta ~ 'MetaCons label _fixity _isRecord

173−instance KnownSymbol label =>

313+ , KnownSymbol label

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

314+ )

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

175 where

316 where

176− fromGADTColumns' _ tag columns

317+ gfromResultADT' _ tag columns

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

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

178 | otherwise = Nothing

319 | otherwise = Nothing

179 where

320 where

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

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

181

322

182− toGADTColumns' _ tag _ = tag tag'

323+ gtoResultADT' _ tag _ = tag tag'

183 where

324 where

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

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

185

326

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

187

328

188

329

189instance {-# OVERLAPPABLE #-}

330instance {-# OVERLAPPABLE #-}

190− ( HTable (GColumns _Columns rep)

331+ ( HTable (GColumns _Columns exprs)

191− , GTable _Table _Columns (Col Result) rep

332+ , GToExprs _ToExprs _Columns exprs rep

333+ , meta ~ 'MetaCons label _fixity _isRecord

192 , KnownSymbol label

334 , KnownSymbol label

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

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

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

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

195 )

337 )

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)

197 where

339 where

198− fromGADTColumns' fromColumns tag (HProduct a b)

340+ gfromResultADT' fromResult tag (HProduct a b)

199 | tag a == tag' =

341 | tag a == tag' =

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

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

201 hunnullify unnullifier (hunlabel unlabeler b)

343 hunnullify unnullifier (hunlabel unlabeler b)

202 | otherwise = Nothing

344 | otherwise = Nothing

203 where

345 where

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

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

205

347

206− toGADTColumns' toColumns tag = \case

348+ gtoResultADT' toResult tag = \case

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

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

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

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

209 hlabel labeler $

351 hlabel labeler $

210 hnullify nullifier $

352 hnullify nullifier $

211− toGColumns @_Table @_Columns toColumns rep

353+ gtoResult @_ToExprs @_Columns @exprs toResult rep

212 where

354 where

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

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

214

356

215 extract (HProduct a _) = a

357 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(..) )

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

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

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

43−import Rel8.Schema.Spec.ConstrainDBType

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

44− ( ConstrainDBType

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

45− , dbTypeDict, dbTypeNullity, fromNullityDict

46− )

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

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

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

181

179

182 hencodeTag _ = Dict

180 hencodeTag _ = Dict

183 hdecodeTag = mempty

181 hdecodeTag = mempty

184−

182+ hnullifier _ _ = ConstrainDBType.nullifier

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

183+ hunnullifier = ConstrainDBType.unnullifier

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

195

184

196

185

197type DefaultConstrainTag :: Type -> Constraint

186type 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 @@

2{-# language DataKinds #-}

3{-# language FlexibleInstances #-}

4{-# language MultiParamTypeClasses #-}

5+{-# language NamedFieldPuns #-}

5{-# language QuantifiedConstraints #-}

6{-# language QuantifiedConstraints #-}

6{-# language StandaloneKindSignatures #-}

7{-# language StandaloneKindSignatures #-}

7{-# language TypeFamilies #-}

8{-# language TypeFamilies #-}

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

10module Rel8.Schema.Spec.ConstrainDBType

11module Rel8.Schema.Spec.ConstrainDBType

11 ( ConstrainDBType

12 ( ConstrainDBType

12− , dbTypeNullity

13+ , dbTypeNullity, dbTypeDict

13− , dbTypeDict

14+ , nullifier, unnullifier

14− , fromNullityDict

15 )

16where

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

22-- rel8

23import Rel8.Schema.Dict ( Dict( Dict ) )

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

24+import Rel8.Schema.Null

25+ ( Nullify, Unnullify

26+ , Nullity( Null, NotNull )

27+ , Sql, nullable

28+ )

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

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

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

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

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

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

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

63fromNullityDict Null Dict = Dict

67fromNullityDict Null Dict = Dict

64fromNullityDict NotNull Dict = Dict

68fromNullityDict 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

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

19 , Congruent

20 , TTable, TColumns, TContext, TUnreify

21− , null, nullifier, unnullifier

22 )

21 )

23where

22where

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

35-- rel8

34-- rel8

36import Rel8.FCF ( Eval, Exp )

35import Rel8.FCF ( Eval, Exp )

36+import Rel8.Kind.Algebra ( KnownAlgebra )

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

38import Rel8.Generic.Table

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

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

40+ , GAlgebra

40 )

41 )

41import Rel8.Generic.Record ( Record(..) )

42import Rel8.Generic.Record ( Record(..) )

43+import Rel8.Generic.Reify ( ARep )

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

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

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

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

46+import Rel8.Schema.Context.Result

47+ ( relabel

48+ , null, nullifier, unnullifier

49+ , vectorizer, unvectorizer

50+ )

44import Rel8.Schema.HTable ( HTable )

51import Rel8.Schema.HTable ( HTable )

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

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

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

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

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

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

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

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

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

55import qualified Rel8.Schema.Kind as K

62import qualified Rel8.Schema.Kind as K

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

63+import Rel8.Schema.Null ( Sql )

57import Rel8.Schema.Reify

64import Rel8.Schema.Reify

58 ( Reify, Col( Reify ), hreify, hunreify

65 ( Reify, Col( Reify ), hreify, hunreify

59 , UnwrapReify

66 , UnwrapReify

60 , notReify

67 , notReify

61 )

68 )

62import Rel8.Schema.Result ( Result )

69import Rel8.Schema.Result ( Result )

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

70+import Rel8.Schema.Spec ( KnownSpec )

64import Rel8.Type ( DBType )

71import Rel8.Type ( DBType )

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

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

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

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

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

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

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

105

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

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

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

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

101 type Unreify a = DefaultUnreify a

108 type Unreify a = DefaultUnreify a

102

109

103 default toColumns ::

110 default toColumns ::

104 ( Generic (Record a)

111 ( Generic (Record a)

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

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

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

106− , Columns a ~ GColumns TColumns (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)))

107 )

116 )

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

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

109 toColumns =

118 toColumns =

119+ ggtoColumns

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

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

121+ @(TTable context)

122+ @TColumns

123+ @TContext

124+ id

125+ id

126+ toColumns .

111 from .

127 from .

112 Record

128 Record

113

129

114 default fromColumns ::

130 default fromColumns ::

115 ( Generic (Record a)

131 ( Generic (Record a)

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

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

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

117− , Columns a ~ GColumns TColumns (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)))

118 )

136 )

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

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

120 fromColumns =

138 fromColumns =

121 unrecord .

139 unrecord .

122 to .

140 to .

141+ ggfromColumns

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

123− fromGColumns @(TTable context) @TColumns fromColumns

143+ @(TTable context)

144+ @TColumns

145+ @TContext

146+ id

147+ id

148+ fromColumns

124

149

125 default reify ::

150 default reify ::

126 ( Generic (Record a)

151 ( Generic (Record a)

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

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

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

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

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

182 DefaultUnreify (t a) = t (Unreify a)

207 DefaultUnreify (t a) = t (Unreify a)

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

183

209

184

210

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

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

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

242 where

268 where

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

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

244

270

245− reify = notReify

246− unreify = notReify

247−

248

271

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

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

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

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

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

253 toColumns = hvectorize vectorizer . fmap toColumns

276 toColumns = hvectorize vectorizer . fmap toColumns

254 fromColumns = fmap fromColumns . hunvectorize unvectorizer

277 fromColumns = fmap fromColumns . hunvectorize unvectorizer

255

278

256− reify = notReify

257− unreify = notReify

258−

259

279

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

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

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

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

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

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

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

278 Just just -> fromColumns just

298 Just just -> fromColumns just

279

299

280− reify = notReify

281− unreify = notReify

282−

283

300

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

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

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

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

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

288 toColumns = hvectorize vectorizer . fmap toColumns

305 toColumns = hvectorize vectorizer . fmap toColumns

289 fromColumns = fmap fromColumns . hunvectorize unvectorizer

306 fromColumns = fmap fromColumns . hunvectorize unvectorizer

290

307

291− reify = notReify

292− unreify = notReify

293−

294

308

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

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

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

310 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

328 , hjust = hlabel labeler (hunlabel unlabeler hthere)

342 , hjust = hlabel labeler (hunlabel unlabeler hthere)

329 }

343 }

330

344

331− reify = notReify

332− unreify = notReify

333−

334

345

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

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

336 => Table context (a, b)

347 => Table context (a, b)

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

377type Congruent :: Type -> Type -> Constraint

388type Congruent :: Type -> Type -> Constraint

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

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

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

390instance 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' )

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

25import Data.Kind ( Constraint, Type )

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

27−import Data.Proxy ( Proxy )

28import GHC.Generics ( Rep )

27import GHC.Generics ( Rep )

29import Prelude

28import Prelude

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

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

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

35import Rel8.FCF ( Eval, Exp )

34import Rel8.FCF ( Eval, Exp )

36import Rel8.Generic.Record ( Record )

35import 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 )

38import Rel8.Schema.Dict ( Dict( Dict ) )

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

39import Rel8.Schema.HTable

42import Rel8.Schema.HTable

40 ( HTable, HConstrainTable

43 ( HTable, HConstrainTable

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

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

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

44import Rel8.Schema.Kind ( Context )

47import Rel8.Schema.Kind ( Context )

45import Rel8.Schema.Null ( Sql )

48import Rel8.Schema.Null ( Sql )

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

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

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

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

48import Rel8.Type.Eq ( DBEq )

51import Rel8.Type.Eq ( DBEq )

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

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

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

58 default eqTable ::

61 default eqTable ::

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

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

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

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

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

61 )

65 )

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

66 => 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

64 where

75 where

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

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

68data TEqTable :: Type -> Exp Constraint

79data TEqTable :: Type -> Exp Constraint

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

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

21-- base

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

23import Data.Kind ( Constraint, Type )

24−import Data.Proxy ( Proxy )

25import GHC.Generics ( Rep )

24import GHC.Generics ( Rep )

26import Prelude hiding ( seq )

25import Prelude hiding ( seq )

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

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

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

33import Rel8.FCF ( Eval, Exp )

32import Rel8.FCF ( Eval, Exp )

34import Rel8.Generic.Record ( Record )

33import 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 )

36import Rel8.Schema.Dict ( Dict( Dict ) )

39import Rel8.Schema.Dict ( Dict( Dict ) )

37import Rel8.Schema.HTable

40import Rel8.Schema.HTable

38 ( HTable, HConstrainTable

41 ( HTable, HConstrainTable

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

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

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

42import Rel8.Schema.Kind ( Context )

45import Rel8.Schema.Kind ( Context )

43import Rel8.Schema.Null (Sql)

46import Rel8.Schema.Null (Sql)

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

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

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

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

46import Rel8.Table.Bool ( bool )

49import Rel8.Table.Bool ( bool )

47import Rel8.Table.Eq ( EqTable )

50import Rel8.Table.Eq ( EqTable )

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

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

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

59 default ordTable ::

62 default ordTable ::

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

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

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

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

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

62 )

66 )

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

67 => 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

65 where

76 where

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

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

69data TOrdTable :: Type -> Exp Constraint

80data TOrdTable :: Type -> Exp Constraint

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

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

25import Data.Bifunctor ( bimap )

26import Data.Kind ( Constraint, Type )

27import Data.List.NonEmpty ( NonEmpty )

28−import GHC.Generics

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

29− ( Generic, Rep, from, to

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

31− )

32−import GHC.TypeLits ( KnownSymbol )

33import Prelude

29import Prelude

35-- hasql

31-- hasql

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

38-- rel8

34-- rel8

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

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

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

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

37+import Rel8.FCF ( Eval, Exp )

41import Rel8.Generic.Record ( Record(..) )

38import 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 )

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

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

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

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

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

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

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

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

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

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

50import Rel8.Schema.Result ( Result )

48import Rel8.Schema.Result ( Result )

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

73 default fromResult ::

71 default fromResult ::

74 ( Generic (Record a)

72 ( Generic (Record a)

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

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

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

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

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

77 )

76 )

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

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

78+ fromResult =

79+ unrecord .

80+ to .

81+ ggfromResult

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

83+ @TToExprs

84+ @TColumns

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

85+ @(Rep (Record exprs))

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

81 default toResult ::

88 default toResult ::

82 ( Generic (Record a)

89 ( Generic (Record a)

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

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

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

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

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

85 )

93 )

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

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

95+ toResult =

96+ ggtoResult

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

98+ @TToExprs

99+ @TColumns

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

100+ @(Rep (Record exprs))

88−

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

89−

102+ from .

103+ Record

104+

105+

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

106+data TToExprs :: Type -> Type -> Exp 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

107+type instance Eval (TToExprs exprs a) = 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)

125

108

126

109

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

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