4017859 · rel8 · git.iko.soy

git.iko.soy/rel8

on master help sign in

Add build{ADT,HKD} alternative to church encoded construct{ADT,HKD}

4017859Shane O'Brien5 years ago

src/Rel8.hs+2

compare with master

unifiedsplit

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

110

111 -- ** @ADT@

112 , ADT, ADTable, fromADT, toADT

113+ , BuildADT, buildADT

113 , ConstructADT, constructADT

114 , ConstructADT, constructADT

114 , DeconstructADT, deconstructADT

115 , DeconstructADT, deconstructADT

115 , InsertADT, insertADT

116 , InsertADT, insertADT

@@ -118,6 +119,7 @@ module Rel8

118

119

119 -- ** @HKD@

120 -- ** @HKD@

120 , HKD, HKDable, fromHKD, toHKD

121 , HKD, HKDable, fromHKD, toHKD

122+ , BuildHKD, buildHKD

121 , ConstructHKD, constructHKD

123 , ConstructHKD, constructHKD

122 , DeconstructHKD, deconstructHKD

124 , DeconstructHKD, deconstructHKD

123 , InsertHKD, insertHKD

125 , InsertHKD, insertHKD

src/Rel8/Generic/Construction.hs+131−52

@@ -14,10 +14,12 @@

14{-# language ViewPatterns #-}

16module Rel8.Generic.Construction

17+ ( GGBuildable

18+ , GGBuild, ggbuild

19+ , GGInsert, gginsert

17− ( GGConstructable

20+ , GGConstructable

18 , GGConstruct, ggconstruct

21 , GGConstruct, ggconstruct

19 , GGDeconstruct, ggdeconstruct

22 , GGDeconstruct, ggdeconstruct

20− , GGInsert, gginsert

21 , GGName, ggname

23 , GGName, ggname

22 , GGAggregate, ggaggregate

24 , GGAggregate, ggaggregate

23 , GGAggregate', ggaggregate'

25 , GGAggregate', ggaggregate'

@@ -29,6 +31,7 @@ import Data.Bifunctor ( first )

29import Data.Kind ( Constraint, Type )

31import Data.Kind ( Constraint, Type )

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

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

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

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

34+import GHC.TypeLits ( Symbol )

32import Prelude

35import Prelude

34-- rel8

37-- rel8

@@ -40,14 +43,16 @@ import Rel8.Expr.Null ( nullify, snull, unsafeUnnullify )

40import Rel8.Expr.Serialize ( litExpr )

43import Rel8.Expr.Serialize ( litExpr )

41import Rel8.FCF ( Compose, Eval, Exp )

44import Rel8.FCF ( Compose, Eval, Exp )

42import Rel8.Generic.Construction.ADT

45import Rel8.Generic.Construction.ADT

46+ ( GConstructorADT, GMakeableADT, gmakeADT

43− ( GConstructableADT

47+ , GConstructableADT

44 , GBuildADT, gbuildADT, gunbuildADT

48 , GBuildADT, gbuildADT, gunbuildADT

45 , GConstructADT, gconstructADT, gdeconstructADT

49 , GConstructADT, gconstructADT, gdeconstructADT

46 , CorepConstructors, GConstructors, gcindex, gctabulate

50 , CorepConstructors, GConstructors, gcindex, gctabulate

47 , CorepFields, gfindex, gftabulate, gftraverse

51 , CorepFields, gfindex, gftabulate, gftraverse

48 )

52 )

49import Rel8.Generic.Construction.Record

53import Rel8.Generic.Construction.Record

54+ ( GConstructor

50− ( GConstructable, GConstruct, gconstruct, gdeconstruct

55+ , GConstructable, GConstruct, gconstruct, gdeconstruct

51 , Corep, gindex, gtabulate, gtraverse

56 , Corep, gindex, gtabulate, gtraverse

52 )

57 )

53import Rel8.Generic.Table ( GGColumns )

58import Rel8.Generic.Table ( GGColumns )

@@ -78,6 +83,124 @@ import Rel8.Type.Tag ( Tag )

78import Data.Functor.Apply ( Apply, MaybeApply( MaybeApply ), liftF2 )

83import Data.Functor.Apply ( Apply, MaybeApply( MaybeApply ), liftF2 )

86+type GGBuildable :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Constraint

87+type GGBuildable algebra name rep =

88+ ( KnownAlgebra algebra

89+ , Eval (GGColumns algebra TColumns (Eval (rep (Reify Aggregate)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))

90+ , Eval (GGColumns algebra TColumns (Eval (rep (Reify Expr)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))

91+ , Eval (GGColumns algebra TColumns (Eval (rep (Reify Insert)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))

92+ , Eval (GGColumns algebra TColumns (Eval (rep (Reify Name)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))

93+ , HTable (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))))

94+ , GGBuildable' algebra name rep

95+ )

96+

97+

98+type GGBuildable' :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Constraint

99+type family GGBuildable' algebra name rep where

100+ GGBuildable' 'K.Product name rep =

101+ ( name ~ GConstructor (Eval (rep (Reify Expr)))

102+ , name ~ GConstructor (Eval (rep (Reify Insert)))

103+ , Corep TUnreify (Eval (rep (Reify Expr)))

104+ , Corep TUnreify (Eval (rep (Reify Insert)))

105+ , GConstructable (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (Eval (rep (Reify Expr)))

106+ , GConstructable (TTable (Reify Insert)) TColumns TUnreify (Col (Reify Insert)) (Eval (rep (Reify Insert)))

107+ )

108+ GGBuildable' 'K.Sum name rep =

109+ ( Corep TUnreify (GConstructorADT name (Eval (rep (Reify Expr))))

110+ , Corep TUnreify (GConstructorADT name (Eval (rep (Reify Insert))))

111+ , GMakeableADT (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) name (Eval (rep (Reify Expr)))

112+ , GMakeableADT (TTable (Reify Insert)) TColumns TUnreify (Col (Reify Insert)) name (Eval (rep (Reify Insert)))

113+ )

114+

115+

116+type GGBuild :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Type -> Type

117+type family GGBuild algebra name rep r where

118+ GGBuild 'K.Product _name rep r =

119+ GConstruct TUnreify (Eval (rep (Reify Expr))) r

120+ GGBuild 'K.Sum name rep r =

121+ GConstruct TUnreify (GConstructorADT name (Eval (rep (Reify Expr)))) r

122+

123+

124+ggbuild :: forall algebra name rep a. GGBuildable algebra name rep

125+ => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr) -> a)

126+ -> GGBuild algebra name rep a

127+ggbuild gfromColumns = case algebraSing @algebra of

128+ SProduct ->

129+ gtabulate @TUnreify @(Eval (rep (Reify Expr))) @a $

130+ gfromColumns .

131+ hunreify .

132+ gconstruct

133+ @(TTable (Reify Expr))

134+ @TColumns

135+ @TUnreify

136+ @(Col (Reify Expr))

137+ @(Eval (rep (Reify Expr)))

138+ (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)

139+ SSum ->

140+ gtabulate @TUnreify @(GConstructorADT name (Eval (rep (Reify Expr)))) @a $

141+ gfromColumns .

142+ hunreify .

143+ gmakeADT

144+ @(TTable (Reify Expr))

145+ @TColumns

146+ @TUnreify

147+ @(Col (Reify Expr))

148+ @name

149+ @(Eval (rep (Reify Expr)))

150+ (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)

151+ (\SSpec {info} -> Reify (DB (snull info)))

152+ (\SSpec {nullity} -> case nullity of

153+ Null -> id

154+ NotNull -> \(Reify (DB a)) -> Reify (DB (nullify a)))

155+ (HType . Reify . DB . litExpr)

156+

157+

158+type GGInsert :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Type -> Type

159+type family GGInsert algebra name rep r where

160+ GGInsert 'K.Product _name rep r =

161+ GConstruct TUnreify (Eval (rep (Reify Insert))) r

162+ GGInsert 'K.Sum name rep r =

163+ GConstruct TUnreify (GConstructorADT name (Eval (rep (Reify Insert)))) r

164+

165+

166+gginsert :: forall algebra name rep a. GGBuildable algebra name rep

167+ => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Insert) -> a)

168+ -> GGInsert algebra name rep a

169+gginsert gfromColumns = case algebraSing @algebra of

170+ SProduct ->

171+ gtabulate @TUnreify @(Eval (rep (Reify Insert))) @a $

172+ gfromColumns .

173+ hunreify .

174+ gconstruct

175+ @(TTable (Reify Insert))

176+ @TColumns

177+ @TUnreify

178+ @(Col (Reify Insert))

179+ @(Eval (rep (Reify Insert)))

180+ (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)

181+ SSum ->

182+ gtabulate @TUnreify @(GConstructorADT name (Eval (rep (Reify Insert)))) @a $

183+ gfromColumns .

184+ hunreify .

185+ gmakeADT

186+ @(TTable (Reify Insert))

187+ @TColumns

188+ @TUnreify

189+ @(Col (Reify Insert))

190+ @name

191+ @(Eval (rep (Reify Insert)))

192+ (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)

193+ (\SSpec {necessity, info} -> Reify $ case necessity of

194+ SRequired -> RequiredInsert (snull info)

195+ SOptional -> OptionalInsert (Just (snull info)))

196+ (\SSpec {nullity} -> case nullity of

197+ Null -> id

198+ NotNull -> \case

199+ Reify (RequiredInsert a) -> Reify (RequiredInsert (nullify a))

200+ Reify (OptionalInsert a) -> Reify (OptionalInsert (nullify <$> a)))

201+ (HType . Reify . RequiredInsert . litExpr)

202+

203+

81type GGConstructable :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint

204type GGConstructable :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint

82type GGConstructable algebra rep =

205type GGConstructable algebra rep =

83 ( KnownAlgebra algebra

206 ( KnownAlgebra algebra

@@ -121,8 +244,10 @@ type family GGConstructable' algebra rep where

121

244

122type GGConstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type

245type GGConstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type

123type family GGConstruct algebra rep r where

246type family GGConstruct algebra rep r where

247+ GGConstruct 'K.Product rep r =

124− GGConstruct 'K.Product rep r = GConstruct TUnreify (Eval (rep (Reify Expr))) r -> r

248+ GConstruct TUnreify (Eval (rep (Reify Expr))) r -> r

249+ GGConstruct 'K.Sum rep r =

125− GGConstruct 'K.Sum rep r = GConstructADT TUnreify (Eval (rep (Reify Expr))) r r

250+ GConstructADT TUnreify (Eval (rep (Reify Expr))) r r

126

251

127

252

128ggconstruct :: forall algebra rep a. GGConstructable algebra rep

253ggconstruct :: forall algebra rep a. GGConstructable algebra rep

@@ -204,52 +329,6 @@ ggdeconstruct gtoColumns = case algebraSing @algebra of

204 case_ cases' r

329 case_ cases' r

205

330

206

331

207−type GGInsert :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type

208−type family GGInsert algebra rep r where

209− GGInsert 'K.Product rep r =

210− GConstruct TUnreify (Eval (rep (Reify Insert))) r -> r

211− GGInsert 'K.Sum rep r =

212− GConstructADT TUnreify (Eval (rep (Reify Insert))) r r

213−

214−

215−gginsert :: forall algebra rep a. GGConstructable algebra rep

216− => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Insert) -> a)

217− -> GGInsert algebra rep a

218− -> a

219−gginsert gfromColumns f = case algebraSing @algebra of

220− SProduct ->

221− f $

222− gtabulate @TUnreify @(Eval (rep (Reify Insert))) @a $

223− gfromColumns .

224− hunreify .

225− gconstruct

226− @(TTable (Reify Insert))

227− @TColumns

228− @TUnreify

229− @(Col (Reify Insert))

230− @(Eval (rep (Reify Insert)))

231− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)

232− SSum ->

233− gcindex @TUnreify @(Eval (rep (Reify Insert))) @a f $

234− fmap (gfromColumns . hunreify) $

235− gconstructADT

236− @(TTable (Reify Insert))

237− @TColumns

238− @TUnreify

239− @(Col (Reify Insert))

240− @(Eval (rep (Reify Insert)))

241− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)

242− (\SSpec {necessity, info} -> Reify $ case necessity of

243− SRequired -> RequiredInsert (snull info)

244− SOptional -> OptionalInsert (Just (snull info)))

245− (\SSpec {nullity} -> case nullity of

246− Null -> id

247− NotNull -> \case

248− Reify (RequiredInsert a) -> Reify (RequiredInsert (nullify a))

249− Reify (OptionalInsert a) -> Reify (OptionalInsert (nullify <$> a)))

250− (HType . Reify . RequiredInsert . litExpr)

251−

252−

253type GGName :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type

332type GGName :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type

254type family GGName algebra rep a where

333type family GGName algebra rep a where

255 GGName 'K.Product rep a = GConstruct TUnreify (Eval (rep (Reify Name))) a

334 GGName 'K.Product rep a = GConstruct TUnreify (Eval (rep (Reify Name))) a

src/Rel8/Generic/Construction/ADT.hs+143−2

@@ -18,6 +18,7 @@ module Rel8.Generic.Construction.ADT

18 , GConstructADT, gconstructADT, gdeconstructADT

19 , GFields, CorepFields, gftabulate, gfindex, gftraverse

20 , GConstructors, CorepConstructors, gctabulate, gcindex

21+ , GConstructorADT, GMakeableADT, gmakeADT

21 )

22 )

22where

23where

@@ -31,9 +32,12 @@ import Data.Proxy ( Proxy( Proxy ) )

31import GHC.Generics

32import GHC.Generics

32 ( (:+:), (:*:)( (:*:) ), M1, U1

33 ( (:+:), (:*:)( (:*:) ), M1, U1

33 , C, D

34 , C, D

34− , Meta( MetaCons )

35+ , Meta( MetaData, MetaCons )

36+ )

37+import GHC.TypeLits

38+ ( ErrorMessage( (:<>:), Text ), TypeError

39+ , Symbol, KnownSymbol, symbolVal

35 )

40 )

36−import GHC.TypeLits ( KnownSymbol, symbolVal )

37import Prelude hiding ( null )

41import Prelude hiding ( null )

39-- rel8

43-- rel8

@@ -80,6 +84,32 @@ type Unnullifier context = forall labels necessity a. ()

80 -> context ('Spec labels necessity a)

84 -> context ('Spec labels necessity a)

87+type NoConstructor :: Symbol -> Symbol -> ErrorMessage

88+type NoConstructor datatype constructor =

89+ ( 'Text "The type `" ':<>:

90+ 'Text datatype ':<>:

91+ 'Text "` has no constructor `" ':<>:

92+ 'Text constructor ':<>:

93+ 'Text "`."

94+ )

95+

96+

97+type GConstructorADT :: Symbol -> (Type -> Type) -> Type -> Type

98+type family GConstructorADT name rep where

99+ GConstructorADT name (M1 D ('MetaData datatype _ _ _) rep) =

100+ GConstructorADT' name rep (TypeError (NoConstructor datatype name))

101+

102+

103+type GConstructorADT' :: Symbol -> (Type -> Type) -> (Type -> Type) -> Type -> Type

104+type family GConstructorADT' name rep fallback where

105+ GConstructorADT' name (M1 D _ rep) fallback =

106+ GConstructorADT' name rep fallback

107+ GConstructorADT' name (a :+: b) fallback =

108+ GConstructorADT' name a (GConstructorADT' name b fallback)

109+ GConstructorADT' name (M1 C ('MetaCons name _ _) rep) _ = rep

110+ GConstructorADT' _ _ fallback = fallback

111+

112+

83type GConstructADT

113type GConstructADT

84 :: (Type -> Exp Type)

114 :: (Type -> Exp Type)

85 -> (Type -> Type) -> Type -> Type -> Type

115 -> (Type -> Type) -> Type -> Type -> Type

@@ -357,3 +387,114 @@ instance {-# OVERLAPPABLE #-}

357 tag = Tag $ pack $ symbolVal (Proxy @label)

387 tag = Tag $ pack $ symbolVal (Proxy @label)

358

388

359 gfill null htable = HProduct htable (hlabel hlabeler (hnulls null))

389 gfill null htable = HProduct htable (hlabel hlabeler (hnulls null))

390+

391+

392+type GMakeableADT

393+ :: (Type -> Exp Constraint)

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

395+ -> (Type -> Exp Type)

396+ -> K.HContext -> Symbol -> (Type -> Type) -> Constraint

397+class GMakeableADT _Table _Columns f context name rep where

398+ gmakeADT :: ()

399+ => ToColumns _Table _Columns f context

400+ -> Null context

401+ -> Nullifier context

402+ -> (Tag -> HType Tag context)

403+ -> GFields f (GConstructorADT name rep)

404+ -> GColumnsADT _Columns rep context

405+

406+

407+instance

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

409+ , meta ~ 'MetaData datatype _module _package _newtype

410+ , fallback ~ TypeError (NoConstructor datatype name)

411+ , fields ~ GFields f (GConstructorADT' name rep fallback)

412+ , GMakeableADT' _Table _Columns f context htable name rep fields

413+ , HLabelable context

414+ , KnownSymbol name

415+ )

416+ => GMakeableADT _Table _Columns f context name (M1 D meta rep)

417+ where

418+ gmakeADT toColumns null nullifier wrap =

419+ gmakeADT'

420+ @_Table @_Columns @f @context @htable @name @rep @fields

421+ toColumns null nullifier htable

422+ where

423+ tag = Tag $ pack $ symbolVal (Proxy @name)

424+ htable = hlabel hlabeler (wrap tag)

425+

426+

427+type GMakeableADT'

428+ :: (Type -> Exp Constraint)

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

430+ -> (Type -> Exp Type)

431+ -> K.HContext -> K.HTable -> Symbol -> (Type -> Type) -> Type -> Constraint

432+class GMakeableADT' _Table _Columns f context htable name rep fields where

433+ gmakeADT' :: ()

434+ => ToColumns _Table _Columns f context

435+ -> Null context

436+ -> Nullifier context

437+ -> htable context

438+ -> fields

439+ -> GColumnsADT' _Columns htable rep context

440+

441+

442+instance

443+ ( htable' ~ GColumnsADT' _Columns htable a

444+ , GMakeableADT' _Table _Columns f context htable name a fields

445+ , GMakeableADT' _Table _Columns f context htable' name b fields

446+ )

447+ => GMakeableADT' _Table _Columns f context htable name (a :+: b) fields

448+ where

449+ gmakeADT' toColumns null nullifier htable x =

450+ gmakeADT' @_Table @_Columns @f @context @htable' @name @b @fields

451+ toColumns null nullifier

452+ (gmakeADT'

453+ @_Table @_Columns @f @context @htable @name @a @fields toColumns

454+ null nullifier htable x)

455+ x

456+

457+

458+instance {-# OVERLAPPING #-}

459+ GMakeableADT' _Table _Columns f context htable name (M1 C ('MetaCons name _fixity _isRecord) U1) fields

460+ where

461+ gmakeADT' _ _ _ = const

462+

463+

464+instance {-# OVERLAPS #-}

465+ GMakeableADT' _Table _Columns f context htable name (M1 C ('MetaCons label _fixity _isRecord) U1) fields

466+ where

467+ gmakeADT' _ _ _ = const

468+

469+

470+instance {-# OVERLAPS #-}

471+ ( HTable (GColumns _Columns rep)

472+ , KnownSymbol name

473+ , HLabelable context

474+ , GConstructable _Table _Columns f context rep

475+ , fields ~ GFields f rep

476+ , GColumnsADT' _Columns htable (M1 C ('MetaCons name _fixity _isRecord) rep) ~

477+ HProduct htable (HLabel name (HNullify (GColumns _Columns rep)))

478+ )

479+ => GMakeableADT' _Table _Columns f context htable name (M1 C ('MetaCons name _fixity _isRecord) rep) fields

480+ where

481+ gmakeADT' toColumns _ nullifier htable =

482+ HProduct htable .

483+ hlabel hlabeler .

484+ hnullify nullifier .

485+ gconstruct @_Table @_Columns @f @context @rep toColumns

486+

487+

488+instance {-# OVERLAPPABLE #-}

489+ ( HTable (GColumns _Columns rep)

490+ , KnownSymbol label

491+ , HLabelable context

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

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

494+ )

495+ => GMakeableADT' _Table _Columns f context htable name (M1 C ('MetaCons label _fixity _isRecord) rep) fields

496+ where

497+ gmakeADT' _ null _ htable _ =

498+ HProduct htable $

499+ hlabel hlabeler $

500+ hnulls null

src/Rel8/Generic/Construction/Record.hs+16−3

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

12{-# language UndecidableInstances #-}

14module Rel8.Generic.Construction.Record

15− ( GConstruct, GConstructable, gconstruct, gdeconstruct

15+ ( GConstructor, GConstruct, GConstructable, gconstruct, gdeconstruct

16 , GFields, Corep, gtabulate, gindex, gtraverse

17 , FromColumns, ToColumns

18 )

@@ -24,9 +24,12 @@ import Data.Kind ( Constraint, Type )

24import Data.Proxy ( Proxy( Proxy ) )

25import GHC.Generics

26 ( (:*:), K1, M1, U1

27− , D, C, S, Meta( MetaSel )

27+ , D, C, S, Meta( MetaData, MetaCons, MetaSel )

28+ )

29+import GHC.TypeLits

30+ ( ErrorMessage( (:<>:), Text ), TypeError

31+ , Symbol, KnownSymbol

28 )

32 )

29−import GHC.TypeLits ( KnownSymbol )

30import Prelude

33import Prelude

32-- rel8

35-- rel8

@@ -59,6 +62,16 @@ type ToColumns _Table _Columns f context = forall proxy x.

59 Eval (_Table x) => proxy x -> Eval (f x) -> Eval (_Columns x) context

62 Eval (_Table x) => proxy x -> Eval (f x) -> Eval (_Columns x) context

65+type GConstructor :: (Type -> Type) -> Symbol

66+type family GConstructor rep where

67+ GConstructor (M1 D _ (M1 C ('MetaCons name _ _) _)) = name

68+ GConstructor (M1 D ('MetaData name _ _ _) _) = TypeError (

69+ 'Text "`" ':<>:

70+ 'Text name ':<>:

71+ 'Text "` does not appear to have exactly 1 constructor"

72+ )

73+

74+

62type GConstruct :: (Type -> Exp Type) -> (Type -> Type) -> Type -> Type

75type GConstruct :: (Type -> Exp Type) -> (Type -> Type) -> Type -> Type

63type family GConstruct f rep r where

76type family GConstruct f rep r where

64 GConstruct f (M1 _ _ rep) r = GConstruct f rep r

77 GConstruct f (M1 _ _ rep) r = GConstruct f rep r

src/Rel8/Generic/Rel8able/Test.hs+1−1

@@ -106,7 +106,7 @@ deriving via HKDT S3Object

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

107

108

109−data HKDSum = HKDSumA Text | HKDSumB Bool Char

109+data HKDSum = HKDSumA Text | HKDSumB Bool Char | HKDSumC

110 deriving stock Generic

111

112

src/Rel8/Table/ADT.hs+32−13

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

2{-# language DataKinds #-}

3{-# language FlexibleContexts #-}

4{-# language FlexibleInstances #-}

5+{-# language MultiParamTypeClasses #-}

5{-# language RankNTypes #-}

6{-# language RankNTypes #-}

6{-# language ScopedTypeVariables #-}

7{-# language ScopedTypeVariables #-}

7{-# language StandaloneKindSignatures #-}

8{-# language StandaloneKindSignatures #-}

@@ -13,10 +14,12 @@

13module Rel8.Table.ADT

14module Rel8.Table.ADT

14 ( ADT( ADT )

15 ( ADT( ADT )

15 , ADTable, fromADT, toADT

16 , ADTable, fromADT, toADT

17+ , BuildableADT

18+ , BuildADT, buildADT

19+ , InsertADT, insertADT

16 , ConstructableADT

20 , ConstructableADT

17 , ConstructADT, constructADT

21 , ConstructADT, constructADT

18 , DeconstructADT, deconstructADT

22 , DeconstructADT, deconstructADT

19− , InsertADT, insertADT

20 , NameADT, nameADT

23 , NameADT, nameADT

21 , AggregateADT, aggregateADT

24 , AggregateADT, aggregateADT

22 , ADTRep

25 , ADTRep

@@ -28,6 +31,7 @@ import Data.Kind ( Constraint, Type )

28import Data.Proxy ( Proxy( Proxy ) )

31import Data.Proxy ( Proxy( Proxy ) )

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

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

30import GHC.Generics ( Generic, Rep, from, to )

33import GHC.Generics ( Generic, Rep, from, to )

34+import GHC.TypeLits ( Symbol )

31import Prelude

35import Prelude

33-- rel8

37-- rel8

@@ -35,10 +39,12 @@ import Rel8.Aggregate ( Aggregate )

35import Rel8.Expr ( Expr )

39import Rel8.Expr ( Expr )

36import Rel8.FCF ( Eval, Exp )

40import Rel8.FCF ( Eval, Exp )

37import Rel8.Generic.Construction

41import Rel8.Generic.Construction

42+ ( GGBuildable

43+ , GGBuild, ggbuild

44+ , GGInsert, gginsert

38− ( GGConstructable

45+ , GGConstructable

39 , GGConstruct, ggconstruct

46 , GGConstruct, ggconstruct

40 , GGDeconstruct, ggdeconstruct

47 , GGDeconstruct, ggdeconstruct

41− , GGInsert, gginsert

42 , GGName, ggname

48 , GGName, ggname

43 , GGAggregate, ggaggregate

49 , GGAggregate, ggaggregate

44 )

50 )

@@ -136,6 +142,29 @@ instance

136 => ADTable t

142 => ADTable t

137

143

138

144

145+type BuildableADT :: K.Rel8able -> Symbol -> Constraint

146+class GGBuildable 'K.Sum name (ADTRep t) => BuildableADT t name

147+instance GGBuildable 'K.Sum name (ADTRep t) => BuildableADT t name

148+

149+

150+type BuildADT :: K.Rel8able -> Symbol -> Type

151+type BuildADT t name = GGBuild 'K.Sum name (ADTRep t) (ADT t Expr)

152+

153+

154+buildADT :: forall t name. BuildableADT t name => BuildADT t name

155+buildADT =

156+ ggbuild @'K.Sum @name @(ADTRep t) @(ADT t Expr) ADT

157+

158+

159+type InsertADT :: K.Rel8able -> Symbol -> Type

160+type InsertADT t name = GGInsert 'K.Sum name (ADTRep t) (ADT t Insert)

161+

162+

163+insertADT :: forall t name. BuildableADT t name => InsertADT t name

164+insertADT =

165+ gginsert @'K.Sum @name @(ADTRep t) @(ADT t Insert) ADT

166+

167+

139type ConstructableADT :: K.Rel8able -> Constraint

168type ConstructableADT :: K.Rel8able -> Constraint

140class GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t

169class GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t

141instance GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t

170instance GGConstructable 'K.Sum (ADTRep t) => ConstructableADT t

@@ -161,16 +190,6 @@ deconstructADT =

161 ggdeconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) @r (\(ADT a) -> a)

190 ggdeconstruct @'K.Sum @(ADTRep t) @(ADT t Expr) @r (\(ADT a) -> a)

162

191

163

192

164−type InsertADT :: K.Rel8able -> Type

165−type InsertADT t = forall r. GGInsert 'K.Sum (ADTRep t) r

166−

167−

168−insertADT :: forall t. ConstructableADT t => InsertADT t -> ADT t Insert

169−insertADT f =

170− gginsert @'K.Sum @(ADTRep t) @(ADT t Insert) ADT

171− (f @(ADT t Insert))

172−

173−

174type NameADT :: K.Rel8able -> Type

193type NameADT :: K.Rel8able -> Type

175type NameADT t = GGName 'K.Sum (ADTRep t) (ADT t Name)

194type NameADT t = GGName 'K.Sum (ADTRep t) (ADT t Name)

176

195

src/Rel8/Table/HKD.hs+31−13

@@ -14,10 +14,12 @@

14module Rel8.Table.HKD

15 ( HKD( HKD )

16 , HKDable, fromHKD, toHKD, HKDT(..)

17+ , BuildableHKD

18+ , BuildHKD, buildHKD

19+ , InsertHKD, insertHKD

17 , ConstructableHKD

20 , ConstructableHKD

18 , ConstructHKD, constructHKD

21 , ConstructHKD, constructHKD

19 , DeconstructHKD, deconstructHKD

22 , DeconstructHKD, deconstructHKD

20− , InsertHKD, insertHKD

21 , NameHKD, nameHKD

23 , NameHKD, nameHKD

22 , AggregateHKD, aggregateHKD

24 , AggregateHKD, aggregateHKD

23 , HKDRep

25 , HKDRep

@@ -30,6 +32,7 @@ import Data.Proxy ( Proxy( Proxy ) )

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

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

31import Data.Void ( Void )

33import Data.Void ( Void )

32import GHC.Generics ( Generic, Rep, from, to )

34import GHC.Generics ( Generic, Rep, from, to )

35+import GHC.TypeLits ( Symbol )

33import Prelude

36import Prelude

35-- rel8

38-- rel8

@@ -39,10 +42,12 @@ import Rel8.Expr ( Expr )

39import Rel8.FCF ( Eval, Exp )

42import Rel8.FCF ( Eval, Exp )

40import Rel8.Kind.Algebra ( KnownAlgebra )

43import Rel8.Kind.Algebra ( KnownAlgebra )

41import Rel8.Generic.Construction

44import Rel8.Generic.Construction

45+ ( GGBuildable

46+ , GGBuild, ggbuild

47+ , GGInsert, gginsert

42− ( GGConstructable

48+ , GGConstructable

43 , GGConstruct, ggconstruct

49 , GGConstruct, ggconstruct

44 , GGDeconstruct, ggdeconstruct

50 , GGDeconstruct, ggdeconstruct

45− , GGInsert, gginsert

46 , GGName, ggname

51 , GGName, ggname

47 , GGAggregate, ggaggregate

52 , GGAggregate, ggaggregate

48 )

53 )

@@ -204,6 +209,29 @@ instance

204 => HKDable a

209 => HKDable a

205

210

206

211

212+type BuildableHKD :: Type -> Symbol -> Constraint

213+class GGBuildable (GAlgebra (Rep a)) name (HKDRep a) => BuildableHKD a name

214+instance GGBuildable (GAlgebra (Rep a)) name (HKDRep a) => BuildableHKD a name

215+

216+

217+type BuildHKD :: Type -> Symbol -> Type

218+type BuildHKD a name = GGBuild (GAlgebra (Rep a)) name (HKDRep a) (HKD a Expr)

219+

220+

221+buildHKD :: forall a name. BuildableHKD a name => BuildHKD a name

222+buildHKD =

223+ ggbuild @(GAlgebra (Rep a)) @name @(HKDRep a) @(HKD a Expr) HKD

224+

225+

226+type InsertHKD :: Type -> Symbol -> Type

227+type InsertHKD a name = GGInsert (GAlgebra (Rep a)) name (HKDRep a) (HKD a Insert)

228+

229+

230+insertHKD :: forall a name. BuildableHKD a name => InsertHKD a name

231+insertHKD =

232+ gginsert @(GAlgebra (Rep a)) @name @(HKDRep a) @(HKD a Insert) HKD

233+

234+

207type ConstructableHKD :: Type -> Constraint

235type ConstructableHKD :: Type -> Constraint

208class GGConstructable (GAlgebra (Rep a)) (HKDRep a) => ConstructableHKD a

236class GGConstructable (GAlgebra (Rep a)) (HKDRep a) => ConstructableHKD a

209instance GGConstructable (GAlgebra (Rep a)) (HKDRep a) => ConstructableHKD a

237instance GGConstructable (GAlgebra (Rep a)) (HKDRep a) => ConstructableHKD a

@@ -228,16 +256,6 @@ deconstructHKD :: forall a r. (ConstructableHKD a, Table Expr r)

228deconstructHKD = ggdeconstruct @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Expr) @r (\(HKD a) -> a)

256deconstructHKD = ggdeconstruct @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Expr) @r (\(HKD a) -> a)

229

257

230

258

231−type InsertHKD :: Type -> Type

232−type InsertHKD a = forall r. GGInsert (GAlgebra (Rep a)) (HKDRep a) r

233−

234−

235−insertHKD :: forall a. ConstructableHKD a => InsertHKD a -> HKD a Insert

236−insertHKD f =

237− gginsert @(GAlgebra (Rep a)) @(HKDRep a) @(HKD a Insert) HKD

238− (f @(HKD a Insert))

239−

240−

241type NameHKD :: Type -> Type

259type NameHKD :: Type -> Type

242type NameHKD a = GGName (GAlgebra (Rep a)) (HKDRep a) (HKD a Name)

260type NameHKD a = GGName (GAlgebra (Rep a)) (HKDRep a) (HKD a Name)

243

261