git.iko.soy/rel8
on master help sign in
Move FromExprs into the Table class and get rid of Unreify (#106)
commit7c5422fff541c8952677ebe40731636007b3b304 authorShane <shane.obrien@circuithub.com> dateTue 6 Jul 2021, 12:36 (5 years ago) parent5a47018
47 files changed+866−2988
compare with master
unifiedsplit
rel8.cabal+2−4 src/Rel8.hs+1−5 src/Rel8/Aggregate.hs+5−18 src/Rel8/Column.hs+6−87 src/Rel8/Column/ADT.hs+4−87 src/Rel8/Column/Either.hs+4−165 src/Rel8/Column/Lift.hs+4−85 src/Rel8/Column/List.hs+4−146 src/Rel8/Column/Maybe.hs+3−117 src/Rel8/Column/NonEmpty.hs+4−146 src/Rel8/Column/These.hs+3−165 src/Rel8/Expr.hs+5−14 src/Rel8/Expr/Eq.hs+1−1 src/Rel8/FCF.hs+3−3 src/Rel8/Generic/Coherence.hs−79 src/Rel8/Generic/Construction.hs+136−154 src/Rel8/Generic/Map.hs+3−67 src/Rel8/Generic/Reify.hs−24 src/Rel8/Generic/Rel8able.hs+86−64 src/Rel8/Generic/Table.hs+25−108 src/Rel8/Generic/Table/ADT.hs+61−194 src/Rel8/Generic/Table/Record.hs+55−102 src/Rel8/Kind/Context.hs+1−21 src/Rel8/Schema/Context.hs+6 src/Rel8/Schema/Context/Abstract.hs−80 src/Rel8/Schema/Context/Nullify.hs−15 src/Rel8/Schema/Context/Virtual.hs+70 src/Rel8/Schema/Name.hs+5−14 src/Rel8/Schema/Reify.hs−68 src/Rel8/Schema/Result.hs−19 src/Rel8/Table.hs+82−295 src/Rel8/Table/ADT.hs+33−59 src/Rel8/Table/Either.hs+27−37 src/Rel8/Table/Eq.hs+6−12 src/Rel8/Table/HKD.hs+64−106 src/Rel8/Table/List.hs+11−38 src/Rel8/Table/Maybe.hs+22−25 src/Rel8/Table/NonEmpty.hs+10−37 src/Rel8/Table/Nullify.hs+15−37 src/Rel8/Table/Ord.hs+6−12 src/Rel8/Table/Recontextualize.hs+1−40 src/Rel8/Table/Rel8able.hs+21−71 src/Rel8/Table/Serialize.hs+12−105 src/Rel8/Table/These.hs+45−36 src/Rel8/Type/Composite.hs+10−10 src/Rel8/Type/Tag.hs+1−1 tests/Rel8/Generic/Rel8able/Test.hs+3−15
rel8.cabal+2−4
@@ -39,6 +39,7 @@ library
3939 default-language:
4040 Haskell2010
4141 ghc-options:
42+ -Werror=missing-methods -Werror=incomplete-patterns -Werror=missing-fields
4243 -Weverything -Wno-unsafe -Wno-safe -Wno-missing-safe-haskell-mode
4344 -Wno-missing-import-lists -Wno-prepositive-qualified-module
4445 -Wno-monomorphism-restriction
@@ -82,13 +83,11 @@ library
8283 Rel8.Kind.Algebra
8384 Rel8.Kind.Context
8485
85− Rel8.Generic.Coherence
8686 Rel8.Generic.Construction
8787 Rel8.Generic.Construction.ADT
8888 Rel8.Generic.Construction.Record
8989 Rel8.Generic.Map
9090 Rel8.Generic.Record
91− Rel8.Generic.Reify
9291 Rel8.Generic.Rel8able
9392 Rel8.Generic.Table
9493 Rel8.Generic.Table.ADT
@@ -116,8 +115,8 @@ library
116115 Rel8.Query.Values
117116
118117 Rel8.Schema.Context
119− Rel8.Schema.Context.Abstract
120118 Rel8.Schema.Context.Nullify
119+ Rel8.Schema.Context.Virtual
121120 Rel8.Schema.Dict
122121 Rel8.Schema.HTable
123122 Rel8.Schema.HTable.Either
@@ -134,7 +133,6 @@ library
134133 Rel8.Schema.Kind
135134 Rel8.Schema.Name
136135 Rel8.Schema.Null
137− Rel8.Schema.Reify
138136 Rel8.Schema.Result
139137 Rel8.Schema.Spec
140138 Rel8.Schema.Spec.Constrain
src/Rel8.hs+1−5
@@ -239,8 +239,7 @@ module Rel8
239239
240240 -- * IO
241241 , Serializable
242− , ToExprs(..)
243− , FromExprs
242+ , ToExprs
244243 , Result
245244
246245 -- * Running statements
@@ -272,9 +271,6 @@ module Rel8
272271 -- ** Sequences
273272 , nextval
274273 , evaluate
275−
276− -- * Implementation details
277− , HKDT(..)
278274 ) where
279275
280276-- base
src/Rel8/Aggregate.hs+5−18
@@ -1,5 +1,4 @@
11{-# language DataKinds #-}
2−{-# language DerivingVia #-}
32{-# language FlexibleContexts #-}
43{-# language FlexibleInstances #-}
54{-# language GADTs #-}
@@ -21,7 +20,6 @@ where
2120
2221-- base
2322import Data.Functor.Const ( Const( Const ), getConst )
24−import Data.Functor.Identity ( Identity )
2523import Data.Kind ( Constraint, Type )
2624import Prelude
2725
@@ -36,12 +34,11 @@ import Rel8.Schema.Context ( Interpretation(..) )
3634import Rel8.Schema.HTable.Identity ( HIdentity(..), HType )
3735import Rel8.Schema.Name ( Name )
3836import Rel8.Schema.Null ( Sql )
39−import Rel8.Schema.Reify ( notReify )
40−import Rel8.Schema.Result ( Result )
37+import Rel8.Schema.Result ( Col( R ) )
4138import Rel8.Schema.Spec ( Spec( Spec ) )
4239import Rel8.Table
4340 ( Table, Columns, Context, fromColumns, toColumns
44− , reify, unreify, coherence, congruence
41+ , FromExprs, fromResult, toResult
4542 )
4643import Rel8.Table.Recontextualize ( Recontextualize )
4744import Rel8.Type ( DBType )
@@ -67,14 +64,12 @@ instance Interpretation Aggregate where
6764instance Sql DBType a => Table Aggregate (Aggregate a) where
6865 type Columns (Aggregate a) = HType a
6966 type Context (Aggregate a) = Aggregate
67+ type FromExprs (Aggregate a) = a
7068
7169 toColumns = HIdentity . A
7270 fromColumns (HIdentity (A a)) = a
73−
74− reify = notReify
75− unreify = notReify
76− coherence = notReify
77− congruence = notReify
71+ toResult = HIdentity . R
72+ fromResult (HIdentity (R a)) = a
7873
7974
8075instance Sql DBType a =>
@@ -85,10 +80,6 @@ instance Sql DBType a =>
8580 Recontextualize Aggregate Expr (Aggregate a) (Expr a)
8681
8782
88−instance Sql DBType a =>
89− Recontextualize Aggregate Result (Aggregate a) (Identity a)
90−
91−
9283instance Sql DBType a =>
9384 Recontextualize Aggregate Name (Aggregate a) (Name a)
9485
@@ -97,10 +88,6 @@ instance Sql DBType a =>
9788 Recontextualize Expr Aggregate (Expr a) (Aggregate a)
9889
9990
100−instance Sql DBType a =>
101− Recontextualize Result Aggregate (Identity a) (Aggregate a)
102−
103−
10491instance Sql DBType a =>
10592 Recontextualize Name Aggregate (Name a) (Aggregate a)
10693
src/Rel8/Column.hs+6−87
@@ -1,41 +1,24 @@
11{-# language DataKinds #-}
2−{-# language FlexibleContexts #-}
3−{-# language LambdaCase #-}
4−{-# language MultiParamTypeClasses #-}
5−{-# language ScopedTypeVariables #-}
62{-# language StandaloneKindSignatures #-}
7−{-# language TypeApplications #-}
83{-# language TypeFamilies #-}
94
105module Rel8.Column
11− ( Column, AColumn(..)
6+ ( Column
127 , TColumn
138 )
149where
1510
1611-- base
1712import Data.Kind ( Type )
18−import Data.Type.Equality ( (:~:)( Refl ) )
19−import Prelude
13+import Prelude ()
2014
2115-- rel8
22−import Rel8.Aggregate ( Aggregate, Col( A ) )
23−import Rel8.Expr ( Expr, Col( E ) )
16+import Rel8.Aggregate ( Aggregate )
17+import Rel8.Expr ( Expr )
2418import Rel8.FCF ( Eval, Exp )
25−import Rel8.Kind.Context ( SContext(..), Reifiable( contextSing ) )
26−import Rel8.Schema.HTable.Identity ( HIdentity(..), HType )
2719import qualified Rel8.Schema.Kind as K
28−import Rel8.Schema.Name ( Name(..), Col( N ) )
29−import Rel8.Schema.Null ( Sql )
30−import Rel8.Schema.Reify ( Reify, Col(..) )
31−import Rel8.Schema.Result ( Col( R ), Result, absurd )
32−import Rel8.Schema.Spec ( Spec( Spec ) )
33−import Rel8.Table
34− ( Table, Columns, Context, fromColumns, toColumns
35− , Unreify, reify, unreify, coherence, congruence
36− )
37−import Rel8.Table.Recontextualize ( Recontextualize )
38−import Rel8.Type ( DBType )
20+import Rel8.Schema.Name ( Name(..) )
21+import Rel8.Schema.Result ( Result )
3922
4023
4124-- | This type family is used to specify columns in 'Rel8able's. In @Column f
@@ -43,75 +26,11 @@ import Rel8.Type ( DBType )
4326-- 'Rel8able' definitions), and @a@ is the type of the column.
4427type Column :: K.Context -> Type -> Type
4528type family Column context a where
46− Column (Reify context) a = AColumn context a
4729 Column Aggregate a = Aggregate a
4830 Column Expr a = Expr a
4931 Column Name a = Name a
5032 Column Result a = a
5133
5234
53−type AColumn :: K.Context -> Type -> Type
54−newtype AColumn context a = AColumn (Column context a)
55−
56−
57−instance (Reifiable context, Sql DBType a) =>
58− Table (Reify context) (AColumn context a)
59− where
60− type Context (AColumn context a) = Reify context
61− type Columns (AColumn context a) = HType a
62− type Unreify (AColumn context a) = Column context a
63−
64− fromColumns (HType (Reify a)) = sfromColumn contextSing a
65− toColumns = HType . Reify . stoColumn contextSing
66− reify _ = AColumn
67− unreify _ (AColumn a) = a
68−
69− coherence Refl = case contextSing @context of
70− SAggregate -> const Refl
71− SExpr -> const Refl
72− SName -> const Refl
73− SResult -> absurd
74− SReify _ -> const Refl
75−
76− congruence Refl = case contextSing @context of
77− SAggregate -> const Refl
78− SExpr -> const Refl
79− SName -> const Refl
80− SResult -> absurd
81− SReify _ -> const Refl
82−
83−
84−instance (Reifiable context, Reifiable context', Sql DBType a) =>
85− Recontextualize
86− (Reify context)
87− (Reify context')
88− (AColumn context a)
89− (AColumn context' a)
90−
91−
92−sfromColumn :: ()
93− => SContext context
94− -> Col context ('Spec a)
95− -> AColumn context a
96−sfromColumn = \case
97− SAggregate -> \(A a) -> AColumn a
98− SExpr -> \(E a) -> AColumn a
99− SName -> \(N a) -> AColumn a
100− SResult -> \(R a) -> AColumn a
101− SReify context -> \(Reify a) -> AColumn (sfromColumn context a)
102−
103−
104−stoColumn :: ()
105− => SContext context
106− -> AColumn context a
107− -> Col context ('Spec a)
108−stoColumn = \case
109− SAggregate -> \(AColumn a) -> A a
110− SExpr -> \(AColumn a) -> E a
111− SName -> \(AColumn a) -> N a
112− SResult -> \(AColumn a) -> R a
113− SReify context -> \(AColumn a) -> Reify (stoColumn context a)
114−
115−
11635data TColumn :: K.Context -> Type -> Exp Type
11736type instance Eval (TColumn f a) = Column f a
src/Rel8/Column/ADT.hs+4−87
@@ -1,106 +1,23 @@
11{-# language DataKinds #-}
2−{-# language LambdaCase #-}
3−{-# language MultiParamTypeClasses #-}
4−{-# language ScopedTypeVariables #-}
52{-# language StandaloneKindSignatures #-}
6−{-# language TypeApplications #-}
73{-# language TypeFamilies #-}
8−{-# language UndecidableInstances #-}
94
105module Rel8.Column.ADT
11− ( HADT, AHADT(..)
6+ ( HADT
127 )
138where
149
1510-- base
1611import Data.Kind ( Type )
17−import Data.Type.Equality ( (:~:)( Refl ) )
18−import Prelude
12+import Prelude ()
1913
2014-- rel8
21−import Rel8.Generic.Rel8able ( GColumns )
22−import Rel8.Kind.Context ( SContext(..), Reifiable, contextSing )
23−import Rel8.Schema.Context ( Col )
2415import qualified Rel8.Schema.Kind as K
25−import Rel8.Schema.Reify ( Reify, hreify, hunreify )
26−import Rel8.Schema.Result ( Result, absurd )
27−import Rel8.Table
28− ( Table, Columns, Context, fromColumns, toColumns
29− , Unreify, reify, unreify, coherence, congruence
30− )
31−import Rel8.Table.ADT ( ADT( ADT ), ADTable, fromADT, toADT )
32−import Rel8.Table.Rel8able ()
33−import Rel8.Table.Recontextualize ( Recontextualize )
16+import Rel8.Schema.Result ( Result )
17+import Rel8.Table.ADT ( ADT )
3418
3519
3620type HADT :: K.Context -> K.Rel8able -> Type
3721type family HADT context t where
38− HADT (Reify context) t = AHADT context t
3922 HADT Result t = t Result
4023 HADT context t = ADT t context
41−
42−
43−type AHADT :: K.Context -> K.Rel8able -> Type
44−newtype AHADT context t = AHADT (HADT context t)
45−
46−
47−instance (ADTable t, Reifiable context) =>
48− Table (Reify context) (AHADT context t)
49− where
50− type Context (AHADT context t) = Reify context
51− type Columns (AHADT context t) = GColumns (ADT t)
52− type Unreify (AHADT context t) = HADT context t
53−
54− fromColumns = sfromColumnsADT contextSing
55− toColumns = stoColumnsADT contextSing
56− reify _ = AHADT
57− unreify _ (AHADT a) = a
58−
59− coherence = case contextSing @context of
60− SAggregate -> \Refl _ -> Refl
61− SExpr -> \Refl _ -> Refl
62− SName -> \Refl _ -> Refl
63− SResult -> \Refl -> absurd
64− SReify _ -> \Refl _ -> Refl
65−
66− congruence = case contextSing @context of
67− SAggregate -> \_ _ -> Refl
68− SExpr -> \_ _ -> Refl
69− SName -> \_ _ -> Refl
70− SResult -> \Refl -> absurd
71− SReify _ -> \_ _ -> Refl
72−
73−
74−instance
75− ( Reifiable context, Reifiable context'
76− , ADTable t, t ~ t'
77− )
78− => Recontextualize
79− (Reify context)
80− (Reify context')
81− (AHADT context t)
82− (AHADT context' t')
83−
84−
85−sfromColumnsADT :: ADTable t
86− => SContext context
87− -> GColumns (ADT t) (Col (Reify context))
88− -> AHADT context t
89−sfromColumnsADT = \case
90− SAggregate -> AHADT . ADT . hunreify
91− SExpr -> AHADT . ADT . hunreify
92− SName -> AHADT . ADT . hunreify
93− SResult -> AHADT . fromADT . ADT . hunreify
94− SReify context -> AHADT . sfromColumnsADT context . hunreify
95−
96−
97−stoColumnsADT :: ADTable t
98− => SContext context
99− -> AHADT context t
100− -> GColumns (ADT t) (Col (Reify context))
101−stoColumnsADT = \case
102− SAggregate -> hreify . (\(AHADT (ADT a)) -> a)
103− SExpr -> hreify . (\(AHADT (ADT a)) -> a)
104− SName -> hreify . (\(AHADT (ADT a)) -> a)
105− SResult -> hreify . (\(ADT a) -> a) . toADT . (\(AHADT a) -> a)
106− SReify context -> hreify . stoColumnsADT context . (\(AHADT a) -> a)
src/Rel8/Column/Either.hs+4−165
@@ -1,42 +1,23 @@
11{-# language DataKinds #-}
2−{-# language FlexibleContexts #-}
3−{-# language LambdaCase #-}
4−{-# language MultiParamTypeClasses #-}
5−{-# language ScopedTypeVariables #-}
62{-# language StandaloneKindSignatures #-}
7−{-# language TypeApplications #-}
83{-# language TypeFamilyDependencies #-}
9−{-# language UndecidableInstances #-}
104
115module Rel8.Column.Either
12− ( HEither, AHEither(..)
6+ ( HEither
137 )
148where
159
1610-- base
17−import Control.Applicative ( liftA2 )
18−import Control.Category ( id )
19−import Data.Bifunctor ( Bifunctor, bimap )
2011import Data.Kind ( Type )
21−import Data.Type.Equality ( (:~:)( Refl ), apply )
22−import Prelude hiding ( id )
12+import Prelude
2313
2414-- rel8
2515import Rel8.Aggregate ( Aggregate )
2616import Rel8.Expr ( Expr )
27−import Rel8.Kind.Context ( SContext(..), Reifiable( contextSing ) )
28−import Rel8.Schema.Context ( Col )
29−import Rel8.Schema.HTable.Either ( HEitherTable )
3017import qualified Rel8.Schema.Kind as K
31−import Rel8.Schema.Name ( Name(..) )
32−import Rel8.Schema.Reify ( Reify, hreify, hunreify )
33−import Rel8.Schema.Result ( Result, absurd )
34−import Rel8.Table
35− ( Table, Columns, Context, fromColumns, toColumns
36− , Unreify, reify, unreify, coherence, congruence
37− )
18+import Rel8.Schema.Name ( Name )
19+import Rel8.Schema.Result ( Result )
3820import Rel8.Table.Either ( EitherTable )
39−import Rel8.Table.Recontextualize ( Recontextualize )
4021
4122
4223-- | Nest an 'Either' value within a 'Rel8able'. @HEither f a b@ will produce a
@@ -44,149 +25,7 @@ import Rel8.Table.Recontextualize ( Recontextualize )
4425-- 'Result' context.
4526type HEither :: K.Context -> Type -> Type -> Type
4627type family HEither context = either | either -> context where
47− HEither (Reify context) = AHEither context
4828 HEither Aggregate = EitherTable Aggregate
4929 HEither Expr = EitherTable Expr
5030 HEither Name = EitherTable Name
5131 HEither Result = Either
52−
53−
54−type AHEither :: K.Context -> Type -> Type -> Type
55−newtype AHEither context a b = AHEither (HEither context a b)
56−
57−
58−instance Reifiable context => Bifunctor (AHEither context) where
59− bimap = sbimapEither contextSing
60−
61−
62−instance Reifiable context => Functor (AHEither context a) where
63− fmap = bimap id
64−
65−
66−instance (Reifiable context, Table (Reify context) a, Table (Reify context) b)
67− => Table (Reify context) (AHEither context a b)
68− where
69− type Context (AHEither context a b) = Reify context
70− type Columns (AHEither context a b) = HEitherTable (Columns a) (Columns b)
71− type Unreify (AHEither context a b) = HEither context (Unreify a) (Unreify b)
72−
73− fromColumns = sfromColumnsEither contextSing
74− toColumns = stoColumnsEither contextSing
75− reify proof = liftA2 bimap reify reify proof . AHEither
76− unreify proof = (\(AHEither a) -> a) . liftA2 bimap unreify unreify proof
77−
78− coherence = case contextSing @context of
79− SAggregate -> coherence @(Reify context) @a
80− SExpr -> coherence @(Reify context) @a
81− SName -> coherence @(Reify context) @a
82− SResult -> \Refl -> absurd
83− SReify _ -> \Refl _ -> Refl
84−
85− congruence proof@Refl abstract = case contextSing @context of
86− SAggregate ->
87− id `apply`
88− congruence @(Reify context) @a proof abstract `apply`
89− congruence @(Reify context) @b proof abstract
90− SExpr ->
91− id `apply`
92− congruence @(Reify context) @a proof abstract `apply`
93− congruence @(Reify context) @b proof abstract
94− SName ->
95− id `apply`
96− congruence @(Reify context) @a proof abstract `apply`
97− congruence @(Reify context) @b proof abstract
98− SResult -> absurd abstract
99− SReify _ ->
100− id `apply`
101− congruence @(Reify context) @a proof abstract `apply`
102− congruence @(Reify context) @b proof abstract
103−
104−
105−instance
106− ( Reifiable context, Reifiable context'
107− , Recontextualize (Reify context) (Reify context') a a'
108− , Recontextualize (Reify context) (Reify context') b b'
109− ) =>
110− Recontextualize
111− (Reify context)
112− (Reify context')
113− (AHEither context a b)
114− (AHEither context' a' b')
115−
116−
117−sbimapEither :: ()
118− => SContext context
119− -> (a -> c)
120− -> (b -> d)
121− -> AHEither context a b
122− -> AHEither context c d
123−sbimapEither = \case
124− SAggregate -> \f g (AHEither a) -> AHEither (bimap f g a)
125− SExpr -> \f g (AHEither a) -> AHEither (bimap f g a)
126− SResult -> \f g (AHEither a) -> AHEither (bimap f g a)
127− SName -> \f g (AHEither a) -> AHEither (bimap f g a)
128− SReify context -> \f g (AHEither a) -> AHEither (sbimapEither context f g a)
129−
130−
131−sfromColumnsEither :: (Table (Reify context) a, Table (Reify context) b)
132− => SContext context
133− -> HEitherTable (Columns a) (Columns b) (Col (Reify context))
134− -> AHEither context a b
135−sfromColumnsEither = \case
136− SAggregate ->
137− AHEither .
138− bimap (fromColumns . hreify) (fromColumns . hreify) .
139− fromColumns .
140− hunreify
141− SExpr ->
142− AHEither .
143− bimap (fromColumns . hreify) (fromColumns . hreify) .
144− fromColumns .
145− hunreify
146− SResult ->
147− AHEither .
148− bimap (fromColumns . hreify) (fromColumns . hreify) .
149− fromColumns .
150− hunreify
151− SName ->
152− AHEither .
153− bimap (fromColumns . hreify) (fromColumns . hreify) .
154− fromColumns .
155− hunreify
156− SReify context ->
157− AHEither .
158− sbimapEither context (fromColumns . hreify) (fromColumns . hreify) .
159− sfromColumnsEither context .
160− hunreify
161−
162−
163−stoColumnsEither :: (Table (Reify context) a, Table (Reify context) b)
164− => SContext context
165− -> AHEither context a b
166− -> HEitherTable (Columns a) (Columns b) (Col (Reify context))
167−stoColumnsEither = \case
168− SAggregate ->
169− hreify .
170− toColumns .
171− bimap (hunreify . toColumns) (hunreify . toColumns) .
172− (\(AHEither a) -> a)
173− SExpr ->
174− hreify .
175− toColumns .
176− bimap (hunreify . toColumns) (hunreify . toColumns) .
177− (\(AHEither a) -> a)
178− SResult ->
179− hreify .
180− toColumns .
181− bimap (hunreify . toColumns) (hunreify . toColumns) .
182− (\(AHEither a) -> a)
183− SName ->
184− hreify .
185− toColumns .
186− bimap (hunreify . toColumns) (hunreify . toColumns) .
187− (\(AHEither a) -> a)
188− SReify context ->
189− hreify .
190− stoColumnsEither context .
191− sbimapEither context (hunreify . toColumns) (hunreify . toColumns) .
192− (\(AHEither a) -> a)
src/Rel8/Column/Lift.hs+4−85
@@ -1,104 +1,23 @@
11{-# language DataKinds #-}
2−{-# language LambdaCase #-}
3−{-# language MultiParamTypeClasses #-}
4−{-# language ScopedTypeVariables #-}
52{-# language StandaloneKindSignatures #-}
6−{-# language TypeApplications #-}
73{-# language TypeFamilies #-}
84
95module Rel8.Column.Lift
10− ( Lift, ALift(..)
6+ ( Lift
117 )
128where
139
1410-- base
1511import Data.Kind ( Type )
16−import Data.Type.Equality ( (:~:)( Refl ) )
17−import Prelude
12+import Prelude ()
1813
1914-- rel8
20−import Rel8.Generic.Rel8able ( GColumns )
21−import Rel8.Kind.Context ( Reifiable(..), SContext(..) )
22−import Rel8.Schema.Context ( Col )
2315import qualified Rel8.Schema.Kind as K
24−import Rel8.Schema.Reify ( Reify, hreify, hunreify )
25−import Rel8.Schema.Result ( Result, absurd )
26−import Rel8.Table
27− ( Table, Columns, Context, fromColumns, toColumns
28− , Unreify, reify, unreify, coherence, congruence
29− )
30−import Rel8.Table.Rel8able ()
31−import Rel8.Table.HKD ( HKD( HKD ), HKDable, fromHKD, toHKD )
32−import Rel8.Table.Recontextualize ( Recontextualize )
16+import Rel8.Schema.Result ( Result )
17+import Rel8.Table.HKD ( HKD )
3318
3419
3520type Lift :: K.Context -> Type -> Type
3621type family Lift context a where
37− Lift (Reify context) a = ALift context a
3822 Lift Result a = a
3923 Lift context a = HKD a context
40−
41−
42−type ALift :: K.Context -> Type -> Type
43−newtype ALift context a = ALift
44− { unALift :: Lift context a
45− }
46−
47−
48−instance (Reifiable context, HKDable a) =>
49− Table (Reify context) (ALift context a)
50− where
51− type Context (ALift context a) = Reify context
52− type Columns (ALift context a) = GColumns (HKD a)
53− type Unreify (ALift context a) = Lift context a
54−
55− fromColumns = sfromColumnsLift contextSing
56− toColumns = stoColumnsLift contextSing
57− reify _ = ALift
58− unreify _ (ALift a) = a
59−
60− coherence = case contextSing @context of
61− SAggregate -> \Refl _ -> Refl
62− SExpr -> \Refl _ -> Refl
63− SName -> \Refl _ -> Refl
64− SResult -> \Refl -> absurd
65− SReify _ -> \Refl _ -> Refl
66−
67− congruence = case contextSing @context of
68− SAggregate -> \_ _ -> Refl
69− SExpr -> \_ _ -> Refl
70− SName -> \_ _ -> Refl
71− SResult -> \Refl -> absurd
72− SReify _ -> \_ _ -> Refl
73−
74−
75−instance (Reifiable context, Reifiable context', HKDable a) =>
76− Recontextualize
77− (Reify context)
78− (Reify context')
79− (ALift context a)
80− (ALift context' a)
81−
82−
83−sfromColumnsLift :: HKDable a
84− => SContext context
85− -> GColumns (HKD a) (Col (Reify context))
86− -> ALift context a
87−sfromColumnsLift = \case
88− SAggregate -> ALift . fromColumns . hunreify
89− SExpr -> ALift . fromColumns . hunreify
90− SName -> ALift . fromColumns . hunreify
91− SResult -> ALift . fromHKD . HKD . hunreify
92− SReify context -> ALift . sfromColumnsLift context . hunreify
93−
94−
95−stoColumnsLift :: HKDable a
96− => SContext context
97− -> ALift context a
98− -> GColumns (HKD a) (Col (Reify context))
99−stoColumnsLift = \case
100− SAggregate -> hreify . toColumns . unALift
101− SExpr -> hreify . toColumns . unALift
102− SName -> hreify . toColumns . unALift
103− SResult -> hreify . (\(HKD a) -> a) . toHKD . unALift
104− SReify context -> hreify . stoColumnsLift context . unALift
src/Rel8/Column/List.hs+4−146
@@ -1,172 +1,30 @@
11{-# language DataKinds #-}
2−{-# language FlexibleContexts #-}
3−{-# language LambdaCase #-}
4−{-# language MultiParamTypeClasses #-}
5−{-# language RankNTypes #-}
6−{-# language ScopedTypeVariables #-}
72{-# language StandaloneKindSignatures #-}
8−{-# language TypeApplications #-}
93{-# language TypeFamilyDependencies #-}
10−{-# language UndecidableInstances #-}
114
125module Rel8.Column.List
13− ( HList, AHList(..)
6+ ( HList
147 )
158where
169
1710-- base
18−import Control.Category ( id )
1911import Data.Kind ( Type )
20−import Data.Type.Equality ( (:~:)( Refl ), apply )
21−import Prelude hiding ( id )
12+import Prelude ()
2213
2314-- rel8
2415import Rel8.Aggregate ( Aggregate )
2516import Rel8.Expr ( Expr )
26−import Rel8.Kind.Context ( SContext(..), Reifiable( contextSing ) )
27−import Rel8.Schema.Context ( Col )
28−import Rel8.Schema.Context.Abstract ( exclusivity, virtualOrResult )
29−import Rel8.Schema.HTable.List ( HListTable )
3017import qualified Rel8.Schema.Kind as K
3118import Rel8.Schema.Name ( Name )
32−import Rel8.Schema.Reify ( Reify, hreify, hunreify )
33−import Rel8.Schema.Result ( Result, absurd )
34−import Rel8.Table
35− ( Table, Columns, Congruent, Context, fromColumns, toColumns
36− , Unreify, reify, unreify, coherence, congruence
37− )
38−import Rel8.Table.List ( ListTable( ListTable ) )
39−import Rel8.Table.Recontextualize ( Recontextualize )
19+import Rel8.Schema.Result ( Result )
20+import Rel8.Table.List ( ListTable )
4021
4122
4223-- | Nest a list within a 'Rel8able'. @HList f a@ will produce a 'ListTable'
4324-- @a@ in the 'Expr' context, and a @[a]@ in the 'Result' context.
4425type HList :: K.Context -> Type -> Type
4526type family HList context = list | list -> context where
46− HList (Reify context) = AHList context
4727 HList Aggregate = ListTable Aggregate
4828 HList Expr = ListTable Expr
4929 HList Name = ListTable Name
5030 HList Result = []
51−
52−
53−type AHList :: K.Context -> Type -> Type
54−newtype AHList context a = AHList (HList context a)
55−
56−
57−instance (Reifiable context, Table (Reify context) a) =>
58− Table (Reify context) (AHList context a)
59− where
60− type Context (AHList context a) = Reify context
61− type Columns (AHList context a) = HListTable (Columns a)
62− type Unreify (AHList context a) = HList context (Unreify a)
63−
64− fromColumns = sfromColumnsList contextSing
65− toColumns = stoColumnsList contextSing
66−
67− reify _ = sreifyList contextSing
68− unreify _ = sunreifyList contextSing
69−
70− coherence = case contextSing @context of
71− SAggregate -> coherence @(Reify context) @a
72− SExpr -> coherence @(Reify context) @a
73− SName -> coherence @(Reify context) @a
74− SResult -> \Refl -> absurd
75− SReify _ -> \Refl _ -> Refl
76−
77− congruence proof@Refl abstract = case contextSing @context of
78− SAggregate -> id `apply` congruence @(Reify context) @a proof abstract
79− SExpr -> id `apply` congruence @(Reify context) @a proof abstract
80− SName -> id `apply` congruence @(Reify context) @a proof abstract
81− SResult -> absurd abstract
82− SReify _ -> id `apply` congruence @(Reify context) @a proof abstract
83−
84−
85−instance
86− ( Reifiable context, Reifiable context'
87− , Recontextualize (Reify context) (Reify context') a a'
88− )
89− => Recontextualize
90− (Reify context)
91− (Reify context')
92− (AHList context a)
93− (AHList context' a')
94−
95−
96−smapList :: Congruent a b
97− => SContext context
98− -> (a -> b)
99− -> (HListTable (Columns a) (Col (Context a)) -> HListTable (Columns b) (Col (Context b)))
100− -> AHList context a
101− -> AHList context b
102−smapList = \case
103− SAggregate -> \_ f (AHList (ListTable a)) -> AHList (ListTable (f a))
104− SExpr -> \_ f (AHList (ListTable a)) -> AHList (ListTable (f a))
105− SResult -> \f _ (AHList as) -> AHList (fmap f as)
106− SName -> \_ f (AHList (ListTable a)) -> AHList (ListTable (f a))
107− SReify context -> \f g (AHList as) -> AHList (smapList context f g as)
108−
109−
110−sfromColumnsList :: Table (Reify context) a
111− => SContext context
112− -> HListTable (Columns a) (Col (Reify context))
113− -> AHList context a
114−sfromColumnsList = \case
115− SAggregate -> AHList . ListTable
116− SExpr -> AHList . ListTable
117− SResult -> AHList . fmap (fromColumns . hreify) . fromColumns . hunreify
118− SName -> AHList . ListTable
119− SReify context ->
120− AHList .
121− smapList context (fromColumns . hreify) hreify .
122− sfromColumnsList context .
123− hunreify
124−
125−
126−stoColumnsList :: Table (Reify context) a
127− => SContext context
128− -> AHList context a
129− -> HListTable (Columns a) (Col (Reify context))
130−stoColumnsList = \case
131− SAggregate -> \(AHList (ListTable a)) -> a
132− SExpr -> \(AHList (ListTable a)) -> a
133− SResult ->
134− hreify . toColumns . fmap (hunreify . toColumns) . (\(AHList a) -> a)
135− SName -> \(AHList (ListTable a)) -> a
136− SReify context ->
137− hreify .
138− stoColumnsList context .
139− smapList context (hunreify . toColumns) hunreify .
140− (\(AHList a) -> a)
141−
142−
143−sreifyList :: forall context a. Table (Reify context) a
144− => SContext context
145− -> HList context (Unreify a)
146− -> AHList context a
147−sreifyList context = case virtualOrResult context of
148− Left Refl -> AHList . fmap (reify Refl)
149− Right virtual ->
150− case coherence @(Reify context) @a Refl abstract of
151− Refl -> case congruence @(Reify context) @a Refl abstract of
152− Refl ->
153− smapList context (reify Refl) hreify .
154− AHList
155− where
156− abstract = exclusivity virtual
157−
158−
159−sunreifyList :: forall context a. Table (Reify context) a
160− => SContext context
161− -> AHList context a
162− -> HList context (Unreify a)
163−sunreifyList context = case virtualOrResult context of
164− Left Refl -> fmap (unreify Refl) . (\(AHList a) -> a)
165− Right virtual ->
166− case coherence @(Reify context) @a Refl abstract of
167− Refl -> case congruence @(Reify context) @a Refl abstract of
168− Refl ->
169− (\(AHList a) -> a) .
170− smapList context (unreify Refl) hunreify
171− where
172− abstract = exclusivity virtual
src/Rel8/Column/Maybe.hs+3−117
@@ -1,41 +1,23 @@
11{-# language DataKinds #-}
2−{-# language FlexibleContexts #-}
3−{-# language GADTs #-}
4−{-# language LambdaCase #-}
5−{-# language MultiParamTypeClasses #-}
6−{-# language ScopedTypeVariables #-}
72{-# language StandaloneKindSignatures #-}
8−{-# language TypeApplications #-}
93{-# language TypeFamilyDependencies #-}
10−{-# language UndecidableInstances #-}
114
125module Rel8.Column.Maybe
13− ( HMaybe, AHMaybe(..)
6+ ( HMaybe
147 )
158where
169
1710-- base
18−import Control.Category ( id )
1911import Data.Kind ( Type )
20−import Data.Type.Equality ( (:~:)( Refl ), apply )
21−import Prelude hiding ( id )
12+import Prelude
2213
2314-- rel8
2415import Rel8.Aggregate ( Aggregate )
2516import Rel8.Expr ( Expr )
26−import Rel8.Kind.Context ( SContext(..), Reifiable( contextSing ) )
27−import Rel8.Schema.Context ( Col )
28−import Rel8.Schema.HTable.Maybe ( HMaybeTable )
2917import qualified Rel8.Schema.Kind as K
3018import Rel8.Schema.Name ( Name )
31−import Rel8.Schema.Reify ( Reify, hreify, hunreify )
32−import Rel8.Schema.Result ( Result, absurd )
33−import Rel8.Table
34− ( Table, Columns, Context, fromColumns, toColumns
35− , Unreify, reify, unreify, coherence, congruence
36− )
19+import Rel8.Schema.Result ( Result )
3720import Rel8.Table.Maybe ( MaybeTable )
38−import Rel8.Table.Recontextualize ( Recontextualize )
3921
4022
4123-- | Nest a 'Maybe' value within a 'Rel8able'. @HMaybe f a@ will produce a
@@ -43,103 +25,7 @@ import Rel8.Table.Recontextualize ( Recontextualize )
4325-- context.
4426type HMaybe :: K.Context -> Type -> Type
4527type family HMaybe context = maybe | maybe -> context where
46− HMaybe (Reify context) = AHMaybe context
4728 HMaybe Aggregate = MaybeTable Aggregate
4829 HMaybe Expr = MaybeTable Expr
4930 HMaybe Name = MaybeTable Name
5031 HMaybe Result = Maybe
51−
52−
53−type AHMaybe :: K.Context -> Type -> Type
54−newtype AHMaybe context a = AHMaybe (HMaybe context a)
55−
56−
57−instance Reifiable context => Functor (AHMaybe context) where
58− fmap = smapMaybe contextSing
59−
60−
61−instance (Reifiable context, Table (Reify context) a) =>
62− Table (Reify context) (AHMaybe context a)
63− where
64− type Context (AHMaybe context a) = Reify context
65− type Columns (AHMaybe context a) = HMaybeTable (Columns a)
66− type Unreify (AHMaybe context a) = HMaybe context (Unreify a)
67−
68− fromColumns = sfromColumnsMaybe contextSing
69− toColumns = stoColumnsMaybe contextSing
70− reify proof = fmap fmap reify proof . AHMaybe
71− unreify proof = (\(AHMaybe a) -> a) . fmap fmap unreify proof
72−
73− coherence = case contextSing @context of
74− SAggregate -> coherence @(Reify context) @a
75− SExpr -> coherence @(Reify context) @a
76− SName -> coherence @(Reify context) @a
77− SResult -> \Refl -> absurd
78− SReify _ -> \Refl _ -> Refl
79−
80− congruence proof@Refl abstract = case contextSing @context of
81− SAggregate -> id `apply` congruence @(Reify context) @a proof abstract
82− SExpr -> id `apply` congruence @(Reify context) @a proof abstract
83− SName -> id `apply` congruence @(Reify context) @a proof abstract
84− SResult -> absurd abstract
85− SReify _ -> id `apply` congruence @(Reify context) @a proof abstract
86−
87−
88−instance
89− ( Reifiable context, Reifiable context'
90− , Recontextualize (Reify context) (Reify context') a a'
91− )
92− => Recontextualize
93− (Reify context)
94− (Reify context')
95− (AHMaybe context a)
96− (AHMaybe context' a')
97−
98−
99−smapMaybe :: ()
100− => SContext context
101− -> (a -> b)
102− -> AHMaybe context a
103− -> AHMaybe context b
104−smapMaybe = \case
105− SAggregate -> \f (AHMaybe a) -> AHMaybe (fmap f a)
106− SExpr -> \f (AHMaybe a) -> AHMaybe (fmap f a)
107− SResult -> \f (AHMaybe a) -> AHMaybe (fmap f a)
108− SName -> \f (AHMaybe a) -> AHMaybe (fmap f a)
109− SReify context -> \f (AHMaybe a) -> AHMaybe (smapMaybe context f a)
110−
111−
112−sfromColumnsMaybe :: Table (Reify context) a
113− => SContext context
114− -> HMaybeTable (Columns a) (Col (Reify context))
115− -> AHMaybe context a
116−sfromColumnsMaybe = \case
117− SAggregate -> AHMaybe . fmap (fromColumns . hreify) . fromColumns . hunreify
118− SExpr -> AHMaybe . fmap (fromColumns . hreify) . fromColumns . hunreify
119− SResult -> AHMaybe . fmap (fromColumns . hreify) . fromColumns . hunreify
120− SName -> AHMaybe . fmap (fromColumns . hreify) . fromColumns . hunreify
121− SReify context ->
122− AHMaybe .
123− smapMaybe context (fromColumns . hreify) .
124− sfromColumnsMaybe context .
125− hunreify
126−
127−
128−stoColumnsMaybe :: Table (Reify context) a
129− => SContext context
130− -> AHMaybe context a
131− -> HMaybeTable (Columns a) (Col (Reify context))
132−stoColumnsMaybe = \case
133− SAggregate ->
134− hreify . toColumns . fmap (hunreify . toColumns) . (\(AHMaybe a) -> a)
135− SExpr ->
136− hreify . toColumns . fmap (hunreify . toColumns) . (\(AHMaybe a) -> a)
137− SResult ->
138− hreify . toColumns . fmap (hunreify . toColumns) . (\(AHMaybe a) -> a)
139− SName ->
140− hreify . toColumns . fmap (hunreify . toColumns) . (\(AHMaybe a) -> a)
141− SReify context ->
142− hreify .
143− stoColumnsMaybe context .
144− smapMaybe context (hunreify . toColumns) .
145− (\(AHMaybe a) -> a)
src/Rel8/Column/NonEmpty.hs+4−146
@@ -1,42 +1,24 @@
11{-# language DataKinds #-}
2−{-# language FlexibleContexts #-}
3−{-# language LambdaCase #-}
4−{-# language MultiParamTypeClasses #-}
5−{-# language ScopedTypeVariables #-}
62{-# language StandaloneKindSignatures #-}
7−{-# language TypeApplications #-}
83{-# language TypeFamilyDependencies #-}
9−{-# language UndecidableInstances #-}
104
115module Rel8.Column.NonEmpty
12− ( HNonEmpty, AHNonEmpty(..)
6+ ( HNonEmpty
137 )
148where
159
1610-- base
17−import Control.Category ( id )
1811import Data.Kind ( Type )
1912import Data.List.NonEmpty ( NonEmpty )
20−import Data.Type.Equality ( (:~:)( Refl ), apply )
21−import Prelude hiding ( id )
13+import Prelude ()
2214
2315-- rel8
2416import Rel8.Aggregate ( Aggregate )
2517import Rel8.Expr ( Expr )
26−import Rel8.Kind.Context ( SContext(..), Reifiable( contextSing ) )
27−import Rel8.Schema.Context ( Col )
28−import Rel8.Schema.Context.Abstract ( exclusivity, virtualOrResult )
29−import Rel8.Schema.HTable.NonEmpty ( HNonEmptyTable )
3018import qualified Rel8.Schema.Kind as K
3119import Rel8.Schema.Name ( Name )
32−import Rel8.Schema.Reify ( Reify, hreify, hunreify )
33−import Rel8.Schema.Result ( Result, absurd )
34−import Rel8.Table
35− ( Table, Columns, Congruent, Context, fromColumns, toColumns
36− , Unreify, reify, unreify, coherence, congruence
37− )
38−import Rel8.Table.NonEmpty ( NonEmptyTable( NonEmptyTable ) )
39−import Rel8.Table.Recontextualize ( Recontextualize )
20+import Rel8.Schema.Result ( Result )
21+import Rel8.Table.NonEmpty ( NonEmptyTable )
4022
4123
4224-- | Nest a 'NonEmpty' list within a 'Rel8able'. @HNonEmpty f a@ will produce a
@@ -44,131 +26,7 @@ import Rel8.Table.Recontextualize ( Recontextualize )
4426-- 'Result' context.
4527type HNonEmpty :: K.Context -> Type -> Type
4628type family HNonEmpty context = nonEmpty | nonEmpty -> context where
47− HNonEmpty (Reify context) = AHNonEmpty context
4829 HNonEmpty Aggregate = NonEmptyTable Aggregate
4930 HNonEmpty Expr = NonEmptyTable Expr
5031 HNonEmpty Name = NonEmptyTable Name
5132 HNonEmpty Result = NonEmpty
52−
53−
54−type AHNonEmpty :: K.Context -> Type -> Type
55−newtype AHNonEmpty context a = AHNonEmpty (HNonEmpty context a)
56−
57−
58−instance (Reifiable context, Table (Reify context) a) =>
59− Table (Reify context) (AHNonEmpty context a)
60− where
61− type Context (AHNonEmpty context a) = Reify context
62− type Columns (AHNonEmpty context a) = HNonEmptyTable (Columns a)
63− type Unreify (AHNonEmpty context a) = HNonEmpty context (Unreify a)
64−
65− fromColumns = sfromColumnsNonEmpty contextSing
66− toColumns = stoColumnsNonEmpty contextSing
67−
68− reify _ = sreifyNonEmpty contextSing
69− unreify _ = sunreifyNonEmpty contextSing
70−
71− coherence = case contextSing @context of
72− SAggregate -> coherence @(Reify context) @a
73− SExpr -> coherence @(Reify context) @a
74− SName -> coherence @(Reify context) @a
75− SResult -> \Refl -> absurd
76− SReify _ -> \Refl _ -> Refl
77−
78− congruence proof@Refl abstract = case contextSing @context of
79− SAggregate -> id `apply` congruence @(Reify context) @a proof abstract
80− SExpr -> id `apply` congruence @(Reify context) @a proof abstract
81− SName -> id `apply` congruence @(Reify context) @a proof abstract
82− SResult -> absurd abstract
83− SReify _ -> id `apply` congruence @(Reify context) @a proof abstract
84−
85−
86−instance
87− ( Reifiable context, Reifiable context'
88− , Recontextualize (Reify context) (Reify context') a a'
89− )
90− => Recontextualize
91− (Reify context)
92− (Reify context')
93− (AHNonEmpty context a)
94− (AHNonEmpty context' a')
95−
96−
97−smapNonEmpty :: Congruent a b
98− => SContext context
99− -> (a -> b)
100− -> (HNonEmptyTable (Columns a) (Col (Context a)) -> HNonEmptyTable (Columns b) (Col (Context b)))
101− -> AHNonEmpty context a
102− -> AHNonEmpty context b
103−smapNonEmpty = \case
104− SAggregate -> \_ f (AHNonEmpty (NonEmptyTable a)) -> AHNonEmpty (NonEmptyTable (f a))
105− SExpr -> \_ f (AHNonEmpty (NonEmptyTable a)) -> AHNonEmpty (NonEmptyTable (f a))
106− SResult -> \f _ (AHNonEmpty as) -> AHNonEmpty (fmap f as)
107− SName -> \_ f (AHNonEmpty (NonEmptyTable a)) -> AHNonEmpty (NonEmptyTable (f a))
108− SReify context -> \f g (AHNonEmpty as) -> AHNonEmpty (smapNonEmpty context f g as)
109−
110−
111−sfromColumnsNonEmpty :: Table (Reify context) a
112− => SContext context
113− -> HNonEmptyTable (Columns a) (Col (Reify context))
114− -> AHNonEmpty context a
115−sfromColumnsNonEmpty = \case
116− SAggregate -> AHNonEmpty . NonEmptyTable
117− SExpr -> AHNonEmpty . NonEmptyTable
118− SResult ->
119− AHNonEmpty . fmap (fromColumns . hreify) . fromColumns . hunreify
120− SName -> AHNonEmpty . NonEmptyTable
121− SReify context ->
122− AHNonEmpty .
123− smapNonEmpty context (fromColumns . hreify) hreify .
124− sfromColumnsNonEmpty context .
125− hunreify
126−
127−
128−stoColumnsNonEmpty :: Table (Reify context) a
129− => SContext context
130− -> AHNonEmpty context a
131− -> HNonEmptyTable (Columns a) (Col (Reify context))
132−stoColumnsNonEmpty = \case
133− SAggregate -> \(AHNonEmpty (NonEmptyTable a)) -> a
134− SExpr -> \(AHNonEmpty (NonEmptyTable a)) -> a
135− SResult ->
136− hreify . toColumns . fmap (hunreify . toColumns) . (\(AHNonEmpty a) -> a)
137− SName -> \(AHNonEmpty (NonEmptyTable a)) -> a
138− SReify context ->
139− hreify .
140− stoColumnsNonEmpty context .
141− smapNonEmpty context (hunreify . toColumns) hunreify .
142− (\(AHNonEmpty a) -> a)
143−
144−
145−sreifyNonEmpty :: forall context a. Table (Reify context) a
146− => SContext context
147− -> HNonEmpty context (Unreify a)
148− -> AHNonEmpty context a
149−sreifyNonEmpty context = case virtualOrResult context of
150− Left Refl -> AHNonEmpty . fmap (reify Refl)
151− Right virtual ->
152− case coherence @(Reify context) @a Refl abstract of
153− Refl -> case congruence @(Reify context) @a Refl abstract of
154− Refl ->
155− smapNonEmpty context (reify Refl) hreify .
156− AHNonEmpty
157− where
158− abstract = exclusivity virtual
159−
160−
161−sunreifyNonEmpty :: forall context a. Table (Reify context) a
162− => SContext context
163− -> AHNonEmpty context a
164− -> HNonEmpty context (Unreify a)
165−sunreifyNonEmpty context = case virtualOrResult context of
166− Left Refl -> fmap (unreify Refl) . (\(AHNonEmpty a) -> a)
167− Right virtual ->
168− case coherence @(Reify context) @a Refl abstract of
169− Refl -> case congruence @(Reify context) @a Refl abstract of
170− Refl ->
171− (\(AHNonEmpty a) -> a) .
172− smapNonEmpty context (unreify Refl) hunreify
173− where
174− abstract = exclusivity virtual
src/Rel8/Column/These.hs+3−165
@@ -1,42 +1,22 @@
11{-# language DataKinds #-}
2−{-# language FlexibleContexts #-}
3−{-# language GADTs #-}
4−{-# language LambdaCase #-}
5−{-# language MultiParamTypeClasses #-}
6−{-# language ScopedTypeVariables #-}
72{-# language StandaloneKindSignatures #-}
8−{-# language TypeApplications #-}
93{-# language TypeFamilyDependencies #-}
10−{-# language UndecidableInstances #-}
114
125module Rel8.Column.These
13− ( HThese, AHThese(..)
6+ ( HThese
147 )
158where
169
1710-- base
18−import Control.Applicative ( liftA2 )
19−import Control.Category ( id )
20−import Data.Bifunctor ( Bifunctor, bimap )
2111import Data.Kind ( Type )
22−import Data.Type.Equality ( (:~:)( Refl ), apply )
23−import Prelude hiding ( id )
12+import Prelude ()
2413
2514-- rel8
2615import Rel8.Aggregate ( Aggregate )
2716import Rel8.Expr ( Expr )
28−import Rel8.Kind.Context ( SContext(..), Reifiable( contextSing ) )
29−import Rel8.Schema.Context ( Col )
30−import Rel8.Schema.HTable.These ( HTheseTable )
3117import qualified Rel8.Schema.Kind as K
3218import Rel8.Schema.Name ( Name )
33−import Rel8.Schema.Reify ( Reify, hreify, hunreify )
34−import Rel8.Schema.Result ( Result, absurd )
35−import Rel8.Table
36− ( Table, Columns, Context, fromColumns, toColumns
37− , Unreify, reify, unreify, coherence, congruence
38− )
39−import Rel8.Table.Recontextualize ( Recontextualize )
19+import Rel8.Schema.Result ( Result )
4020import Rel8.Table.These ( TheseTable )
4121
4222-- these
@@ -48,149 +28,7 @@ import Data.These ( These )
4828-- 'Result' context.
4929type HThese :: K.Context -> Type -> Type -> Type
5030type family HThese context = these | these -> context where
51− HThese (Reify context) = AHThese context
5231 HThese Aggregate = TheseTable Aggregate
5332 HThese Expr = TheseTable Expr
5433 HThese Name = TheseTable Name
5534 HThese Result = These
56−
57−
58−type AHThese :: K.Context -> Type -> Type -> Type
59−newtype AHThese context a b = AHThese (HThese context a b)
60−
61−
62−instance Reifiable context => Bifunctor (AHThese context) where
63− bimap = sbimapThese contextSing
64−
65−
66−instance Reifiable context => Functor (AHThese context a) where
67− fmap = bimap id
68−
69−
70−instance (Reifiable context, Table (Reify context) a, Table (Reify context) b)
71− => Table (Reify context) (AHThese context a b)
72− where
73− type Context (AHThese context a b) = Reify context
74− type Columns (AHThese context a b) = HTheseTable (Columns a) (Columns b)
75− type Unreify (AHThese context a b) = HThese context (Unreify a) (Unreify b)
76−
77− fromColumns = sfromColumnsThese contextSing
78− toColumns = stoColumnsThese contextSing
79− reify proof = liftA2 bimap reify reify proof . AHThese
80− unreify proof = (\(AHThese a) -> a) . liftA2 bimap unreify unreify proof
81−
82− coherence = case contextSing @context of
83− SAggregate -> coherence @(Reify context) @a
84− SExpr -> coherence @(Reify context) @a
85− SName -> coherence @(Reify context) @a
86− SResult -> \Refl -> absurd
87− SReify _ -> \Refl _ -> Refl
88−
89− congruence proof@Refl abstract = case contextSing @context of
90− SAggregate ->
91− id `apply`
92− congruence @(Reify context) @a proof abstract `apply`
93− congruence @(Reify context) @b proof abstract
94− SExpr ->
95− id `apply`
96− congruence @(Reify context) @a proof abstract `apply`
97− congruence @(Reify context) @b proof abstract
98− SName ->
99− id `apply`
100− congruence @(Reify context) @a proof abstract `apply`
101− congruence @(Reify context) @b proof abstract
102− SResult -> absurd abstract
103− SReify _ ->
104− id `apply`
105− congruence @(Reify context) @a proof abstract `apply`
106− congruence @(Reify context) @b proof abstract
107−
108−
109−instance
110− ( Reifiable context, Reifiable context'
111− , Recontextualize (Reify context) (Reify context') a a'
112− , Recontextualize (Reify context) (Reify context') b b'
113− ) =>
114− Recontextualize
115− (Reify context)
116− (Reify context')
117− (AHThese context a b)
118− (AHThese context' a' b')
119−
120−
121−sbimapThese :: ()
122− => SContext context
123− -> (a -> c)
124− -> (b -> d)
125− -> AHThese context a b
126− -> AHThese context c d
127−sbimapThese = \case
128− SAggregate -> \f g (AHThese a) -> AHThese (bimap f g a)
129− SExpr -> \f g (AHThese a) -> AHThese (bimap f g a)
130− SResult -> \f g (AHThese a) -> AHThese (bimap f g a)
131− SName -> \f g (AHThese a) -> AHThese (bimap f g a)
132− SReify context -> \f g (AHThese a) -> AHThese (sbimapThese context f g a)
133−
134−
135−sfromColumnsThese :: (Table (Reify context) a, Table (Reify context) b)
136− => SContext context
137− -> HTheseTable (Columns a) (Columns b) (Col (Reify context))
138− -> AHThese context a b
139−sfromColumnsThese = \case
140− SAggregate ->
141− AHThese .
142− bimap (fromColumns . hreify) (fromColumns . hreify) .
143− fromColumns .
144− hunreify
145− SExpr ->
146− AHThese .
147− bimap (fromColumns . hreify) (fromColumns . hreify) .
148− fromColumns .
149− hunreify
150− SResult ->
151− AHThese .
152− bimap (fromColumns . hreify) (fromColumns . hreify) .
153− fromColumns .
154− hunreify
155− SName ->
156− AHThese .
157− bimap (fromColumns . hreify) (fromColumns . hreify) .
158− fromColumns .
159− hunreify
160− SReify context ->
161− AHThese .
162− sbimapThese context (fromColumns . hreify) (fromColumns . hreify) .
163− sfromColumnsThese context .
164− hunreify
165−
166−
167−stoColumnsThese :: (Table (Reify context) a, Table (Reify context) b)
168− => SContext context
169− -> AHThese context a b
170− -> HTheseTable (Columns a) (Columns b) (Col (Reify context))
171−stoColumnsThese = \case
172− SAggregate ->
173− hreify .
174− toColumns .
175− bimap (hunreify . toColumns) (hunreify . toColumns) .
176− (\(AHThese a) -> a)
177− SExpr ->
178− hreify .
179− toColumns .
180− bimap (hunreify . toColumns) (hunreify . toColumns) .
181− (\(AHThese a) -> a)
182− SResult ->
183− hreify .
184− toColumns .
185− bimap (hunreify . toColumns) (hunreify . toColumns) .
186− (\(AHThese a) -> a)
187− SName ->
188− hreify .
189− toColumns .
190− bimap (hunreify . toColumns) (hunreify . toColumns) .
191− (\(AHThese a) -> a)
192− SReify context ->
193− hreify .
194− stoColumnsThese context .
195− sbimapThese context (hunreify . toColumns) (hunreify . toColumns) .
196− (\(AHThese a) -> a)
src/Rel8/Expr.hs+5−14
@@ -20,7 +20,6 @@ module Rel8.Expr
2020where
2121
2222-- base
23−import Data.Functor.Identity ( Identity )
2423import Data.Kind ( Type )
2524import Data.String ( IsString, fromString )
2625import Prelude hiding ( null )
@@ -41,12 +40,11 @@ import Rel8.Expr.Serialize ( litExpr )
4140import Rel8.Schema.Context ( Interpretation, Col )
4241import Rel8.Schema.HTable.Identity ( HIdentity( HType ), HType )
4342import Rel8.Schema.Null ( Nullity( Null, NotNull ), Sql, nullable )
44−import Rel8.Schema.Reify ( notReify )
45−import Rel8.Schema.Result ( Result )
43+import Rel8.Schema.Result ( Col( R ) )
4644import Rel8.Schema.Spec ( Spec( Spec ) )
4745import Rel8.Table
4846 ( Table, Columns, Context, fromColumns, toColumns
49− , reify, unreify, coherence, congruence
47+ , FromExprs, fromResult, toResult
5048 )
5149import Rel8.Table.Recontextualize ( Recontextualize )
5250import Rel8.Type ( DBType )
@@ -134,19 +132,12 @@ instance Interpretation Expr where
134132instance Sql DBType a => Table Expr (Expr a) where
135133 type Columns (Expr a) = HType a
136134 type Context (Expr a) = Expr
135+ type FromExprs (Expr a) = a
137136
138137 toColumns a = HType (E a)
139138 fromColumns (HType (E a)) = a
140− reify = notReify
141− unreify = notReify
142− coherence = notReify
143− congruence = notReify
139+ toResult a = HType (R a)
140+ fromResult (HType (R a)) = a
144141
145142
146143instance Sql DBType a => Recontextualize Expr Expr (Expr a) (Expr a)
147−
148−
149−instance Sql DBType a => Recontextualize Expr Result (Expr a) (Identity a)
150−
151−
152−instance Sql DBType a => Recontextualize Result Expr (Identity a) (Expr a)
src/Rel8/Expr/Eq.hs+1−1
@@ -22,7 +22,7 @@ import Prelude
2222import qualified Opaleye.Internal.HaskellDB.PrimQuery as Opaleye
2323
2424-- rel8
25−import {-# SOURCE #-} Rel8.Expr ( Expr )
25+import Rel8.Expr ( Expr )
2626import Rel8.Expr.Bool ( (&&.), (||.), false, or_, coalesce )
2727import Rel8.Expr.Null ( isNull, unsafeLiftOpNull )
2828import Rel8.Expr.Opaleye ( fromPrimExpr, toPrimExpr, zipPrimExprsWith )
src/Rel8/FCF.hs+3−3
@@ -5,7 +5,7 @@
55
66module Rel8.FCF
77 ( Exp, Eval
8− , Compose
8+ , Id
99 )
1010where
1111
@@ -22,5 +22,5 @@ type Eval :: Exp e -> e
2222type family Eval a
2323
2424
25−data Compose :: (Type -> Type) -> (Type -> Exp Type) -> Type -> Exp Type
26−type instance Eval (Compose f g a) = f (Eval (g a))
25+data Id :: a -> Exp a
26+type instance Eval (Id a) = a
src/Rel8/Generic/Coherence.hsdeleted−79
@@ -1,79 +0,0 @@
1−{-# language AllowAmbiguousTypes #-}
2−{-# language DataKinds #-}
3−{-# language FlexibleInstances #-}
4−{-# language MultiParamTypeClasses #-}
5−{-# language PolyKinds #-}
6−{-# language RankNTypes #-}
7−{-# language ScopedTypeVariables #-}
8−{-# language StandaloneKindSignatures #-}
9−{-# language TypeApplications #-}
10−{-# language TypeFamilies #-}
11−{-# language TypeOperators #-}
12−{-# language UndecidableInstances #-}
13−
14−module Rel8.Generic.Coherence
15− ( GCoherent
16− , gcoherence
17− , gcongruence
18− )
19−where
20−
21−-- base
22−import Control.Category ( id )
23−import Data.Kind ( Constraint, Type )
24−import Data.Proxy ( Proxy( Proxy ) )
25−import Data.Type.Equality ( (:~:), apply )
26−import GHC.Generics ( (:*:), K1, M1, Meta( MetaSel ), C, D, S )
27−import Prelude hiding ( id )
28−
29−-- rel8
30−import Rel8.FCF ( Eval, Exp )
31−import Rel8.Generic.Map ( GMap )
32−import Rel8.Generic.Table.Record ( GColumns, GContext )
33−
34−
35−type GCoherent :: (Type -> Exp Constraint) -> (Type -> Type) -> Constraint
36−class GCoherent _Table rep where
37− gcoherence :: ()
38− => proxy _Context
39− -> proxy' f
40− -> (forall a proxy_. Eval (_Table a)
41− => proxy_ a -> Eval (_Context (Eval (f a))) :~: context)
42− -> GContext _Context (GMap f rep) :~: context
43−
44− gcongruence :: ()
45− => proxy _Columns
46− -> proxy' f
47− -> (forall a proxy_. Eval (_Table a)
48− => proxy_ a -> Eval (_Columns a) :~: Eval (_Columns (Eval (f a))))
49− -> GColumns _Columns rep :~: GColumns _Columns (GMap f rep)
50−
51−
52−instance GCoherent _Table rep => GCoherent _Table (M1 D c rep) where
53− gcoherence = gcoherence @_Table @rep
54− gcongruence = gcongruence @_Table @rep
55−
56−
57−instance GCoherent _Table rep => GCoherent _Table (M1 C c rep) where
58− gcoherence = gcoherence @_Table @rep
59− gcongruence = gcongruence @_Table @rep
60−
61−
62−instance (GCoherent _Table rep1, GCoherent _Table rep2) =>
63− GCoherent _Table (rep1 :*: rep2)
64− where
65− gcoherence = gcoherence @_Table @rep1
66− gcongruence _Columns f proof = id `apply`
67− gcongruence @_Table @rep1 _Columns f proof `apply`
68− gcongruence @_Table @rep2 _Columns f proof
69−
70−
71−instance
72− ( Eval (_Table a)
73− , meta ~ 'MetaSel ('Just _l) _su _ss _ds
74− , k1 ~ K1 i a
75− )
76− => GCoherent _Table (M1 S meta k1)
77− where
78− gcoherence _ _ proof = proof (Proxy @a)
79− gcongruence _ _ proof = id `apply` proof (Proxy @a)
src/Rel8/Generic/Construction.hs+136−154
@@ -2,8 +2,6 @@
22{-# language ConstraintKinds #-}
33{-# language DataKinds #-}
44{-# language FlexibleContexts #-}
5−{-# language FlexibleInstances #-}
6−{-# language MultiParamTypeClasses #-}
75{-# language NamedFieldPuns #-}
86{-# language ScopedTypeVariables #-}
97{-# language StandaloneKindSignatures #-}
@@ -27,7 +25,6 @@ where
2725import Data.Bifunctor ( first )
2826import Data.Kind ( Constraint, Type )
2927import Data.List.NonEmpty ( NonEmpty( (:|) ) )
30−import Data.Type.Equality ( (:~:)( Refl ) )
3128import GHC.TypeLits ( Symbol )
3229import Prelude
3330
@@ -38,7 +35,7 @@ import Rel8.Expr.Aggregate ( groupByExpr )
3835import Rel8.Expr.Eq ( (==.) )
3936import Rel8.Expr.Null ( nullify, snull, unsafeUnnullify )
4037import Rel8.Expr.Serialize ( litExpr )
41−import Rel8.FCF ( Eval, Exp )
38+import Rel8.FCF ( Eval, Exp, Id )
4239import Rel8.Generic.Construction.ADT
4340 ( GConstructorADT, GMakeableADT, gmakeADT
4441 , GConstructableADT
@@ -65,11 +62,9 @@ import qualified Rel8.Schema.Kind as K
6562import Rel8.Schema.Name ( Col( N ), Name( Name ) )
6663import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
6764import Rel8.Schema.Spec ( SSpec( SSpec, nullity, info ) )
68−import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify )
69−import Rel8.Schema.Result ( Result )
7065import Rel8.Table
71− ( TTable, TColumns, TUnreify
72− , Table, fromColumns, toColumns, reify, unreify
66+ ( TTable, TColumns
67+ , Table, fromColumns, toColumns
7368 )
7469import Rel8.Table.Bool ( case_ )
7570import Rel8.Type.Tag ( Tag )
@@ -78,10 +73,10 @@ import Rel8.Type.Tag ( Tag )
7873type GGBuildable :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Constraint
7974type GGBuildable algebra name rep =
8075 ( KnownAlgebra algebra
81− , Eval (GGColumns algebra TColumns (Eval (rep (Reify Aggregate)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
82− , Eval (GGColumns algebra TColumns (Eval (rep (Reify Expr)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
83− , Eval (GGColumns algebra TColumns (Eval (rep (Reify Name)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
84− , HTable (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))))
76+ , Eval (GGColumns algebra TColumns (Eval (rep Aggregate))) ~ Eval (GGColumns algebra TColumns (Eval (rep Expr)))
77+ , Eval (GGColumns algebra TColumns (Eval (rep Expr))) ~ Eval (GGColumns algebra TColumns (Eval (rep Expr)))
78+ , Eval (GGColumns algebra TColumns (Eval (rep Name))) ~ Eval (GGColumns algebra TColumns (Eval (rep Expr)))
79+ , HTable (Eval (GGColumns algebra TColumns (Eval (rep Expr))))
8580 , GGBuildable' algebra name rep
8681 )
8782
@@ -89,65 +84,63 @@ type GGBuildable algebra name rep =
8984type GGBuildable' :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Constraint
9085type family GGBuildable' algebra name rep where
9186 GGBuildable' 'K.Product name rep =
92− ( name ~ GConstructor (Eval (rep (Reify Expr)))
93− , Representable TUnreify (Eval (rep (Reify Expr)))
94− , GConstructable (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (Eval (rep (Reify Expr)))
87+ ( name ~ GConstructor (Eval (rep Expr))
88+ , Representable Id (Eval (rep Expr))
89+ , GConstructable (TTable Expr) TColumns Id (Col Expr) (Eval (rep Expr))
9590 )
9691 GGBuildable' 'K.Sum name rep =
97− ( Representable TUnreify (GConstructorADT name (Eval (rep (Reify Expr))))
98− , GMakeableADT (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) name (Eval (rep (Reify Expr)))
92+ ( Representable Id (GConstructorADT name (Eval (rep Expr)))
93+ , GMakeableADT (TTable Expr) TColumns Id (Col Expr) name (Eval (rep Expr))
9994 )
10095
10196
10297type GGBuild :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
10398type family GGBuild algebra name rep r where
10499 GGBuild 'K.Product _name rep r =
105− GConstruct TUnreify (Eval (rep (Reify Expr))) r
100+ GConstruct Id (Eval (rep Expr)) r
106101 GGBuild 'K.Sum name rep r =
107− GConstruct TUnreify (GConstructorADT name (Eval (rep (Reify Expr)))) r
102+ GConstruct Id (GConstructorADT name (Eval (rep Expr))) r
108103
109104
110105ggbuild :: forall algebra name rep a. GGBuildable algebra name rep
111− => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr) -> a)
106+ => (Eval (GGColumns algebra TColumns (Eval (rep Expr))) (Col Expr) -> a)
112107 -> GGBuild algebra name rep a
113108ggbuild gfromColumns = case algebraSing @algebra of
114109 SProduct ->
115− gtabulate @TUnreify @(Eval (rep (Reify Expr))) @a $
110+ gtabulate @Id @(Eval (rep Expr)) @a $
116111 gfromColumns .
117− hunreify .
118112 gconstruct
119− @(TTable (Reify Expr))
113+ @(TTable Expr)
120114 @TColumns
121− @TUnreify
122− @(Col (Reify Expr))
123− @(Eval (rep (Reify Expr)))
124− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
115+ @Id
116+ @(Col Expr)
117+ @(Eval (rep Expr))
118+ (const toColumns)
125119 SSum ->
126− gtabulate @TUnreify @(GConstructorADT name (Eval (rep (Reify Expr)))) @a $
120+ gtabulate @Id @(GConstructorADT name (Eval (rep Expr))) @a $
127121 gfromColumns .
128− hunreify .
129122 gmakeADT
130− @(TTable (Reify Expr))
123+ @(TTable Expr)
131124 @TColumns
132− @TUnreify
133− @(Col (Reify Expr))
125+ @Id
126+ @(Col Expr)
134127 @name
135− @(Eval (rep (Reify Expr)))
136− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
137− (\SSpec {info} -> Reify (E (snull info)))
128+ @(Eval (rep Expr))
129+ (const toColumns)
130+ (\SSpec {info} -> E (snull info))
138131 (\SSpec {nullity} -> case nullity of
139132 Null -> id
140− NotNull -> \(Reify (E a)) -> Reify (E (nullify a)))
141− (HType . Reify . E . litExpr)
133+ NotNull -> \(E a) -> E (nullify a))
134+ (HType . E . litExpr)
142135
143136
144137type GGConstructable :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
145138type GGConstructable algebra rep =
146139 ( KnownAlgebra algebra
147− , Eval (GGColumns algebra TColumns (Eval (rep (Reify Aggregate)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
148− , Eval (GGColumns algebra TColumns (Eval (rep (Reify Expr)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
149− , Eval (GGColumns algebra TColumns (Eval (rep (Reify Name)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
150− , HTable (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))))
140+ , Eval (GGColumns algebra TColumns (Eval (rep Aggregate))) ~ Eval (GGColumns algebra TColumns (Eval (rep Expr)))
141+ , Eval (GGColumns algebra TColumns (Eval (rep Expr))) ~ Eval (GGColumns algebra TColumns (Eval (rep Expr)))
142+ , Eval (GGColumns algebra TColumns (Eval (rep Name))) ~ Eval (GGColumns algebra TColumns (Eval (rep Expr)))
143+ , HTable (Eval (GGColumns algebra TColumns (Eval (rep Expr))))
151144 , GGConstructable' algebra rep
152145 )
153146
@@ -155,105 +148,100 @@ type GGConstructable algebra rep =
155148type GGConstructable' :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
156149type family GGConstructable' algebra rep where
157150 GGConstructable' 'K.Product rep =
158− ( Representable TUnreify (Eval (rep (Reify Aggregate)))
159− , Representable TUnreify (Eval (rep (Reify Expr)))
160− , Representable TUnreify (Eval (rep (Reify Name)))
161− , GConstructable (TTable (Reify Aggregate)) TColumns TUnreify (Col (Reify Aggregate)) (Eval (rep (Reify Aggregate)))
162− , GConstructable (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (Eval (rep (Reify Expr)))
163− , GConstructable (TTable (Reify Name)) TColumns TUnreify (Col (Reify Name)) (Eval (rep (Reify Name)))
151+ ( Representable Id (Eval (rep Aggregate))
152+ , Representable Id (Eval (rep Expr))
153+ , Representable Id (Eval (rep Name))
154+ , GConstructable (TTable Aggregate) TColumns Id (Col Aggregate) (Eval (rep Aggregate))
155+ , GConstructable (TTable Expr) TColumns Id (Col Expr) (Eval (rep Expr))
156+ , GConstructable (TTable Name) TColumns Id (Col Name) (Eval (rep Name))
164157 )
165158 GGConstructable' 'K.Sum rep =
166− ( RepresentableConstructors TUnreify (Eval (rep (Reify Expr)))
167− , RepresentableFields TUnreify (Eval (rep (Reify Aggregate)))
168− , RepresentableFields TUnreify (Eval (rep (Reify Expr)))
169− , RepresentableFields TUnreify (Eval (rep (Reify Name)))
170− , Functor (GConstructors TUnreify (Eval (rep (Reify Expr))))
171− , GConstructableADT (TTable (Reify Aggregate)) TColumns TUnreify (Col (Reify Aggregate)) (Eval (rep (Reify Aggregate)))
172− , GConstructableADT (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (Eval (rep (Reify Expr)))
173− , GConstructableADT (TTable (Reify Name)) TColumns TUnreify (Col (Reify Name)) (Eval (rep (Reify Name)))
159+ ( RepresentableConstructors Id (Eval (rep Expr))
160+ , RepresentableFields Id (Eval (rep Aggregate))
161+ , RepresentableFields Id (Eval (rep Expr))
162+ , RepresentableFields Id (Eval (rep Name))
163+ , Functor (GConstructors Id (Eval (rep Expr)))
164+ , GConstructableADT (TTable Aggregate) TColumns Id (Col Aggregate) (Eval (rep Aggregate))
165+ , GConstructableADT (TTable Expr) TColumns Id (Col Expr) (Eval (rep Expr))
166+ , GConstructableADT (TTable Name) TColumns Id (Col Name) (Eval (rep Name))
174167 )
175168
176169
177170type GGConstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
178171type family GGConstruct algebra rep r where
179− GGConstruct 'K.Product rep r =
180− GConstruct TUnreify (Eval (rep (Reify Expr))) r -> r
181− GGConstruct 'K.Sum rep r =
182− GConstructADT TUnreify (Eval (rep (Reify Expr))) r r
172+ GGConstruct 'K.Product rep r = GConstruct Id (Eval (rep Expr)) r -> r
173+ GGConstruct 'K.Sum rep r = GConstructADT Id (Eval (rep Expr)) r r
183174
184175
185176ggconstruct :: forall algebra rep a. GGConstructable algebra rep
186− => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr) -> a)
177+ => (Eval (GGColumns algebra TColumns (Eval (rep Expr))) (Col Expr) -> a)
187178 -> GGConstruct algebra rep a -> a
188179ggconstruct gfromColumns f = case algebraSing @algebra of
189180 SProduct ->
190181 f $
191− gtabulate @TUnreify @(Eval (rep (Reify Expr))) @a $
182+ gtabulate @Id @(Eval (rep Expr)) @a $
192183 gfromColumns .
193− hunreify .
194184 gconstruct
195− @(TTable (Reify Expr))
185+ @(TTable Expr)
196186 @TColumns
197− @TUnreify
198− @(Col (Reify Expr))
199− @(Eval (rep (Reify Expr)))
200− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
187+ @Id
188+ @(Col Expr)
189+ @(Eval (rep Expr))
190+ (const toColumns)
201191 SSum ->
202− gcindex @TUnreify @(Eval (rep (Reify Expr))) @a f $
203− fmap (gfromColumns . hunreify) $
192+ gcindex @Id @(Eval (rep Expr)) @a f $
193+ fmap gfromColumns $
204194 gconstructADT
205− @(TTable (Reify Expr))
195+ @(TTable Expr)
206196 @TColumns
207− @TUnreify
208− @(Col (Reify Expr))
209− @(Eval (rep (Reify Expr)))
210− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
211− (\SSpec {info} -> Reify (E (snull info)))
197+ @Id
198+ @(Col Expr)
199+ @(Eval (rep Expr))
200+ (const toColumns)
201+ (\SSpec {info} -> E (snull info))
212202 (\SSpec {nullity} -> case nullity of
213203 Null -> id
214− NotNull -> \(Reify (E a)) -> Reify (E (nullify a)))
215− (HType . Reify . E . litExpr)
204+ NotNull -> \(E a) -> E (nullify a))
205+ (HType . E . litExpr)
216206
217207
218208type GGDeconstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type -> Type
219209type family GGDeconstruct algebra rep a r where
220210 GGDeconstruct 'K.Product rep a r =
221− GConstruct TUnreify (Eval (rep (Reify Expr))) r -> a -> r
211+ GConstruct Id (Eval (rep Expr)) r -> a -> r
222212 GGDeconstruct 'K.Sum rep a r =
223− GConstructADT TUnreify (Eval (rep (Reify Expr))) r (a -> r)
213+ GConstructADT Id (Eval (rep Expr)) r (a -> r)
224214
225215
226216ggdeconstruct :: forall algebra rep a r. (GGConstructable algebra rep, Table Expr r)
227− => (a -> Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr))
217+ => (a -> Eval (GGColumns algebra TColumns (Eval (rep Expr))) (Col Expr))
228218 -> GGDeconstruct algebra rep a r
229219ggdeconstruct gtoColumns = case algebraSing @algebra of
230220 SProduct -> \build ->
231− gindex @TUnreify @(Eval (rep (Reify Expr))) @r build .
221+ gindex @Id @(Eval (rep Expr)) @r build .
232222 gdeconstruct
233− @(TTable (Reify Expr))
223+ @(TTable Expr)
234224 @TColumns
235− @TUnreify
236− @(Col (Reify Expr))
237− @(Eval (rep (Reify Expr)))
238− (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns) .
239− hreify .
225+ @Id
226+ @(Col Expr)
227+ @(Eval (rep Expr))
228+ (const fromColumns) .
240229 gtoColumns
241230 SSum ->
242− gctabulate @TUnreify @(Eval (rep (Reify Expr))) @r @(a -> r) $ \constructors as ->
231+ gctabulate @Id @(Eval (rep Expr)) @r @(a -> r) $ \constructors as ->
243232 let
244− (HType (Reify (E tag)), cases) =
233+ (HType (E tag), cases) =
245234 gdeconstructADT
246− @(TTable (Reify Expr))
235+ @(TTable Expr)
247236 @TColumns
248− @TUnreify
249− @(Col (Reify Expr))
250− @(Eval (rep (Reify Expr)))
251− (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns)
237+ @Id
238+ @(Col Expr)
239+ @(Eval (rep Expr))
240+ (const fromColumns)
252241 (\SSpec {nullity} -> case nullity of
253242 Null -> id
254− NotNull -> \(Reify (E a)) -> Reify (E (unsafeUnnullify a)))
243+ NotNull -> \(E a) -> E (unsafeUnnullify a))
255244 constructors $
256− hreify $
257245 gtoColumns as
258246 in
259247 case cases of
@@ -263,108 +251,102 @@ ggdeconstruct gtoColumns = case algebraSing @algebra of
263251
264252type GGName :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
265253type family GGName algebra rep a where
266− GGName 'K.Product rep a = GConstruct TUnreify (Eval (rep (Reify Name))) a
267− GGName 'K.Sum rep a = Name Tag -> GBuildADT TUnreify (Eval (rep (Reify Name))) a
254+ GGName 'K.Product rep a = GConstruct Id (Eval (rep Name)) a
255+ GGName 'K.Sum rep a = Name Tag -> GBuildADT Id (Eval (rep Name)) a
268256
269257
270258ggname :: forall algebra rep a. GGConstructable algebra rep
271− => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Name) -> a)
259+ => (Eval (GGColumns algebra TColumns (Eval (rep Expr))) (Col Name) -> a)
272260 -> GGName algebra rep a
273261ggname gfromColumns = case algebraSing @algebra of
274262 SProduct ->
275− gtabulate @TUnreify @(Eval (rep (Reify Name))) @a $
263+ gtabulate @Id @(Eval (rep Name)) @a $
276264 gfromColumns .
277− hunreify .
278265 gconstruct
279− @(TTable (Reify Name))
266+ @(TTable Name)
280267 @TColumns
281− @TUnreify
282− @(Col (Reify Name))
283− @(Eval (rep (Reify Name)))
284− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
268+ @Id
269+ @(Col Name)
270+ @(Eval (rep Name))
271+ (const toColumns)
285272 SSum -> \tag ->
286− gftabulate @TUnreify @(Eval (rep (Reify Name))) @a $
273+ gftabulate @Id @(Eval (rep Name)) @a $
287274 gfromColumns .
288− hunreify .
289275 gbuildADT
290− @(TTable (Reify Name))
276+ @(TTable Name)
291277 @TColumns
292− @TUnreify
293− @(Col (Reify Name))
294− @(Eval (rep (Reify Name)))
295− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
296− (\_ _ (Reify (N (Name a))) -> Reify (N (Name a)))
297− (HType (Reify (N tag)))
278+ @Id
279+ @(Col Name)
280+ @(Eval (rep Name))
281+ (const toColumns)
282+ (\_ _ (N (Name a)) -> N (Name a))
283+ (HType (N tag))
298284
299285
300286type GGAggregate :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
301287type family GGAggregate algebra rep r where
302288 GGAggregate 'K.Product rep r =
303− GConstruct TUnreify (Eval (rep (Reify Aggregate))) r ->
304− GConstruct TUnreify (Eval (rep (Reify Expr))) r
289+ GConstruct Id (Eval (rep Aggregate)) r ->
290+ GConstruct Id (Eval (rep Expr)) r
305291 GGAggregate 'K.Sum rep r =
306− GBuildADT TUnreify (Eval (rep (Reify Aggregate))) r ->
307− GBuildADT TUnreify (Eval (rep (Reify Expr))) r
292+ GBuildADT Id (Eval (rep Aggregate)) r ->
293+ GBuildADT Id (Eval (rep Expr)) r
308294
309295
310296ggaggregate :: forall algebra rep exprs agg. GGConstructable algebra rep
311− => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Aggregate) -> agg)
312− -> (exprs -> Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr))
297+ => (Eval (GGColumns algebra TColumns (Eval (rep Expr))) (Col Aggregate) -> agg)
298+ -> (exprs -> Eval (GGColumns algebra TColumns (Eval (rep Expr))) (Col Expr))
313299 -> GGAggregate algebra rep agg -> exprs -> agg
314300ggaggregate gfromColumns gtoColumns agg es = case algebraSing @algebra of
315301 SProduct -> flip f exprs $
316302 gfromColumns .
317− hunreify .
318303 gconstruct
319− @(TTable (Reify Aggregate))
304+ @(TTable Aggregate)
320305 @TColumns
321− @TUnreify
322− @(Col (Reify Aggregate))
323− @(Eval (rep (Reify Aggregate)))
324− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
306+ @Id
307+ @(Col Aggregate)
308+ @(Eval (rep Aggregate))
309+ (const toColumns)
325310 where
326311 f =
327− gindex @TUnreify @(Eval (rep (Reify Expr))) @agg .
312+ gindex @Id @(Eval (rep Expr)) @agg .
328313 agg .
329− gtabulate @TUnreify @(Eval (rep (Reify Aggregate))) @agg
314+ gtabulate @Id @(Eval (rep Aggregate)) @agg
330315 exprs =
331316 gdeconstruct
332− @(TTable (Reify Expr))
317+ @(TTable Expr)
333318 @TColumns
334− @TUnreify
335− @(Col (Reify Expr))
336− @(Eval (rep (Reify Expr)))
337− (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns) $
338− hreify $
319+ @Id
320+ @(Col Expr)
321+ @(Eval (rep Expr))
322+ (const fromColumns) $
339323 gtoColumns es
340324 SSum -> flip f exprs $
341325 gfromColumns .
342− hunreify .
343326 gbuildADT
344− @(TTable (Reify Aggregate))
327+ @(TTable Aggregate)
345328 @TColumns
346− @TUnreify
347− @(Col (Reify Aggregate))
348− @(Eval (rep (Reify Aggregate)))
349− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
350− (\tag' SSpec {nullity} (Reify (A (Aggregate a))) ->
351− Reify $ A $ Aggregate $ sguard (tag ==. litExpr tag') . snullify nullity <$> a)
352− (HType (Reify (A (groupByExpr tag))))
329+ @Id
330+ @(Col Aggregate)
331+ @(Eval (rep Aggregate))
332+ (const toColumns)
333+ (\tag' SSpec {nullity} (A (Aggregate a)) ->
334+ A $ Aggregate $ sguard (tag ==. litExpr tag') . snullify nullity <$> a)
335+ (HType (A (groupByExpr tag)))
353336 where
354337 f =
355− gfindex @TUnreify @(Eval (rep (Reify Expr))) @agg .
338+ gfindex @Id @(Eval (rep Expr)) @agg .
356339 agg .
357− gftabulate @TUnreify @(Eval (rep (Reify Aggregate))) @agg
358− (HType (Reify (E tag)), exprs) =
340+ gftabulate @Id @(Eval (rep Aggregate)) @agg
341+ (HType (E tag), exprs) =
359342 gunbuildADT
360− @(TTable (Reify Expr))
343+ @(TTable Expr)
361344 @TColumns
362− @TUnreify
363− @(Col (Reify Expr))
364− @(Eval (rep (Reify Expr)))
365− (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns)
345+ @Id
346+ @(Col Expr)
347+ @(Eval (rep Expr))
348+ (const fromColumns)
366349 (\SSpec {nullity} -> case nullity of
367350 Null -> id
368− NotNull -> \(Reify (E a)) -> Reify (E (unsafeUnnullify a))) $
369− hreify $
351+ NotNull -> \(E a) -> E (unsafeUnnullify a)) $
370352 gtoColumns es
src/Rel8/Generic/Map.hs+3−67
@@ -1,26 +1,17 @@
1−{-# language AllowAmbiguousTypes #-}
21{-# language DataKinds #-}
3−{-# language EmptyCase #-}
4−{-# language FlexibleInstances #-}
5−{-# language LambdaCase #-}
6−{-# language MultiParamTypeClasses #-}
7−{-# language RankNTypes #-}
8−{-# language ScopedTypeVariables #-}
92{-# language StandaloneKindSignatures #-}
10−{-# language TypeApplications #-}
113{-# language TypeFamilies #-}
124{-# language TypeOperators #-}
13−{-# language UndecidableInstances #-}
145
156module Rel8.Generic.Map
16− ( GMap, GMappable (gmap, gunmap)
7+ ( GMap
178 )
189where
1910
2011-- base
21−import Data.Kind ( Constraint, Type )
12+import Data.Kind ( Type )
2213import GHC.Generics
23− ( (:+:)( L1, R1 ), (:*:)( (:*:) ), K1( K1 ), M1( M1 ), U1( U1 ), V1
14+ ( (:+:), (:*:), K1, M1, U1, V1
2415 )
2516import Prelude ()
2617
@@ -36,58 +27,3 @@ type family GMap f rep where
3627 GMap _ U1 = U1
3728 GMap f (rep1 :*: rep2) = GMap f rep1 :*: GMap f rep2
3829 GMap f (K1 i a) = K1 i (Eval (f a))
39−
40−
41−type GMappable :: (Type -> Exp Constraint) -> (Type -> Type) -> Constraint
42−class GMappable constraint rep where
43− gmap :: ()
44− => proxy f
45− -> (forall a. Eval (constraint a) => a -> Eval (f a))
46− -> rep x
47− -> GMap f rep x
48−
49− gunmap :: ()
50− => proxy f
51− -> (forall a. Eval (constraint a) => Eval (f a) -> a)
52− -> GMap f rep x
53− -> rep x
54−
55−
56−instance GMappable constraint rep => GMappable constraint (M1 i c rep) where
57− gmap proxy f (M1 a) = M1 (gmap @constraint proxy f a)
58− gunmap proxy f (M1 a) = M1 (gunmap @constraint proxy f a)
59−
60−
61−instance GMappable constraint V1 where
62− gmap _ _ = \case
63− gunmap _ _ = \case
64−
65−
66−instance (GMappable constraint rep1, GMappable constraint rep2) =>
67− GMappable constraint (rep1 :+: rep2)
68− where
69− gmap proxy f = \case
70− L1 a -> L1 (gmap @constraint proxy f a)
71− R1 a -> R1 (gmap @constraint proxy f a)
72− gunmap proxy f = \case
73− L1 a -> L1 (gunmap @constraint proxy f a)
74− R1 a -> R1 (gunmap @constraint proxy f a)
75−
76−
77−instance GMappable constraint U1 where
78− gmap _ _ U1 = U1
79− gunmap _ _ U1 = U1
80−
81−
82−instance (GMappable constraint rep1, GMappable constraint rep2) =>
83− GMappable constraint (rep1 :*: rep2)
84− where
85− gmap proxy f (a :*: b) =
86− gmap @constraint proxy f a :*: gmap @constraint proxy f b
87− gunmap proxy f (a :*: b) =
88− gunmap @constraint proxy f a :*: gunmap @constraint proxy f b
89−
90−
91−instance Eval (constraint a) => GMappable constraint (K1 i a) where
92− gmap _ f (K1 a) = K1 (f a)
93− gunmap _ f (K1 a) = K1 (f a)
src/Rel8/Generic/Reify.hsdeleted−24
@@ -1,24 +0,0 @@
1−{-# language StandaloneKindSignatures #-}
2−{-# language TypeFamilies #-}
3−
4−module Rel8.Generic.Reify
5− ( ARep
6− )
7−where
8−
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/Generic/Rel8able.hs+86−64
@@ -1,9 +1,9 @@
11{-# language AllowAmbiguousTypes #-}
2+{-# language ConstraintKinds #-}
23{-# language DataKinds #-}
34{-# language DefaultSignatures #-}
45{-# language FlexibleContexts #-}
5−{-# language FlexibleInstances #-}
6−{-# language MultiParamTypeClasses #-}
6+{-# language LambdaCase #-}
77{-# language ScopedTypeVariables #-}
88{-# language StandaloneKindSignatures #-}
99{-# language TypeApplications #-}
@@ -15,34 +15,32 @@ module Rel8.Generic.Rel8able
1515 , Algebra
1616 , GRep
1717 , GColumns, gfromColumns, gtoColumns
18− , greify, gunreify
19− , TUnreifyContext
18+ , GFromExprs, gfromResult, gtoResult
2019 )
2120where
2221
2322-- base
2423import Data.Kind ( Constraint, Type )
25−import Data.Proxy ( Proxy( Proxy ) )
26−import Data.Type.Equality ( (:~:)( Refl ) )
2724import GHC.Generics ( Generic, Rep, from, to )
2825import Prelude
2926
3027-- rel8
31−import Rel8.Kind.Context ( Reifiable )
32−import Rel8.FCF ( Eval, Exp )
33−import Rel8.Generic.Map ( GMap, GMappable, gmap, gunmap )
28+import Rel8.Aggregate ( Aggregate )
29+import Rel8.Expr ( Expr )
30+import Rel8.Generic.Map ( GMap )
3431import Rel8.Generic.Record ( Record(..) )
3532import Rel8.Generic.Table ( GAlgebra )
3633import qualified Rel8.Generic.Table.Record as G
3734import qualified Rel8.Kind.Algebra as K ( Algebra(..) )
3835import Rel8.Schema.Context ( Col )
36+import Rel8.Schema.Context.Virtual ( Abstract(..) )
3937import Rel8.Schema.HTable ( HTable )
4038import qualified Rel8.Schema.Kind as K
41−import Rel8.Schema.Reify ( Reify, UnwrapReify )
39+import Rel8.Schema.Name ( Name )
4240import Rel8.Schema.Result ( Result )
4341import Rel8.Table
44− ( fromColumns, toColumns, reify, unreify
45− , TTable, TColumns, TContext, TUnreify
42+ ( fromColumns, toColumns, fromResult, toResult
43+ , TTable, TColumns, TFromExprs
4644 )
4745
4846
@@ -96,79 +94,103 @@ type KRel8able = K.Rel8able
9694type Rel8able :: K.Rel8able -> Constraint
9795class HTable (GColumns t) => Rel8able t where
9896 type GColumns t :: K.HTable
97+ type GFromExprs t :: Type
9998
100− gfromColumns :: Reifiable context
101− => GColumns t (Col (Reify context)) -> t (Reify context)
99+ gfromColumns :: Abstract context -> GColumns t (Col context) -> t context
100+ gtoColumns :: Abstract context -> t context -> GColumns t (Col context)
102101
103− gtoColumns :: Reifiable context
104− => t (Reify context) -> GColumns t (Col (Reify context))
102+ gfromResult :: GColumns t (Col Result) -> GFromExprs t
103+ gtoResult :: GFromExprs t -> GColumns t (Col Result)
105104
106− greify :: Reifiable context
107− => t context -> t (Reify context)
108−
109− gunreify :: Reifiable context
110− => t (Reify context) -> t context
111−
112− type GColumns t = G.GColumns TColumns (GRep t (Reify Result))
105+ type GColumns t = G.GColumns TColumns (GRep t Expr)
106+ type GFromExprs t = t Result
113107
114108 default gfromColumns :: forall context.
115− ( Generic (Record (t (Reify context)))
116− , G.GTable (TTable (Reify context)) TColumns (Col (Reify context)) (GRep t (Reify context))
117− , G.GColumns TColumns (GRep t (Reify context)) ~ GColumns t
109+ ( VRel8able t Aggregate
110+ , VRel8able t Expr
111+ , VRel8able t Name
118112 )
119− => GColumns t (Col (Reify context)) -> t (Reify context)
120− gfromColumns =
121− unrecord .
122− to .
123− G.gfromColumns @(TTable (Reify context)) @TColumns fromColumns
113+ => Abstract context -> GColumns t (Col context) -> t context
114+ gfromColumns = \case
115+ VAggregate -> vfromColumns
116+ VExpr -> vfromColumns
117+ VName -> vfromColumns
124118
125119 default gtoColumns :: forall context.
126− ( Generic (Record (t (Reify context)))
127− , G.GTable (TTable (Reify context)) TColumns (Col (Reify context)) (GRep t (Reify context))
128− , G.GColumns TColumns (GRep t (Reify context)) ~ GColumns t
120+ ( VRel8able t Aggregate
121+ , VRel8able t Expr
122+ , VRel8able t Name
129123 )
130− => t (Reify context) -> GColumns t (Col (Reify context))
131− gtoColumns =
132− G.gtoColumns @(TTable (Reify context)) @TColumns toColumns .
133− from .
134− Record
135−
136− default greify :: forall context.
137− ( Generic (Record (t context))
138− , Generic (Record (t (Reify context)))
139− , GMappable (TTable (Reify context)) (GRep t (Reify context))
140− , GRep t context ~ GMap TUnreify (GRep t (Reify context))
124+ => Abstract context -> t context -> GColumns t (Col context)
125+ gtoColumns = \case
126+ VAggregate -> vtoColumns
127+ VExpr -> vtoColumns
128+ VName -> vtoColumns
129+
130+ default gfromResult ::
131+ ( Generic (Record (t Result))
132+ , G.GTable (TTable Expr) TColumns TFromExprs (GRep t Expr)
133+ , G.GColumns TColumns (GRep t Expr) ~ GColumns t
134+ , Rep (Record (t Result)) ~ GMap TFromExprs (GRep t Expr)
135+ , GFromExprs t ~ t Result
141136 )
142− => t context -> t (Reify context)
143− greify =
137+ => GColumns t (Col Result) -> GFromExprs t
138+ gfromResult =
144139 unrecord .
145140 to .
146− gunmap @(TTable (Reify context)) (Proxy @TUnreify) (reify Refl) .
147− from .
148− Record
149−
150− default gunreify :: forall context.
151− ( Generic (Record (t context))
152− , Generic (Record (t (Reify context)))
153− , GMappable (TTable (Reify context)) (GRep t (Reify context))
154− , GRep t context ~ GMap TUnreify (GRep t (Reify context))
141+ G.gfromResult
142+ @(TTable Expr)
143+ @TColumns
144+ @TFromExprs
145+ @(GRep t Expr)
146+ (\(_ :: proxy x) -> fromResult @Expr @x)
147+
148+ default gtoResult ::
149+ ( Generic (Record (t Result))
150+ , G.GTable (TTable Expr) TColumns TFromExprs (GRep t Expr)
151+ , G.GColumns TColumns (GRep t Expr) ~ GColumns t
152+ , Rep (Record (t Result)) ~ GMap TFromExprs (GRep t Expr)
153+ , GFromExprs t ~ t Result
155154 )
156− => t (Reify context) -> t context
157− gunreify =
158− unrecord .
159− to .
160− gmap @(TTable (Reify context)) (Proxy @TUnreify) (unreify Refl) .
155+ => GFromExprs t -> GColumns t (Col Result)
156+ gtoResult =
157+ G.gtoResult
158+ @(TTable Expr)
159+ @TColumns
160+ @TFromExprs
161+ @(GRep t Expr)
162+ (\(_ :: proxy x) -> toResult @Expr @x) .
161163 from .
162164 Record
163165
164166
165167type Algebra :: K.Rel8able -> K.Algebra
166−type Algebra t = GAlgebra (GRep t (Reify Result))
168+type Algebra t = GAlgebra (GRep t Expr)
167169
168170
169171type GRep :: K.Rel8able -> K.Context -> Type -> Type
170172type GRep t context = Rep (Record (t context))
171173
172174
173−data TUnreifyContext :: Type -> Exp K.Context
174−type instance Eval (TUnreifyContext a) = UnwrapReify (Eval (TContext a))
175+type VRel8able :: K.Rel8able -> K.Context -> Constraint
176+type VRel8able t context =
177+ ( Generic (Record (t context))
178+ , G.GTable (TTable context) TColumns TFromExprs (GRep t context)
179+ , G.GColumns TColumns (GRep t context) ~ GColumns t
180+ )
181+
182+
183+vfromColumns :: forall t context. VRel8able t context
184+ => GColumns t (Col context) -> t context
185+vfromColumns =
186+ unrecord .
187+ to .
188+ G.gfromColumns @(TTable context) @TColumns @TFromExprs fromColumns
189+
190+
191+vtoColumns :: forall t context. VRel8able t context
192+ => t context -> GColumns t (Col context)
193+vtoColumns =
194+ G.gtoColumns @(TTable context) @TColumns @TFromExprs toColumns .
195+ from .
196+ Record
src/Rel8/Generic/Table.hs+25−108
@@ -12,8 +12,7 @@
1212{-# language UndecidableInstances #-}
1313
1414module Rel8.Generic.Table
15− ( GGTable, GGColumns, GGContext, ggfromColumns, ggtoColumns, ggtable
16− , GGToExprs, ggfromResult, ggtoResult
15+ ( GGTable, GGColumns, ggfromResult, ggtoResult
1716 , GAlgebra
1817 )
1918where
@@ -25,14 +24,11 @@ import Prelude ()
2524
2625-- rel8
2726import Rel8.FCF ( Eval, Exp )
27+import Rel8.Generic.Map ( GMap )
2828import Rel8.Generic.Table.ADT
29− ( GTableADT, GColumnsADT, gfromColumnsADT, gtoColumnsADT, gtableADT
30− , GToExprsADT, gtoResultADT, gfromResultADT
31− )
32−import Rel8.Generic.Table.Record
33− ( GTable, GColumns, GContext, gfromColumns, gtoColumns, gtable
34− , GToExprs, gtoResult, gfromResult
29+ ( GTableADT, GColumnsADT, gtoResultADT, gfromResultADT
3530 )
31+import Rel8.Generic.Table.Record ( GTable, GColumns, gtoResult, gfromResult )
3632import Rel8.Kind.Algebra
3733 ( Algebra( Product, Sum )
3834 , SAlgebra( SProduct, SSum )
@@ -40,8 +36,6 @@ import Rel8.Kind.Algebra
4036 )
4137import Rel8.Schema.Context ( Col )
4238import qualified Rel8.Schema.Kind as K
43−import Rel8.Schema.Null ( Nullify )
44−import Rel8.Schema.Spec ( Spec( Spec ), SSpec )
4539import Rel8.Schema.Result ( Result )
4640
4741
@@ -49,34 +43,17 @@ data GGTable
4943 :: Algebra
5044 -> (Type -> Exp Constraint)
5145 -> (Type -> Exp K.HTable)
52− -> K.HContext
46+ -> (Type -> Exp Type)
5347 -> (Type -> Type)
5448 -> Exp Constraint
5549
5650
57−type instance Eval (GGTable 'Product _Table _Columns context rep) =
58− GTable _Table _Columns context rep
59−
51+type instance Eval (GGTable 'Product _Table _Columns _FromExprs rep) =
52+ GTable _Table _Columns _FromExprs rep
6053
61−type instance Eval (GGTable 'Sum _Table _Columns context rep) =
62− GTableADT _Table _Columns context rep
6354
64−
65−data GGToExprs
66− :: Algebra
67− -> (Type -> Type -> Exp Constraint)
68− -> (Type -> Exp K.HTable)
69− -> (Type -> Type)
70− -> (Type -> Type)
71− -> Exp Constraint
72−
73−
74−type instance Eval (GGToExprs 'Product _ToExprs _Columns exprs rep) =
75− GToExprs _ToExprs _Columns exprs rep
76−
77−
78−type instance Eval (GGToExprs 'Sum _ToExprs _Columns exprs rep) =
79− GToExprsADT _ToExprs _Columns exprs rep
55+type instance Eval (GGTable 'Sum _Table _Columns _FromExprs rep) =
56+ GTableADT _Table _Columns _FromExprs rep
8057
8158
8259data GGColumns
@@ -92,19 +69,6 @@ type instance Eval (GGColumns 'Product _Columns rep) = GColumns _Columns rep
9269type instance Eval (GGColumns 'Sum _Columns rep) = GColumnsADT _Columns rep
9370
9471
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−
10872type GAlgebra :: (Type -> Type) -> Algebra
10973type family GAlgebra rep where
11074 GAlgebra (M1 _ _ rep) = GAlgebra rep
@@ -115,74 +79,27 @@ type family GAlgebra rep where
11579 GAlgebra (K1 _ _) = 'Product
11680
11781
118−ggfromColumns :: forall algebra _Table _Columns rep context x.
119− ( KnownAlgebra algebra
120− , Eval (GGTable algebra _Table _Columns context rep)
121− )
122− => (forall spec. algebra ~ 'Sum => context spec -> Col Result spec)
123− -> (forall spec. algebra ~ 'Sum => Col Result 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 f g h x = case algebraSing @algebra of
128− SProduct -> gfromColumns @_Table @_Columns h x
129− SSum -> gfromColumnsADT @_Table @_Columns f g h x
130−
131−
132−ggtoColumns :: forall algebra _Table _Columns rep context x.
133− ( KnownAlgebra algebra
134− , Eval (GGTable algebra _Table _Columns context rep)
135− )
136− => (forall spec. algebra ~ 'Sum => context spec -> Col Result spec)
137− -> (forall spec. algebra ~ 'Sum => Col Result spec -> context spec)
138− -> (forall a. Eval (_Table a) => a -> Eval (_Columns a) context)
139− -> rep x
140− -> Eval (GGColumns algebra _Columns rep) context
141−ggtoColumns f g h x = case algebraSing @algebra of
142− SProduct -> gtoColumns @_Table @_Columns h x
143− SSum -> gtoColumnsADT @_Table @_Columns f g h x
144−
145−
146−ggtable :: forall algebra _Table _Columns rep context.
147− ( KnownAlgebra algebra
148− , Eval (GGTable algebra _Table _Columns context rep)
149− )
150− => (forall a proxy. Eval (_Table a) => proxy a -> Eval (_Columns a) context)
151− -> (forall a. ()
152− => SSpec ('Spec a)
153− -> context ('Spec a)
154− -> context ('Spec (Nullify a)))
155− -> Eval (GGColumns algebra _Columns rep) context
156−ggtable = case algebraSing @algebra of
157− SProduct -> \table _ -> gtable @_Table @_Columns @_ @rep table
158− SSum -> gtableADT @_Table @_Columns @_ @rep
159−
160−
161−ggfromResult :: forall algebra _ToExprs _Columns exprs rep x.
82+ggfromResult :: forall algebra _Table _Columns _FromExprs rep x.
16283 ( KnownAlgebra algebra
163− , Eval (GGToExprs algebra _ToExprs _Columns exprs rep)
84+ , Eval (GGTable algebra _Table _Columns _FromExprs rep)
16485 )
165− => (forall expr a proxy. Eval (_ToExprs expr a)
166− => proxy expr
167− -> Eval (_Columns expr) (Col Result)
168− -> a)
169− -> Eval (GGColumns algebra _Columns exprs) (Col Result)
170− -> rep x
86+ => (forall a proxy. Eval (_Table a)
87+ => proxy a -> Eval (_Columns a) (Col Result) -> Eval (_FromExprs a))
88+ -> Eval (GGColumns algebra _Columns rep) (Col Result)
89+ -> GMap _FromExprs rep x
17190ggfromResult f x = case algebraSing @algebra of
172− SProduct -> gfromResult @_ToExprs @_Columns @exprs f x
173− SSum -> gfromResultADT @_ToExprs @_Columns @exprs f x
91+ SProduct -> gfromResult @_Table @_Columns @_FromExprs @rep f x
92+ SSum -> gfromResultADT @_Table @_Columns @_FromExprs @rep f x
17493
17594
176−ggtoResult :: forall algebra _ToExprs _Columns exprs rep x.
95+ggtoResult :: forall algebra _Table _Columns _FromExprs rep x.
17796 ( KnownAlgebra algebra
178− , Eval (GGToExprs algebra _ToExprs _Columns exprs rep)
97+ , Eval (GGTable algebra _Table _Columns _FromExprs rep)
17998 )
180− => (forall expr a proxy. Eval (_ToExprs expr a)
181− => proxy expr
182− -> a
183− -> Eval (_Columns expr) (Col Result))
184− -> rep x
185− -> Eval (GGColumns algebra _Columns exprs) (Col Result)
99+ => (forall a proxy. Eval (_Table a)
100+ => proxy a -> Eval (_FromExprs a) -> Eval (_Columns a) (Col Result))
101+ -> GMap _FromExprs rep x
102+ -> Eval (GGColumns algebra _Columns rep) (Col Result)
186103ggtoResult f x = case algebraSing @algebra of
187− SProduct -> gtoResult @_ToExprs @_Columns @exprs f x
188− SSum -> gtoResultADT @_ToExprs @_Columns @exprs f x
104+ SProduct -> gtoResult @_Table @_Columns @_FromExprs @rep f x
105+ SSum -> gtoResultADT @_Table @_Columns @_FromExprs @rep f x
src/Rel8/Generic/Table/ADT.hs+61−194
@@ -1,10 +1,8 @@
11{-# language AllowAmbiguousTypes #-}
22{-# language DataKinds #-}
3−{-# language FlexibleContexts #-}
43{-# language FlexibleInstances #-}
54{-# language LambdaCase #-}
65{-# language MultiParamTypeClasses #-}
7−{-# language PolyKinds #-}
86{-# language RankNTypes #-}
97{-# language ScopedTypeVariables #-}
108{-# language StandaloneKindSignatures #-}
@@ -14,9 +12,8 @@
1412{-# language UndecidableInstances #-}
1513
1614module Rel8.Generic.Table.ADT
17− ( GTableADT, GColumnsADT, gfromColumnsADT, gtoColumnsADT, gtableADT
15+ ( GTableADT, GColumnsADT, gfromResultADT, gtoResultADT
1816 , GTableADT', GColumnsADT'
19− , GToExprsADT, gfromResultADT, gtoResultADT
2017 )
2118where
2219
@@ -33,18 +30,14 @@ import Prelude hiding ( null )
3330
3431-- rel8
3532import Rel8.FCF ( Eval, Exp )
36−import Rel8.Generic.Table.Record
37− ( GTable, GColumns, gtable
38− , GToExprs, gfromResult, gtoResult
39− )
40−import Rel8.Schema.HTable ( HTable, hmap )
33+import Rel8.Generic.Map ( GMap )
34+import Rel8.Generic.Table.Record ( GTable, GColumns, gfromResult, gtoResult )
35+import Rel8.Schema.HTable ( HTable )
4136import Rel8.Schema.HTable.Identity ( HIdentity( HType ), HType )
4237import Rel8.Schema.HTable.Label ( HLabel, hlabel, hunlabel )
4338import Rel8.Schema.HTable.Nullify ( HNullify, hnulls, hnullify, hunnullify )
4439import Rel8.Schema.HTable.Product ( HProduct( HProduct ) )
4540import qualified Rel8.Schema.Kind as K
46−import Rel8.Schema.Null ( Nullify )
47−import Rel8.Schema.Spec ( Spec( Spec ), SSpec )
4841import Rel8.Schema.Result
4942 ( Col( R ), Result
5043 , null, nullifier, unnullifier
@@ -77,241 +70,119 @@ type family GColumnsADT' _Columns htable rep where
7770type GTableADT
7871 :: (Type -> Exp Constraint)
7972 -> (Type -> Exp K.HTable)
80− -> K.HContext -> (Type -> Type) -> Constraint
81−class GTableADT _Table _Columns context rep where
82− gfromColumnsADT :: ()
83− => (forall spec. context spec -> Col Result spec)
84− -> (forall spec. Col Result spec -> context spec)
85− -> (forall a. Eval (_Table a) => Eval (_Columns a) context -> a)
86− -> GColumnsADT _Columns rep context
87− -> rep x
88−
89− gtoColumnsADT :: ()
90− => (forall spec. context spec -> Col Result spec)
91− -> (forall spec. Col Result spec -> context spec)
92− -> (forall a. Eval (_Table a) => a -> Eval (_Columns a) context)
93− -> rep x
94− -> GColumnsADT _Columns rep context
95−
96− gtableADT :: ()
97− => (forall a proxy. Eval (_Table a) => proxy a -> Eval (_Columns a) context)
98− -> (forall a. ()
99− => SSpec ('Spec a)
100− -> context ('Spec a)
101− -> context ('Spec (Nullify a)))
102− -> GColumnsADT _Columns rep context
103−
104−
105−instance
106− ( htable ~ HLabel "tag" (HType Tag)
107− , HTable (GColumnsADT _Columns (M1 D meta rep))
108− , Eval (_Table (htable context))
109− , Eval (_Columns (htable context)) ~ htable
110− , GTableADT' _Table _Columns htable context rep
111− , GToExprsADT' (Const _Table) _Columns htable rep rep
112− )
113− => GTableADT _Table _Columns context (M1 D meta rep)
114− where
115− gfromColumnsADT fromContext toContext fromColumns =
116− gfromResultADT @(Const _Table) @_Columns @(M1 D meta rep) @(M1 D meta rep)
117− (const (fromColumns . hmap toContext)) .
118− hmap fromContext
119−
120− gtoColumnsADT fromContext toContext toColumns =
121− hmap toContext .
122− gtoResultADT @(Const _Table) @_Columns @(M1 D meta rep) @(M1 D meta rep)
123− (const (hmap fromContext . toColumns))
124−
125− gtableADT table hnullifier =
126− gtableADT' @_Table @_Columns @htable @context @rep table hnullifier htable
127− where
128− htable = table (Proxy @(htable context))
129−
130−
131−type GTableADT'
132− :: (Type -> Exp Constraint)
133− -> (Type -> Exp K.HTable)
134− -> K.HTable -> K.HContext -> (Type -> Type) -> Constraint
135−class GTableADT' _Table _Columns htable context rep where
136− gtableADT' :: ()
137− => (forall a proxy. Eval (_Table a) => proxy a -> Eval (_Columns a) context)
138− -> (forall a. ()
139− => SSpec ('Spec a)
140− -> context ('Spec a)
141− -> context ('Spec (Nullify a)))
142− -> htable context
143− -> GColumnsADT' _Columns htable rep context
144−
145−
146−instance
147− ( htable' ~ GColumnsADT' _Columns htable a
148− , GTableADT' _Table _Columns htable context a
149− , GTableADT' _Table _Columns htable' context b
150− )
151− => GTableADT' _Table _Columns htable context (a :+: b)
152− where
153− gtableADT' table hnullifier =
154− gtableADT' @_Table @_Columns @_ @_ @b table hnullifier .
155− gtableADT' @_Table @_Columns @_ @_ @a table hnullifier
156−
157−
158−instance meta ~ 'MetaCons label _fixity _isRecord =>
159− GTableADT' _Table _Columns htable context (M1 C meta U1)
160− where
161− gtableADT' _ _ = id
162−
163−
164−instance {-# OVERLAPPABLE #-}
165− ( HTable (GColumns _Columns rep)
166− , GTable _Table _Columns context rep
167− , meta ~ 'MetaCons label _fixity _isRecord
168− , GColumnsADT' _Columns htable (M1 C ('MetaCons label _fixity _isRecord) rep) ~
169− HProduct htable (HLabel label (HNullify (GColumns _Columns rep)))
170− )
171− => GTableADT' _Table _Columns htable context (M1 C meta rep)
172− where
173− gtableADT' table hnullifier htable =
174− HProduct htable $
175− hlabel $
176− hnullify hnullifier $
177− gtable @_Table @_Columns @_ @rep table
178−
179−
180−type GToExprsADT
181− :: (Type -> Type -> Exp Constraint)
182− -> (Type -> Exp K.HTable)
183− -> (Type -> Type) -> (Type -> Type) -> Constraint
184−class GToExprsADT _ToExprs _Columns exprs rep where
73+ -> (Type -> Exp Type)
74+ -> (Type -> Type) -> Constraint
75+class GTableADT _Table _Columns _FromExprs rep where
18576 gfromResultADT :: ()
186− => (forall expr a proxy.
187− ( Eval (_ToExprs expr a)
188− , HTable (Eval (_Columns expr))
189− )
190− => proxy expr
191− -> Eval (_Columns expr) (Col Result)
192− -> a)
193− -> GColumnsADT _Columns exprs (Col Result)
194− -> rep x
77+ => (forall a proxy. Eval (_Table a)
78+ => proxy a -> Eval (_Columns a) (Col Result) -> Eval (_FromExprs a))
79+ -> GColumnsADT _Columns rep (Col Result)
80+ -> GMap _FromExprs rep x
19581
19682 gtoResultADT :: ()
197− => (forall expr a proxy.
198− ( Eval (_ToExprs expr a)
199− , HTable (Eval (_Columns expr))
200− )
201− => proxy expr
202− -> a
203− -> Eval (_Columns expr) (Col Result))
204− -> rep x
205− -> GColumnsADT _Columns exprs (Col Result)
83+ => (forall a proxy. Eval (_Table a)
84+ => proxy a -> Eval (_FromExprs a) -> Eval (_Columns a) (Col Result))
85+ -> GMap _FromExprs rep x
86+ -> GColumnsADT _Columns rep (Col Result)
20687
20788
20889instance
20990 ( htable ~ HLabel "tag" (HType Tag)
210− , GToExprsADT' _ToExprs _Columns htable exprs rep
91+ , Eval (_Table (htable context))
92+ , Eval (_Columns (htable context)) ~ htable
93+ , GTableADT' _Table _Columns _FromExprs htable rep
21194 )
212− => GToExprsADT _ToExprs _Columns (M1 D meta exprs) (M1 D meta rep)
95+ => GTableADT _Table _Columns _FromExprs (M1 D meta rep)
21396 where
21497 gfromResultADT fromResult columns =
215− case gfromResultADT' @_ToExprs @_Columns @_ @exprs fromResult tag columns of
98+ case gfromResultADT' @_Table @_Columns @_FromExprs @htable @rep fromResult tag columns of
21699 Just rep -> M1 rep
217100 _ -> error "ADT.fromColumns: mismatch between tag and data"
218101 where
219102 tag = (\(HType (R a)) -> a) . hunlabel @"tag"
220103
221104 gtoResultADT toResult (M1 rep) =
222− gtoResultADT' @_ToExprs @_Columns @_ @exprs toResult tag (Just rep)
105+ gtoResultADT' @_Table @_Columns @_FromExprs @htable @rep toResult tag (Just rep)
223106 where
224107 tag = hlabel @"tag" . HType . R
225108
226109
227−type GToExprsADT'
228− :: (Type -> Type -> Exp Constraint)
110+type GTableADT'
111+ :: (Type -> Exp Constraint)
229112 -> (Type -> Exp K.HTable)
230− -> K.HTable -> (Type -> Type) -> (Type -> Type) -> Constraint
231−class GToExprsADT' _ToExprs _Columns htable exprs rep where
232− gfromResultADT' :: ()
233− => (forall expr a proxy.
234− ( Eval (_ToExprs expr a)
235− , HTable (Eval (_Columns expr))
236− )
237− => proxy expr
238− -> Eval (_Columns expr) (Col Result)
239− -> a)
113+ -> (Type -> Exp Type)
114+ -> K.HTable -> (Type -> Type) -> Constraint
115+class GTableADT' _Table _Columns _FromExprs htable rep where
116+ gfromResultADT' :: context ~ Col Result
117+ => (forall a proxy. Eval (_Table a)
118+ => proxy a -> Eval (_Columns a) context -> Eval (_FromExprs a))
240119 -> (htable (Col Result) -> Tag)
241− -> GColumnsADT' _Columns htable exprs (Col Result)
242− -> Maybe (rep x)
120+ -> GColumnsADT' _Columns htable rep context
121+ -> Maybe (GMap _FromExprs rep x)
243122
244− gtoResultADT' :: ()
245− => (forall expr a proxy.
246− ( Eval (_ToExprs expr a)
247− , HTable (Eval (_Columns expr))
248− )
249− => proxy expr
250− -> a
251− -> Eval (_Columns expr) (Col Result))
123+ gtoResultADT' :: context ~ Col Result
124+ => (forall a proxy. Eval (_Table a)
125+ => proxy a -> Eval (_FromExprs a) -> Eval (_Columns a) context)
252126 -> (Tag -> htable (Col Result))
253− -> Maybe (rep x)
254− -> GColumnsADT' _Columns htable exprs (Col Result)
127+ -> Maybe (GMap _FromExprs rep x)
128+ -> GColumnsADT' _Columns htable rep context
255129
256− extract :: GColumnsADT' _Columns htable exprs context -> htable context
130+ extract :: GColumnsADT' _Columns htable rep context -> htable context
257131
258132
259133instance
260134 ( htable' ~ GColumnsADT' _Columns htable a
261− , GToExprsADT' _ToExprs _Columns htable a rep1
262− , GToExprsADT' _ToExprs _Columns htable' b rep2
135+ , GTableADT' _Table _Columns _FromExprs htable a
136+ , GTableADT' _Table _Columns _FromExprs htable' b
263137 )
264− => GToExprsADT' _ToExprs _Columns htable (a :+: b) (rep1 :+: rep2)
138+ => GTableADT' _Table _Columns _FromExprs htable (a :+: b)
265139 where
266140 gfromResultADT' fromResult f columns =
267141 case ma of
268142 Just a -> Just (L1 a)
269143 Nothing -> R1 <$>
270− gfromResultADT' @_ToExprs @_Columns @_ @b @rep2
144+ gfromResultADT' @_Table @_Columns @_FromExprs @_ @b
271145 fromResult
272− (f . extract @_ToExprs @_Columns @_ @a @rep1)
146+ (f . extract @_Table @_Columns @_FromExprs @_ @a)
273147 columns
274148 where
275149 ma =
276− gfromResultADT' @_ToExprs @_Columns @_ @a @rep1
150+ gfromResultADT' @_Table @_Columns @_FromExprs @_ @a
277151 fromResult
278152 f
279− (extract @_ToExprs @_Columns @_ @b @rep2 columns)
153+ (extract @_Table @_Columns @_FromExprs @_ @b columns)
280154
281155 gtoResultADT' toResult tag = \case
282156 Just (L1 a) ->
283− gtoResultADT' @_ToExprs @_Columns @_ @b @rep2
157+ gtoResultADT' @_Table @_Columns @_FromExprs @_ @b
284158 toResult
285− (\_ -> gtoResultADT' @_ToExprs @_Columns @_ @a @rep1
159+ (\_ -> gtoResultADT' @_Table @_Columns @_FromExprs @_ @a
286160 toResult
287161 tag
288162 (Just a))
289163 Nothing
290164 Just (R1 b) ->
291− gtoResultADT' @_ToExprs @_Columns @_ @b @rep2
165+ gtoResultADT' @_Table @_Columns @_FromExprs @_ @b
292166 toResult
293167 (\tag' ->
294− gtoResultADT' @_ToExprs @_Columns @_ @a @rep1
168+ gtoResultADT' @_Table @_Columns @_FromExprs @_ @a
295169 toResult
296170 (\_ -> tag tag')
297171 Nothing)
298172 (Just b)
299173 Nothing ->
300− gtoResultADT' @_ToExprs @_Columns @_ @b @rep2
174+ gtoResultADT' @_Table @_Columns @_FromExprs @_ @b
301175 toResult
302− (\_ -> gtoResultADT' @_ToExprs @_Columns @_ @a @rep1 toResult tag Nothing)
176+ (\_ -> gtoResultADT' @_Table @_Columns @_FromExprs @_ @a toResult tag Nothing)
303177 Nothing
304178
305179 extract =
306− extract @_ToExprs @_Columns @_ @a @rep1 .
307− extract @_ToExprs @_Columns @_ @b @rep2
180+ extract @_Table @_Columns @_FromExprs @_ @a .
181+ extract @_Table @_Columns @_FromExprs @_ @b
308182
309183
310−instance
311− ( meta ~ 'MetaCons label _fixity _isRecord
312− , KnownSymbol label
313− )
314− => GToExprsADT' _ToExprs _Columns htable (M1 C meta U1) (M1 C meta U1)
184+instance (meta ~ 'MetaCons label _fixity _isRecord, KnownSymbol label) =>
185+ GTableADT' _Table _Columns _FromExprs htable (M1 C meta U1)
315186 where
316187 gfromResultADT' _ tag columns
317188 | tag columns == tag' = Just (M1 U1)
@@ -327,18 +198,18 @@ instance
327198
328199
329200instance {-# OVERLAPPABLE #-}
330− ( HTable (GColumns _Columns exprs)
331− , GToExprs _ToExprs _Columns exprs rep
201+ ( HTable (GColumns _Columns rep)
202+ , GTable _Table _Columns _FromExprs rep
332203 , meta ~ 'MetaCons label _fixity _isRecord
333204 , KnownSymbol label
334− , GColumnsADT' _Columns htable (M1 C meta exprs) ~
335− HProduct htable (HLabel label (HNullify (GColumns _Columns exprs)))
205+ , GColumnsADT' _Columns htable (M1 C ('MetaCons label _fixity _isRecord) rep) ~
206+ HProduct htable (HLabel label (HNullify (GColumns _Columns rep)))
336207 )
337− => GToExprsADT' _ToExprs _Columns htable (M1 C meta exprs) (M1 C meta rep)
208+ => GTableADT' _Table _Columns _FromExprs htable (M1 C meta rep)
338209 where
339210 gfromResultADT' fromResult tag (HProduct a b)
340211 | tag a == tag' =
341− M1 . gfromResult @_ToExprs @_Columns @exprs fromResult <$>
212+ M1 . gfromResult @_Table @_Columns @_FromExprs @rep fromResult <$>
342213 hunnullify unnullifier (hunlabel b)
343214 | otherwise = Nothing
344215 where
@@ -349,12 +220,8 @@ instance {-# OVERLAPPABLE #-}
349220 Just (M1 rep) -> HProduct (tag tag') $
350221 hlabel $
351222 hnullify nullifier $
352− gtoResult @_ToExprs @_Columns @exprs toResult rep
223+ gtoResult @_Table @_Columns @_FromExprs @rep toResult rep
353224 where
354225 tag' = Tag $ pack $ symbolVal (Proxy @label)
355226
356227 extract (HProduct a _) = a
357−
358−
359−data Const :: (a -> Exp Constraint) -> a -> a -> Exp Constraint
360−type instance Eval (Const f x a) = (Eval (f a), x ~ a)
src/Rel8/Generic/Table/Record.hs+55−102
@@ -13,8 +13,8 @@
1313{-# language UndecidableInstances #-}
1414
1515module Rel8.Generic.Table.Record
16− ( GTable, GColumns, GContext, gfromColumns, gtoColumns, gtable
17− , GToExprs, gfromResult, gtoResult
16+ ( GTable, GColumns, GContext
17+ , gfromColumns, gtoColumns, gfromResult, gtoResult, gtable
1818 )
1919where
2020
@@ -30,12 +30,10 @@ import Prelude hiding ( null )
3030
3131-- rel8
3232import Rel8.FCF ( Eval, Exp )
33−import Rel8.Schema.Context ( Col )
34−import Rel8.Schema.HTable ( HTable )
33+import Rel8.Generic.Map ( GMap )
3534import Rel8.Schema.HTable.Label ( HLabel, hlabel, hunlabel )
3635import Rel8.Schema.HTable.Product ( HProduct(..) )
3736import qualified Rel8.Schema.Kind as K
38−import Rel8.Schema.Result ( Result )
3937
4038
4139type GColumns :: (Type -> Exp K.HTable) -> (Type -> Type) -> K.HTable
@@ -58,8 +56,9 @@ type family GContext _Context rep where
5856type GTable
5957 :: (Type -> Exp Constraint)
6058 -> (Type -> Exp K.HTable)
61− -> K.HContext -> (Type -> Type) -> Constraint
62−class GTable _Table _Columns context rep
59+ -> (Type -> Exp Type)
60+ -> (Type -> Type) -> Constraint
61+class GTable _Table _Columns _FromExprs rep
6362 where
6463 gfromColumns :: ()
6564 => (forall a. Eval (_Table a) => Eval (_Columns a) context -> a)
@@ -71,46 +70,73 @@ class GTable _Table _Columns context rep
7170 -> rep x
7271 -> GColumns _Columns rep context
7372
73+ gfromResult :: ()
74+ => (forall a proxy. Eval (_Table a)
75+ => proxy a -> Eval (_Columns a) context -> Eval (_FromExprs a))
76+ -> GColumns _Columns rep context
77+ -> GMap _FromExprs rep x
78+
79+ gtoResult :: ()
80+ => (forall a proxy. Eval (_Table a)
81+ => proxy a -> Eval (_FromExprs a) -> Eval (_Columns a) context)
82+ -> GMap _FromExprs rep x
83+ -> GColumns _Columns rep context
84+
7485 gtable :: ()
7586 => (forall a proxy. Eval (_Table a) => proxy a -> Eval (_Columns a) context)
7687 -> GColumns _Columns rep context
7788
7889
79−instance GTable _Table _Columns context rep =>
80− GTable _Table _Columns context (M1 D c rep)
90+instance GTable _Table _Columns _FromExprs rep =>
91+ GTable _Table _Columns _FromExprs (M1 D c rep)
8192 where
8293 gfromColumns fromColumns =
83− M1 . gfromColumns @_Table @_Columns @context @rep fromColumns
94+ M1 . gfromColumns @_Table @_Columns @_FromExprs @rep fromColumns
8495 gtoColumns toColumns (M1 a) =
85− gtoColumns @_Table @_Columns @context @rep toColumns a
86− gtable = gtable @_Table @_Columns @context @rep
96+ gtoColumns @_Table @_Columns @_FromExprs @rep toColumns a
97+ gfromResult fromResult =
98+ M1 . gfromResult @_Table @_Columns @_FromExprs @rep fromResult
99+ gtoResult toResult (M1 a) =
100+ gtoResult @_Table @_Columns @_FromExprs @rep toResult a
101+ gtable = gtable @_Table @_Columns @_FromExprs @rep
87102
88103
89−instance GTable _Table _Columns context rep =>
90− GTable _Table _Columns context (M1 C c rep)
104+instance GTable _Table _Columns _FromExprs rep =>
105+ GTable _Table _Columns _FromExprs (M1 C c rep)
91106 where
92107 gfromColumns fromColumns =
93− M1 . gfromColumns @_Table @_Columns @context @rep fromColumns
108+ M1 . gfromColumns @_Table @_Columns @_FromExprs @rep fromColumns
94109 gtoColumns toColumns (M1 a) =
95− gtoColumns @_Table @_Columns @context @rep toColumns a
96− gtable = gtable @_Table @_Columns @context @rep
110+ gtoColumns @_Table @_Columns @_FromExprs @rep toColumns a
111+ gfromResult fromResult =
112+ M1 . gfromResult @_Table @_Columns @_FromExprs @rep fromResult
113+ gtoResult toResult (M1 a) =
114+ gtoResult @_Table @_Columns @_FromExprs @rep toResult a
115+ gtable = gtable @_Table @_Columns @_FromExprs @rep
97116
98117
99118instance
100− ( GTable _Table _Columns context rep1
101− , GTable _Table _Columns context rep2
119+ ( GTable _Table _Columns _FromExprs rep1
120+ , GTable _Table _Columns _FromExprs rep2
102121 )
103− => GTable _Table _Columns context (rep1 :*: rep2)
122+ => GTable _Table _Columns _FromExprs (rep1 :*: rep2)
104123 where
105124 gfromColumns fromColumns (HProduct a b) =
106− gfromColumns @_Table @_Columns @context @rep1 fromColumns a :*:
107− gfromColumns @_Table @_Columns @context @rep2 fromColumns b
125+ gfromColumns @_Table @_Columns @_FromExprs @rep1 fromColumns a :*:
126+ gfromColumns @_Table @_Columns @_FromExprs @rep2 fromColumns b
108127 gtoColumns toColumns (a :*: b) = HProduct
109− (gtoColumns @_Table @_Columns @context @rep1 toColumns a)
110− (gtoColumns @_Table @_Columns @context @rep2 toColumns b)
128+ (gtoColumns @_Table @_Columns @_FromExprs @rep1 toColumns a)
129+ (gtoColumns @_Table @_Columns @_FromExprs @rep2 toColumns b)
130+ gfromResult fromResult (HProduct a b) =
131+ gfromResult @_Table @_Columns @_FromExprs @rep1 fromResult a :*:
132+ gfromResult @_Table @_Columns @_FromExprs @rep2 fromResult b
133+ gtoResult toResult (a :*: b) =
134+ HProduct
135+ (gtoResult @_Table @_Columns @_FromExprs @rep1 toResult a)
136+ (gtoResult @_Table @_Columns @_FromExprs @rep2 toResult b)
111137 gtable table = HProduct
112− (gtable @_Table @_Columns @context @rep1 table)
113− (gtable @_Table @_Columns @context @rep2 table)
138+ (gtable @_Table @_Columns @_FromExprs @rep1 table)
139+ (gtable @_Table @_Columns @_FromExprs @rep2 table)
114140
115141
116142instance
@@ -118,83 +144,10 @@ instance
118144 , meta ~ 'MetaSel ('Just label) _su _ss _ds
119145 , k1 ~ K1 i a
120146 )
121− => GTable _Table _Columns context (M1 S meta k1)
147+ => GTable _Table _Columns _FromExprs (M1 S meta k1)
122148 where
123149 gfromColumns fromColumns = M1 . K1 . fromColumns . hunlabel
124150 gtoColumns toColumns (M1 (K1 a)) = hlabel (toColumns a)
151+ gfromResult fromResult = M1 . K1 . fromResult (Proxy @a) . hunlabel
152+ gtoResult toResult (M1 (K1 a)) = hlabel (toResult (Proxy @a) a)
125153 gtable table = hlabel (table (Proxy @a))
126−
127−
128−type GToExprs
129− :: (Type -> Type -> Exp Constraint)
130− -> (Type -> Exp K.HTable)
131− -> (Type -> Type) -> (Type -> Type) -> Constraint
132−class GToExprs _ToExprs _Columns exprs rep where
133− gfromResult :: ()
134− => (forall expr a proxy.
135− ( Eval (_ToExprs expr a)
136− , HTable (Eval (_Columns expr))
137− )
138− => proxy expr
139− -> Eval (_Columns expr) (Col Result)
140− -> a)
141− -> GColumns _Columns exprs (Col Result)
142− -> rep x
143− gtoResult :: ()
144− => (forall expr a proxy.
145− ( Eval (_ToExprs expr a)
146− , HTable (Eval (_Columns expr))
147− )
148− => proxy expr
149− -> a
150− -> Eval (_Columns expr) (Col Result))
151− -> rep x
152− -> GColumns _Columns exprs (Col Result)
153−
154−
155−instance GToExprs _ToExprs _Columns exprs rep =>
156− GToExprs _ToExprs _Columns (M1 D c exprs) (M1 D c rep)
157− where
158− gfromResult fromResult =
159− M1 . gfromResult @_ToExprs @_Columns @exprs fromResult
160− gtoResult toResult (M1 a) =
161− gtoResult @_ToExprs @_Columns @exprs toResult a
162−
163−
164−instance GToExprs _ToExprs _Columns exprs rep =>
165− GToExprs _ToExprs _Columns (M1 C c exprs) (M1 C c rep)
166− where
167− gfromResult fromResult =
168− M1 . gfromResult @_ToExprs @_Columns @exprs fromResult
169− gtoResult toResult (M1 a) =
170− gtoResult @_ToExprs @_Columns @exprs toResult a
171−
172−
173−instance
174− ( GToExprs _ToExprs _Columns exprs1 rep1
175− , GToExprs _ToExprs _Columns exprs2 rep2
176− )
177− => GToExprs _ToExprs _Columns (exprs1 :*: exprs2) (rep1 :*: rep2)
178− where
179− gfromResult fromResult (HProduct a b) =
180− gfromResult @_ToExprs @_Columns @exprs1 fromResult a :*:
181− gfromResult @_ToExprs @_Columns @exprs2 fromResult b
182− gtoResult toResult (a :*: b) =
183− HProduct
184− (gtoResult @_ToExprs @_Columns @exprs1 toResult a)
185− (gtoResult @_ToExprs @_Columns @exprs2 toResult b)
186−
187−
188−instance
189− ( Eval (_ToExprs exprs a)
190− , HTable (Eval (_Columns exprs))
191− , meta ~ 'MetaSel ('Just label) _su _ss _ds
192− , k1 ~ K1 i exprs
193− , k1' ~ K1 i a
194− )
195− => GToExprs _ToExprs _Columns (M1 S meta k1) (M1 S meta k1')
196− where
197− gfromResult fromResult =
198− M1 . K1 . fromResult (Proxy @exprs) . hunlabel
199− gtoResult toResult (M1 (K1 a)) =
200− hlabel (toResult (Proxy @exprs) a)
src/Rel8/Kind/Context.hs+1−21
@@ -1,12 +1,10 @@
11{-# language DataKinds #-}
22{-# language GADTs #-}
3−{-# language LambdaCase #-}
43{-# language StandaloneKindSignatures #-}
54
65module Rel8.Kind.Context
76 ( Reifiable( contextSing )
87 , SContext(..)
9− , sReifiable
108 )
119where
1210
@@ -17,11 +15,8 @@ import Prelude ()
1715-- rel8
1816import Rel8.Aggregate ( Aggregate )
1917import Rel8.Expr ( Expr )
20−import Rel8.Schema.Dict ( Dict( Dict ) )
21−import Rel8.Schema.Context ( Interpretation )
2218import Rel8.Schema.Kind ( Context )
2319import Rel8.Schema.Name ( Name )
24−import Rel8.Schema.Reify ( Reify )
2520import Rel8.Schema.Result ( Result )
2621
2722
@@ -31,11 +26,10 @@ data SContext context where
3126 SExpr :: SContext Expr
3227 SName :: SContext Name
3328 SResult :: SContext Result
34− SReify :: SContext context -> SContext (Reify context)
3529
3630
3731type Reifiable :: Context -> Constraint
38−class Interpretation context => Reifiable context where
32+class Reifiable context where
3933 contextSing :: SContext context
4034
4135
@@ -53,17 +47,3 @@ instance Reifiable Result where
5347
5448instance Reifiable Name where
5549 contextSing = SName
56−
57−
58−instance Reifiable context => Reifiable (Reify context) where
59− contextSing = SReify contextSing
60−
61−
62−sReifiable :: SContext context -> Dict Reifiable context
63−sReifiable = \case
64− SAggregate -> Dict
65− SExpr -> Dict
66− SName -> Dict
67− SResult -> Dict
68− SReify context -> case sReifiable context of
69− Dict -> Dict
src/Rel8/Schema/Context.hs+6
@@ -4,6 +4,7 @@
44
55module Rel8.Schema.Context
66 ( Interpretation( Col )
7+ , UnCol
78 )
89where
910
@@ -18,3 +19,8 @@ import Rel8.Schema.Kind ( Context, HContext )
1819type Interpretation :: Context -> Constraint
1920class Interpretation context where
2021 data Col context :: HContext
22+
23+
24+type UnCol :: HContext -> Context
25+type family UnCol context where
26+ UnCol (Col context) = context
src/Rel8/Schema/Context/Abstract.hsdeleted−80
@@ -1,80 +0,0 @@
1−{-# language DataKinds #-}
2−{-# language GADTs #-}
3−{-# language LambdaCase #-}
4−{-# language StandaloneKindSignatures #-}
5−{-# language TypeFamilies #-}
6−{-# language TypeOperators #-}
7−
8−module Rel8.Schema.Context.Abstract
9− ( Abstract, virtual
10− , Virtual(..), virtualOrResult, exclusivity
11− )
12−where
13−
14−-- base
15−import Data.Kind ( Constraint, Type )
16−import Data.Type.Equality ( (:~:)( Refl) )
17−import Prelude
18−
19−-- rel8
20−import Rel8.Aggregate ( Aggregate )
21−import Rel8.Expr ( Expr )
22−import Rel8.Kind.Context ( SContext(..) )
23−import qualified Rel8.Schema.Kind as K
24−import Rel8.Schema.Name ( Name )
25−import Rel8.Schema.Reify ( Reify )
26−import Rel8.Schema.Result ( Result, NotResult( NotResult ) )
27−
28−
29−type Abstract :: K.Context -> Constraint
30−type family Abstract context where
31− Abstract (Reify context) = IsVirtual context
32− Abstract _ = ()
33−
34−
35−type IsVirtual :: K.Context -> Constraint
36−class IsVirtual context where
37− virtual :: Virtual context
38−
39−
40−instance IsVirtual Aggregate where
41− virtual = VAggregate
42−
43−
44−instance IsVirtual Expr where
45− virtual = VExpr
46−
47−
48−instance IsVirtual Name where
49− virtual = VName
50−
51−
52−instance IsVirtual (Reify context) where
53− virtual = VReify
54−
55−
56−type Virtual :: K.Context -> Type
57−data Virtual context where
58− VAggregate :: Virtual Aggregate
59− VExpr :: Virtual Expr
60− VName :: Virtual Name
61− VReify :: Virtual (Reify context)
62−
63−
64−virtualOrResult :: ()
65− => SContext context
66− -> Either (context :~: Result) (Virtual context)
67−virtualOrResult = \case
68− SAggregate -> Right VAggregate
69− SExpr -> Right VExpr
70− SName -> Right VName
71− SResult -> Left Refl
72− SReify _ -> Right VReify
73−
74−
75−exclusivity :: Virtual context -> NotResult context
76−exclusivity = \case
77− VAggregate -> NotResult
78− VExpr -> NotResult
79− VName -> NotResult
80− VReify -> NotResult
src/Rel8/Schema/Context/Nullify.hs−15
@@ -15,7 +15,6 @@ module Rel8.Schema.Context.Nullify
1515where
1616
1717-- base
18−import Data.Bifunctor ( bimap )
1918import Data.Bool ( bool )
2019import Data.Kind ( Constraint, Type )
2120import Data.Monoid ( getFirst )
@@ -37,7 +36,6 @@ import Rel8.Kind.Context ( SContext(..) )
3736import qualified Rel8.Schema.Kind as K
3837import Rel8.Schema.Name ( Col( N ), Name( Name ) )
3938import Rel8.Schema.Null ( Nullify, Nullity( Null, NotNull ) )
40−import Rel8.Schema.Reify ( Col( Reify ), Reify )
4139import Rel8.Schema.Result ( Col( R ), Result )
4240import Rel8.Schema.Spec ( Spec( Spec ), SSpec(..) )
4341
@@ -47,7 +45,6 @@ data Nullifiability context where
4745 NAggregate :: Nullifiability Aggregate
4846 NExpr :: Nullifiability Expr
4947 NName :: Nullifiability Name
50− NReify :: Nullifiability context -> Nullifiability (Reify context)
5148
5249
5350type Nullifiable :: K.Context -> Constraint
@@ -67,14 +64,9 @@ instance Nullifiable Name where
6764 nullifiability = NName
6865
6966
70−instance Nullifiable context => Nullifiable (Reify context) where
71− nullifiability = NReify nullifiability
72−
73−
7467type NonNullifiability :: K.Context -> Type
7568data NonNullifiability context where
7669 NNResult :: NonNullifiability Result
77− NNReify :: NonNullifiability context -> NonNullifiability (Reify context)
7870
7971
8072nullifiableOrNot :: ()
@@ -85,7 +77,6 @@ nullifiableOrNot = \case
8577 SExpr -> Right NExpr
8678 SName -> Right NName
8779 SResult -> Left NNResult
88− SReify context -> bimap NNReify NReify $ nullifiableOrNot context
8980
9081
9182absurd :: Nullifiability context -> NonNullifiability context -> a
@@ -93,8 +84,6 @@ absurd = \case
9384 NAggregate -> \case
9485 NExpr -> \case
9586 NName -> \case
96− NReify context -> \case
97− NNReify context' -> absurd context context'
9887
9988
10089guarder :: ()
@@ -119,8 +108,6 @@ guarder SName _ _ _ name = name
119108guarder SResult (R tag) isNonNull _ (R a) = R (bool Nothing a condition)
120109 where
121110 condition = isNonNull tag
122−guarder (SReify context) (Reify tag) isNonNull isNonNullExpr (Reify a) =
123− Reify $ guarder context tag isNonNull isNonNullExpr a
124111
125112
126113nullifier :: ()
@@ -132,7 +119,6 @@ nullifier NAggregate SSpec {nullity} (A (Aggregate a)) =
132119 A $ Aggregate $ snullify nullity <$> a
133120nullifier NExpr SSpec {nullity} (E a) = E $ snullify nullity a
134121nullifier NName _ (N (Name a)) = N $ Name a
135−nullifier (NReify context) spec (Reify a) = Reify $ nullifier context spec a
136122
137123
138124unnullifier :: ()
@@ -144,7 +130,6 @@ unnullifier NAggregate SSpec {nullity} (A (Aggregate a)) =
144130 A $ Aggregate $ sunnullify nullity <$> a
145131unnullifier NExpr SSpec {nullity} (E a) = E $ sunnullify nullity a
146132unnullifier NName _ (N (Name a)) = N $ Name a
147−unnullifier (NReify context) spec (Reify a) = Reify (unnullifier context spec a)
148133
149134
150135sguard :: Expr Bool -> Expr (Maybe a) -> Expr (Maybe a)
src/Rel8/Schema/Context/Virtual.hsnew file+70
@@ -0,0 +1,70 @@
1+{-# language EmptyCase #-}
2+{-# language DataKinds #-}
3+{-# language GADTs #-}
4+{-# language LambdaCase #-}
5+{-# language StandaloneKindSignatures #-}
6+{-# language TypeFamilies #-}
7+
8+module Rel8.Schema.Context.Virtual
9+ ( Virtual, virtual
10+ , Abstract(..), Concrete(..), abstractOrConcrete, absurd
11+ )
12+where
13+
14+-- base
15+import Data.Kind ( Constraint, Type )
16+import Prelude
17+
18+-- rel8
19+import Rel8.Aggregate ( Aggregate )
20+import Rel8.Expr ( Expr )
21+import Rel8.Kind.Context ( SContext(..) )
22+import qualified Rel8.Schema.Kind as K
23+import Rel8.Schema.Name ( Name )
24+import Rel8.Schema.Result ( Result )
25+
26+
27+type Virtual :: K.Context -> Constraint
28+class Virtual context where
29+ virtual :: Abstract context
30+
31+
32+instance Virtual Aggregate where
33+ virtual = VAggregate
34+
35+
36+instance Virtual Expr where
37+ virtual = VExpr
38+
39+
40+instance Virtual Name where
41+ virtual = VName
42+
43+
44+type Abstract :: K.Context -> Type
45+data Abstract context where
46+ VAggregate :: Abstract Aggregate
47+ VExpr :: Abstract Expr
48+ VName :: Abstract Name
49+
50+
51+type Concrete :: K.Context -> Type
52+data Concrete context where
53+ VResult :: Concrete Result
54+
55+
56+abstractOrConcrete :: ()
57+ => SContext context
58+ -> Either (Concrete context) (Abstract context)
59+abstractOrConcrete = \case
60+ SAggregate -> Right VAggregate
61+ SExpr -> Right VExpr
62+ SName -> Right VName
63+ SResult -> Left VResult
64+
65+
66+absurd :: Abstract context -> Concrete context -> a
67+absurd = \case
68+ VAggregate -> \case
69+ VExpr -> \case
70+ VName -> \case
src/Rel8/Schema/Name.hs+5−14
@@ -20,7 +20,6 @@ module Rel8.Schema.Name
2020where
2121
2222-- base
23−import Data.Functor.Identity ( Identity )
2423import Data.Kind ( Constraint, Type )
2524import Data.String ( IsString, fromString )
2625import Prelude
@@ -30,12 +29,11 @@ import Rel8.Expr ( Expr )
3029import Rel8.Schema.Context ( Interpretation, Col )
3130import Rel8.Schema.HTable.Identity ( HIdentity( HType ), HType )
3231import Rel8.Schema.Null ( Sql )
33−import Rel8.Schema.Reify ( notReify )
34−import Rel8.Schema.Result ( Result )
32+import Rel8.Schema.Result ( Col( R ) )
3533import Rel8.Schema.Spec ( Spec( Spec ) )
3634import Rel8.Table
3735 ( Table, Columns, Context, fromColumns, toColumns
38− , reify, unreify, coherence, congruence
36+ , FromExprs, fromResult, toResult
3937 )
4038import Rel8.Table.Recontextualize ( Recontextualize )
4139import Rel8.Type ( DBType )
@@ -60,27 +58,20 @@ instance k ~ Type => IsString (Name (a :: k)) where
6058instance Sql DBType a => Table Name (Name a) where
6159 type Columns (Name a) = HType a
6260 type Context (Name a) = Name
61+ type FromExprs (Name a) = a
6362
6463 toColumns a = HType (N a)
6564 fromColumns (HType (N a)) = a
66− reify = notReify
67− unreify = notReify
68− coherence = notReify
69− congruence = notReify
65+ toResult a = HType (R a)
66+ fromResult (HType (R a)) = a
7067
7168
7269instance Sql DBType a => Recontextualize Expr Name (Expr a) (Name a)
7370
7471
75−instance Sql DBType a => Recontextualize Result Name (Identity a) (Name a)
76−
77−
7872instance Sql DBType a => Recontextualize Name Expr (Name a) (Expr a)
7973
8074
81−instance Sql DBType a => Recontextualize Name Result (Name a) (Identity a)
82−
83−
8475instance Sql DBType a => Recontextualize Name Name (Name a) (Name a)
8576
8677
src/Rel8/Schema/Reify.hsdeleted−68
@@ -1,68 +0,0 @@
1−{-# language AllowAmbiguousTypes #-}
2−{-# language EmptyCase #-}
3−{-# language DataKinds #-}
4−{-# language FlexibleInstances #-}
5−{-# language ScopedTypeVariables #-}
6−{-# language StandaloneKindSignatures #-}
7−{-# language TypeApplications #-}
8−{-# language TypeFamilies #-}
9−{-# language TypeOperators #-}
10−{-# language UndecidableInstances #-}
11−
12−module Rel8.Schema.Reify
13− ( Reify, Col( Reify ), hreify, hunreify
14− , UnwrapReify
15− , NotReify, notReify
16− )
17−where
18−
19−-- base
20−import Data.Kind ( Constraint )
21−import Data.Type.Equality ( (:~:)( Refl ) )
22−import Prelude
23−
24−-- rel8
25−import Rel8.Schema.Context ( Interpretation, Col )
26−import Rel8.Schema.HTable ( HTable, hmap )
27−import Rel8.Schema.Kind ( Context )
28−
29−
30−type Reify :: Context -> Context
31−data Reify context a
32−
33−
34−instance Interpretation (Reify context) where
35− newtype Col (Reify context) spec = Reify (Col context spec)
36−
37−
38−hreify :: HTable t => t (Col context) -> t (Col (Reify context))
39−hreify = hmap Reify
40−
41−
42−hunreify :: HTable t => t (Col (Reify context)) -> t (Col context)
43−hunreify = hmap (\(Reify a) -> a)
44−
45−
46−type UnwrapReify :: Context -> Context
47−type family UnwrapReify context where
48− UnwrapReify (Reify context) = context
49−
50−
51−type IsReify :: Context -> Bool
52−type family IsReify context where
53− IsReify (Reify _) = 'True
54− IsReify _ = 'False
55−
56−
57−type NotReify :: Context -> Constraint
58−class IsReify context ~ 'False => NotReify context
59−instance IsReify context ~ 'False => NotReify context
60−
61−
62−notReify :: forall context ctx a. NotReify context => context :~: Reify ctx -> a
63−notReify refl = case lemma @context of
64− Refl -> case refl of
65−
66−
67−lemma :: NotReify context => IsReify context :~: 'False
68−lemma = Refl
src/Rel8/Schema/Result.hs−19
@@ -1,21 +1,17 @@
11{-# language DataKinds #-}
2−{-# language EmptyCase #-}
32{-# language GADTs #-}
4−{-# language LambdaCase #-}
53{-# language NamedFieldPuns #-}
64{-# language StandaloneKindSignatures #-}
75{-# language TypeFamilies #-}
86
97module Rel8.Schema.Result
108 ( Col( R, unR ), Result
11− , NotResult( NotResult ), absurd
129 , null, nullifier, unnullifier
1310 , vectorizer, unvectorizer
1411 )
1512where
1613
1714-- base
18−import Data.Kind ( Type )
1915import Prelude hiding ( null )
2016
2117-- rel8
@@ -38,21 +34,6 @@ instance Interpretation Result where
3834 R :: {unR :: !a} -> Col Result ('Spec a)
3935
4036
41−type IsResult :: Context -> Bool
42−type family IsResult context where
43− IsResult Result = 'True
44− IsResult _ = 'False
45−
46−
47−type NotResult :: Context -> Type
48−data NotResult context where
49− NotResult :: IsResult context ~ 'False => NotResult context
50−
51−
52−absurd :: NotResult Result -> a
53−absurd = \case
54−
55−
5637null :: Col Result ('Spec (Maybe a))
5738null = R Nothing
5839
src/Rel8/Table.hs+82−295
@@ -1,83 +1,44 @@
11{-# language AllowAmbiguousTypes #-}
22{-# language DataKinds #-}
33{-# language DefaultSignatures #-}
4−{-# language DisambiguateRecordFields #-}
54{-# language FlexibleContexts #-}
65{-# language FlexibleInstances #-}
76{-# language FunctionalDependencies #-}
8−{-# language LambdaCase #-}
9−{-# language NamedFieldPuns #-}
107{-# language ScopedTypeVariables #-}
118{-# language StandaloneKindSignatures #-}
129{-# language TypeApplications #-}
1310{-# language TypeFamilies #-}
14−{-# language TypeOperators #-}
1511{-# language UndecidableInstances #-}
1612
1713module Rel8.Table
1814 ( Table
19− ( Columns, Context, toColumns, fromColumns
20− , Unreify, reify, unreify, coherence, congruence
15+ ( Columns, Context, fromColumns, toColumns
16+ , FromExprs, fromResult, toResult
2117 )
2218 , Congruent
23− , TTable, TColumns, TContext, TUnreify
19+ , TTable, TColumns, TContext, TFromExprs
2420 )
2521where
2622
2723-- base
28−import Data.Functor ( ($>) )
29−import Data.Functor.Identity ( Identity( Identity ) )
3024import Data.Kind ( Constraint, Type )
31−import Data.List.NonEmpty ( NonEmpty )
32−import Data.Proxy ( Proxy( Proxy ) )
33−import Data.Type.Equality ( (:~:)( Refl ) )
3425import GHC.Generics ( Generic, Rep, from, to )
3526import Prelude hiding ( null )
3627
3728-- rel8
3829import Rel8.FCF ( Eval, Exp )
39−import Rel8.Kind.Algebra
40− ( SAlgebra( SSum, SProduct )
41− , KnownAlgebra, algebraSing
42− )
43−import Rel8.Generic.Coherence ( GCoherent, gcoherence, gcongruence )
44−import Rel8.Generic.Map ( GMap, GMappable, gmap, gunmap )
45−import Rel8.Generic.Table
46− ( GGTable, GGColumns, GGContext, ggfromColumns, ggtoColumns
47− , GAlgebra
30+import Rel8.Generic.Map ( GMap )
31+import Rel8.Generic.Table.Record
32+ ( GTable, GColumns, GContext
33+ , gfromColumns, gtoColumns, gfromResult, gtoResult
4834 )
4935import Rel8.Generic.Record ( Record(..) )
50−import Rel8.Generic.Reify ( ARep )
36+import Rel8.Schema.Context ( Col, UnCol )
5137import Rel8.Schema.HTable ( HTable )
52−import Rel8.Schema.HTable.Either ( HEitherTable(..) )
53−import Rel8.Schema.HTable.Identity ( HIdentity(..), HType )
54−import Rel8.Schema.HTable.Label ( hlabel, hrelabel, hunlabel )
55−import Rel8.Schema.HTable.List ( HListTable )
56−import Rel8.Schema.HTable.Maybe ( HMaybeTable(..) )
57−import Rel8.Schema.HTable.NonEmpty ( HNonEmptyTable )
58−import Rel8.Schema.HTable.Nullify ( hnulls, hnullify, hunnullify )
59−import Rel8.Schema.HTable.These ( HTheseTable(..) )
60−import Rel8.Schema.HTable.Vectorize ( hvectorize, hunvectorize )
38+import Rel8.Schema.HTable.Identity ( HIdentity(..) )
6139import qualified Rel8.Schema.Kind as K
62−import Rel8.Schema.Null ( Sql )
63−import Rel8.Schema.Reify
64− ( Reify, Col( Reify ), hreify, hunreify
65− , UnwrapReify
66− , notReify
67− )
68−import Rel8.Schema.Result
69− ( Col( R ), Result
70− , NotResult
71− , null, nullifier, unnullifier
72− , vectorizer, unvectorizer
73− )
40+import Rel8.Schema.Result ( Result )
7441import Rel8.Schema.Spec ( KnownSpec )
75−import Rel8.Type ( DBType )
76−import Rel8.Type.Tag ( EitherTag( IsLeft, IsRight ), MaybeTag( IsJust ) )
77−
78−-- these
79−import Data.These ( These( This, That, These ) )
80−import Data.These.Combinators ( justHere, justThere )
8142
8243
8344-- | @Table@s are one of the foundational elements of Rel8, and describe data
@@ -99,123 +60,100 @@ class (HTable (Columns a), context ~ Context a) => Table context a | a -> contex
9960 -- | The common context that all columns use as an interpretation.
10061 type Context a :: K.Context
10162
102− type Unreify a :: Type
63+ -- | The @FromExprs@ type family maps a type in the @Expr@ context to the
64+ -- corresponding Haskell type.
65+ type FromExprs a :: Type
10366
10467 toColumns :: a -> Columns a (Col context)
10568 fromColumns :: Columns a (Col context) -> a
10669
107− reify :: context :~: Reify ctx -> Unreify a -> a
108− unreify :: context :~: Reify ctx -> a -> Unreify a
109− coherence :: context :~: Reify ctx -> NotResult ctx -> Context (Unreify a) :~: ctx
110− congruence :: context :~: Reify ctx -> NotResult ctx -> Columns a :~: Columns (Unreify a)
111−
70+ fromResult :: Columns a (Col Result) -> FromExprs a
71+ toResult :: FromExprs a -> Columns a (Col Result)
11272
113− type Columns a = Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))
114− type Context a = Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record a)))
115− type Unreify a = DefaultUnreify a
73+ type Columns a = GColumns TColumns (Rep (Record a))
74+ type Context a = GContext TContext (Rep (Record a))
75+ type FromExprs a = DefaultFromExprs a
11676
11777 default toColumns ::
11878 ( Generic (Record a)
119− , KnownAlgebra (GAlgebra (Rep (Record a)))
120− , Eval (GGTable (GAlgebra (Rep (Record a))) (TTable context) TColumns (Col context) (Rep (Record a)))
121− , Columns a ~ Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))
122− , Context a ~ Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record a)))
79+ , GTable (TTable context) TColumns TFromExprs (Rep (Record a))
80+ , Columns a ~ GColumns TColumns (Rep (Record a))
12381 )
12482 => a -> Columns a (Col context)
12583 toColumns =
126− ggtoColumns
127− @(GAlgebra (Rep (Record a)))
84+ gtoColumns
12885 @(TTable context)
12986 @TColumns
130− id
131− id
87+ @TFromExprs
13288 toColumns .
13389 from .
13490 Record
13591
13692 default fromColumns ::
13793 ( Generic (Record a)
138− , KnownAlgebra (GAlgebra (Rep (Record a)))
139− , Eval (GGTable (GAlgebra (Rep (Record a))) (TTable context) TColumns (Col context) (Rep (Record a)))
140− , Columns a ~ Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))
141− , Context a ~ Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record a)))
94+ , GTable (TTable context) TColumns TFromExprs (Rep (Record a))
95+ , Columns a ~ GColumns TColumns (Rep (Record a))
14296 )
14397 => Columns a (Col context) -> a
14498 fromColumns =
14599 unrecord .
146100 to .
147− ggfromColumns
148− @(GAlgebra (Rep (Record a)))
101+ gfromColumns
149102 @(TTable context)
150103 @TColumns
151− id
152− id
104+ @TFromExprs
153105 fromColumns
154106
155− default reify ::
156− ( Generic (Record a)
157− , Generic (Record (Unreify a))
158− , GMappable (TTable context) (Rep (Record a))
159− , Rep (Record (Unreify a)) ~ GMap TUnreify (Rep (Record a))
107+ default toResult ::
108+ ( Generic (Record (FromExprs a))
109+ , GTable (TTable context) TColumns TFromExprs (Rep (Record a))
110+ , Columns a ~ GColumns TColumns (Rep (Record a))
111+ , Rep (Record (FromExprs a)) ~ GMap TFromExprs (Rep (Record a))
160112 )
161− => context :~: Reify ctx -> Unreify a -> a
162− reify Refl =
163− unrecord .
164− to .
165− gunmap @(TTable context) (Proxy @TUnreify) (reify Refl) .
113+ => FromExprs a -> Columns a (Col Result)
114+ toResult =
115+ gtoResult
116+ @(TTable context)
117+ @TColumns
118+ @TFromExprs
119+ @(Rep (Record a))
120+ (\(_ :: proxy x) -> toResult @(Context x) @x) .
166121 from .
167122 Record
168123
169− default unreify ::
170− ( Generic (Record a)
171− , Generic (Record (Unreify a))
172− , GMappable (TTable context) (Rep (Record a))
173− , Rep (Record (Unreify a)) ~ GMap TUnreify (Rep (Record a))
124+ default fromResult ::
125+ ( Generic (Record (FromExprs a))
126+ , GTable (TTable context) TColumns TFromExprs (Rep (Record a))
127+ , Columns a ~ GColumns TColumns (Rep (Record a))
128+ , Rep (Record (FromExprs a)) ~ GMap TFromExprs (Rep (Record a))
174129 )
175− => context :~: Reify ctx -> a -> Unreify a
176− unreify Refl =
130+ => Columns a (Col Result) -> FromExprs a
131+ fromResult =
177132 unrecord .
178133 to .
179− gmap @(TTable context) (Proxy @TUnreify) (unreify Refl) .
180− from .
181− Record
182−
183− default coherence ::
184− ( KnownAlgebra (GAlgebra (Rep (Record a)))
185− , GCoherent (TTable context) (Rep (Record a))
186− , Context a ~ Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record a)))
187− , Context (Unreify a) ~ Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record (Unreify a))))
188− , Rep (Record (Unreify a)) ~ GMap TUnreify (Rep (Record a))
189− )
190− => context :~: Reify ctx -> NotResult ctx -> Context (Unreify a) :~: ctx
191− coherence = case algebraSing @(GAlgebra (Rep (Record a))) of
192− SSum -> notReify
193− SProduct -> \proof abstract ->
194− gcoherence
195− @(TTable context)
196− @(Rep (Record a))
197− (Proxy @TContext)
198− (Proxy @TUnreify)
199− (\(_ :: _proxy x) -> coherence @context @x proof abstract)
200−
201− default congruence ::
202− ( KnownAlgebra (GAlgebra (Rep (Record a)))
203− , GCoherent (TTable context) (Rep (Record a))
204− , Context a ~ Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record a)))
205− , Columns a ~ Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))
206− , Columns (Unreify a) ~ Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record (Unreify a))))
207− , Rep (Record (Unreify a)) ~ GMap TUnreify (Rep (Record a))
208− )
209− => context :~: Reify ctx -> NotResult ctx -> Columns a :~: Columns (Unreify a)
210− congruence = case algebraSing @(GAlgebra (Rep (Record a))) of
211− SSum -> notReify
212− SProduct -> \proof abstract ->
213− gcongruence
214− @(TTable context)
215− @(Rep (Record a))
216− (Proxy @TColumns)
217− (Proxy @TUnreify)
218− (\(_ :: _proxy x) -> congruence @context @x proof abstract)
134+ gfromResult
135+ @(TTable context)
136+ @TColumns
137+ @TFromExprs
138+ @(Rep (Record a))
139+ (\(_ :: proxy x) -> fromResult @(Context x) @x)
140+
141+
142+type DefaultFromExprs :: Type -> Type
143+type family DefaultFromExprs a where
144+ DefaultFromExprs (t a b c d e f g) =
145+ t (FromExprs a) (FromExprs b) (FromExprs c) (FromExprs d) (FromExprs e)
146+ (FromExprs f) (FromExprs g)
147+ DefaultFromExprs (t a b c d e f) =
148+ t (FromExprs a) (FromExprs b) (FromExprs c) (FromExprs d) (FromExprs e)
149+ (FromExprs f)
150+ DefaultFromExprs (t a b c d e) =
151+ t (FromExprs a) (FromExprs b) (FromExprs c) (FromExprs d) (FromExprs e)
152+ DefaultFromExprs (t a b c d) =
153+ t (FromExprs a) (FromExprs b) (FromExprs c) (FromExprs d)
154+ DefaultFromExprs (t a b c) = t (FromExprs a) (FromExprs b) (FromExprs c)
155+ DefaultFromExprs (t a b) = t (FromExprs a) (FromExprs b)
156+ DefaultFromExprs (t a) = t (FromExprs a)
219157
220158
221159data TTable :: K.Context -> Type -> Exp Constraint
@@ -230,185 +168,34 @@ data TContext :: Type -> Exp K.Context
230168type instance Eval (TContext a) = Context a
231169
232170
233−data TUnreify :: Type -> Exp Type
234−type instance Eval (TUnreify a) = Unreify a
235−
236−
237−type DefaultUnreify :: Type -> Type
238−type family DefaultUnreify a where
239− DefaultUnreify (t a b c d e f g) =
240− t (Unreify a) (Unreify b) (Unreify c) (Unreify d) (Unreify e) (Unreify f) (Unreify g)
241− DefaultUnreify (t a b c d e f) =
242− t (Unreify a) (Unreify b) (Unreify c) (Unreify d) (Unreify e) (Unreify f)
243− DefaultUnreify (t a b c d e) =
244− t (Unreify a) (Unreify b) (Unreify c) (Unreify d) (Unreify e)
245− DefaultUnreify (t a b c d) =
246− t (Unreify a) (Unreify b) (Unreify c) (Unreify d)
247− DefaultUnreify (t a b c) = t (Unreify a) (Unreify b) (Unreify c)
248− DefaultUnreify (t a b) = t (Unreify a) (Unreify b)
249− DefaultUnreify (t a) = t (Unreify a)
250− DefaultUnreify a = ARep (GMap TUnreify (Rep a))
171+data TFromExprs :: Type -> Exp Type
172+type instance Eval (TFromExprs a) = FromExprs a
251173
252174
253175-- | Any 'HTable' is also a 'Table'.
254−instance HTable t => Table context (t (Col context)) where
255− type Columns (t (Col context)) = t
256− type Context (t (Col context)) = context
257− type Unreify (t (Col context)) = t (Col (UnwrapReify context))
176+instance (context ~ UnCol hcontext, hcontext ~ Col context, HTable t) =>
177+ Table context (t hcontext)
178+ where
179+ type Columns (t hcontext) = t
180+ type Context (t hcontext) = UnCol hcontext
181+ type FromExprs (t hcontext) = t (Col Result)
258182
259183 toColumns = id
260184 fromColumns = id
261−
262− reify Refl = hreify
263− unreify Refl = hunreify
264− coherence Refl _ = Refl
265− congruence Refl _ = Refl
185+ toResult = id
186+ fromResult = id
266187
267188
268189-- | Any context is trivially a table.
269190instance KnownSpec spec => Table context (Col context spec) where
270191 type Columns (Col context spec) = HIdentity spec
271192 type Context (Col context spec) = context
272− type Unreify (Col context spec) = Col (UnwrapReify context) spec
193+ type FromExprs (Col context spec) = Col Result spec
273194
274195 toColumns = HIdentity
275196 fromColumns = unHIdentity
276−
277− reify Refl = Reify
278− unreify Refl (Reify a) = a
279− coherence Refl _ = Refl
280− congruence Refl _ = Refl
281−
282−
283−instance Sql DBType a => Table Result (Identity a) where
284− type Columns (Identity a) = HType a
285− type Context (Identity a) = Result
286−
287− toColumns (Identity a) = HType (R a)
288− fromColumns (HType (R a)) = Identity a
289−
290− reify = notReify
291− unreify = notReify
292− coherence = notReify
293− congruence = notReify
294−
295−
296−instance (context ~ Result, Table context a, Table context b) =>
297− Table context (Either a b)
298− where
299− type Columns (Either a b) = HEitherTable (Columns a) (Columns b)
300− type Context (Either a b) = Context a
301−
302− toColumns = \case
303− Left table -> HEitherTable
304− { htag = hlabel (HType (R IsLeft))
305− , hleft = hlabel (hnullify nullifier (toColumns table))
306− , hright = hlabel (hnulls (const null))
307− }
308− Right table -> HEitherTable
309− { htag = hlabel (HType (R IsRight))
310− , hleft = hlabel (hnulls (const null))
311− , hright = hlabel (hnullify nullifier (toColumns table))
312− }
313−
314− fromColumns HEitherTable {htag, hleft, hright} = case hunlabel htag of
315− HType (R tag) -> case tag of
316− IsLeft -> maybe err (Left . fromColumns) $ hunnullify unnullifier (hunlabel hleft)
317− IsRight -> maybe err (Right . fromColumns) $ hunnullify unnullifier (hunlabel hright)
318− where
319− err = error "Either.fromColumns: mismatch between tag and data"
320−
321− coherence = notReify
322− congruence = notReify
323−
324−
325−instance (context ~ Result, Table context a) => Table context [a] where
326− type Columns [a] = HListTable (Columns a)
327− type Context [a] = Context a
328−
329− toColumns = hvectorize vectorizer . fmap toColumns
330− fromColumns = fmap fromColumns . hunvectorize unvectorizer
331−
332− coherence = notReify
333− congruence = notReify
334−
335−
336−instance (context ~ Result, Table context a) => Table context (Maybe a) where
337− type Columns (Maybe a) = HMaybeTable (Columns a)
338− type Context (Maybe a) = Context a
339−
340− toColumns = \case
341− Nothing -> HMaybeTable
342− { htag = hlabel (HIdentity (R Nothing))
343− , hjust = hlabel (hnulls (const null))
344− }
345− Just table -> HMaybeTable
346− { htag = hlabel (HIdentity (R (Just IsJust)))
347− , hjust = hlabel (hnullify nullifier (toColumns table))
348− }
349−
350− fromColumns HMaybeTable {htag, hjust} = case hunlabel htag of
351− HType (R tag) -> tag $>
352− case hunnullify unnullifier (hunlabel hjust) of
353− Nothing -> error "Maybe.fromColumns: mismatch between tag and data"
354− Just just -> fromColumns just
355−
356− coherence = notReify
357− congruence = notReify
358−
359−
360−instance (context ~ Result, Table context a) => Table context (NonEmpty a)
361− where
362− type Columns (NonEmpty a) = HNonEmptyTable (Columns a)
363− type Context (NonEmpty a) = Context a
364−
365− toColumns = hvectorize vectorizer . fmap toColumns
366− fromColumns = fmap fromColumns . hunvectorize unvectorizer
367−
368− coherence = notReify
369− congruence = notReify
370−
371−
372−instance (context ~ Result, Table context a, Table context b) =>
373− Table context (These a b)
374− where
375− type Columns (These a b) = HTheseTable (Columns a) (Columns b)
376− type Context (These a b) = Context a
377−
378− toColumns tables = HTheseTable
379− { hhereTag = hrelabel hhereTag
380− , hhere = hrelabel (toColumns hhere)
381− , hthereTag = hrelabel hthereTag
382− , hthere = hrelabel (toColumns hthere)
383− }
384− where
385− HMaybeTable
386− { htag = hhereTag
387− , hjust = hhere
388− } = toColumns (justHere tables)
389− HMaybeTable
390− { htag = hthereTag
391− , hjust = hthere
392− } = toColumns (justThere tables)
393−
394− fromColumns HTheseTable {hhereTag, hhere, hthereTag, hthere} =
395− case (fromColumns mhere, fromColumns mthere) of
396− (Just a, Nothing) -> This (fromColumns a)
397− (Nothing, Just b) -> That (fromColumns b)
398− (Just a, Just b) -> These (fromColumns a) (fromColumns b)
399− _ -> error "These.fromColumns: mismatch between tags and data"
400− where
401− mhere = HMaybeTable
402− { htag = hrelabel hhereTag
403− , hjust = hrelabel hhere
404− }
405− mthere = HMaybeTable
406− { htag = hrelabel hthereTag
407− , hjust = hrelabel hthere
408− }
409−
410− coherence = notReify
411− congruence = notReify
197+ toResult = HIdentity
198+ fromResult = unHIdentity
412199
413200
414201instance (Table context a, Table context b) => Table context (a, b)
src/Rel8/Table/ADT.hs+33−59
@@ -13,7 +13,7 @@
1313
1414module Rel8.Table.ADT
1515 ( ADT( ADT )
16− , ADTable, fromADT, toADT
16+ , ADTable
1717 , BuildableADT
1818 , BuildADT, buildADT
1919 , ConstructableADT
@@ -27,8 +27,6 @@ where
2727
2828-- base
2929import Data.Kind ( Constraint, Type )
30−import Data.Proxy ( Proxy( Proxy ) )
31−import Data.Type.Equality ( (:~:)( Refl ) )
3230import GHC.Generics ( Generic, Rep, from, to )
3331import GHC.TypeLits ( Symbol )
3432import Prelude
@@ -46,12 +44,12 @@ import Rel8.Generic.Construction
4644 , GGName, ggname
4745 , GGAggregate, ggaggregate
4846 )
49−import Rel8.Generic.Map ( GMappable, GMap, gmap, gunmap )
50−import Rel8.Generic.Record ( GRecordable, GRecord, grecord, gunrecord )
47+import Rel8.Generic.Map ( GMap )
48+import Rel8.Generic.Record ( Record( Record ), unrecord )
5149import Rel8.Generic.Rel8able
5250 ( Rel8able
5351 , GRep, GColumns, gfromColumns, gtoColumns
54− , greify, gunreify
52+ , GFromExprs, gfromResult, gtoResult
5553 )
5654import qualified Rel8.Generic.Table.ADT as G
5755import qualified Rel8.Kind.Algebra as K
@@ -59,12 +57,10 @@ import Rel8.Schema.Context ( Col )
5957import Rel8.Schema.HTable ( HTable )
6058import qualified Rel8.Schema.Kind as K
6159import Rel8.Schema.Name ( Name )
62−import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify )
6360import Rel8.Schema.Result ( Result )
6461import Rel8.Table
65− ( Table
66− , fromColumns, toColumns, reify, unreify
67− , TTable, TColumns, TUnreify
62+ ( Table, fromResult, toResult
63+ , TTable, TColumns, TFromExprs
6864 )
6965
7066
@@ -74,67 +70,45 @@ newtype ADT t context = ADT (GColumnsADT t (Col context))
7470
7571instance ADTable t => Rel8able (ADT t) where
7672 type GColumns (ADT t) = GColumnsADT t
73+ type GFromExprs (ADT t) = t Result
7774
78− gfromColumns = ADT
79− gtoColumns (ADT a) = a
75+ gfromColumns _ = ADT
76+ gtoColumns _ (ADT a) = a
8077
81− greify (ADT a) = ADT (hreify a)
82− gunreify (ADT a) = ADT (hunreify a)
83−
84−
85−instance (ADTable t, context ~ Result) => Generic (ADT t context) where
86− type Rep (ADT t context) = Rep (t context)
87−
88− from =
89− gmap @(TTable (Reify Result)) (Proxy @TUnreify) (unreify Refl) .
90− gunrecord @(Rep (t (Reify Result))) .
91− G.gfromColumnsADT
92− @(TTable (Reify Result))
93− @TColumns
94− (\(Reify a) -> a)
95− Reify
96− fromColumns .
97− hreify .
98− (\(ADT a) -> a)
99−
100− to =
101− ADT .
102− hunreify .
103− G.gtoColumnsADT
104− @(TTable (Reify Result))
78+ gfromResult =
79+ unrecord .
80+ to .
81+ G.gfromResultADT
82+ @(TTable Expr)
10583 @TColumns
106− (\(Reify a) -> a)
107− Reify
108− toColumns .
109− grecord @(Rep (t (Reify Result))) .
110− gunmap @(TTable (Reify Result)) (Proxy @TUnreify) (reify Refl)
84+ @TFromExprs
85+ @(Eval (ADTRep t Expr))
86+ (\(_ :: proxy x) -> fromResult @_ @x)
11187
112−
113−fromADT :: ADTable t => ADT t Result -> t Result
114−fromADT = to . from
115−
116−
117−toADT :: ADTable t => t Result -> ADT t Result
118−toADT = to . from
88+ gtoResult =
89+ G.gtoResultADT
90+ @(TTable Expr)
91+ @TColumns
92+ @TFromExprs
93+ @(Eval (ADTRep t Expr))
94+ (\(_ :: proxy x) -> toResult @_ @x) .
95+ from .
96+ Record
11997
12098
12199type ADTable :: K.Rel8able -> Constraint
122100class
123− ( Generic (t Result)
101+ ( Generic (Record (t Result))
124102 , HTable (GColumnsADT t)
125− , G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (Rep (t (Reify Result))))
126− , GRecordable (Rep (t (Reify Result)))
127− , GMappable (TTable (Reify Result)) (Rep (t (Reify Result)))
128− , GMap TUnreify (Rep (t (Reify Result))) ~ Rep (t Result)
103+ , G.GTableADT (TTable Expr) TColumns TFromExprs (Eval (ADTRep t Expr))
104+ , GMap TFromExprs (Rep (Record (t Expr))) ~ Rep (Record (t Result))
129105 )
130106 => ADTable t
131107instance
132− ( Generic (t Result)
108+ ( Generic (Record (t Result))
133109 , HTable (GColumnsADT t)
134− , G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (Rep (t (Reify Result))))
135− , GRecordable (Rep (t (Reify Result)))
136− , GMappable (TTable (Reify Result)) (Rep (t (Reify Result)))
137− , GMap TUnreify (Rep (t (Reify Result))) ~ Rep (t Result)
110+ , G.GTableADT (TTable Expr) TColumns TFromExprs (Eval (ADTRep t Expr))
111+ , GMap TFromExprs (Rep (Record (t Expr))) ~ Rep (Record (t Result))
138112 )
139113 => ADTable t
140114
@@ -202,4 +176,4 @@ type instance Eval (ADTRep t context) = GRep t context
202176
203177
204178type GColumnsADT :: K.Rel8able -> K.HTable
205−type GColumnsADT t = G.GColumnsADT TColumns (GRep t (Reify Result))
179+type GColumnsADT t = G.GColumnsADT TColumns (GRep t Expr)
src/Rel8/Table/Either.hs+27−37
@@ -3,6 +3,7 @@
33{-# language DerivingStrategies #-}
44{-# language FlexibleContexts #-}
55{-# language FlexibleInstances #-}
6+{-# language LambdaCase #-}
67{-# language MultiParamTypeClasses #-}
78{-# language NamedFieldPuns #-}
89{-# language ScopedTypeVariables #-}
@@ -23,11 +24,9 @@ module Rel8.Table.Either
2324where
2425
2526-- base
26−import Control.Category ( id )
2727import Data.Bifunctor ( Bifunctor, bimap )
2828import Data.Kind ( Type )
29−import Data.Type.Equality ( apply )
30−import Prelude hiding ( id, undefined )
29+import Prelude hiding ( undefined )
3130
3231-- comonad
3332import Control.Comonad ( extract )
@@ -38,7 +37,6 @@ import Rel8.Expr ( Col( E ), Expr )
3837import Rel8.Expr.Aggregate ( groupByExpr )
3938import Rel8.Expr.Serialize ( litExpr )
4039import Rel8.Kind.Context ( Reifiable )
41−import Rel8.Schema.Context.Abstract ( Abstract )
4240import Rel8.Schema.Context.Nullify ( Nullifiable )
4341import Rel8.Schema.Dict ( Dict( Dict ) )
4442import Rel8.Schema.HTable.Either ( HEitherTable(..) )
@@ -46,17 +44,18 @@ import Rel8.Schema.HTable.Identity ( HIdentity(..) )
4644import Rel8.Schema.HTable.Label ( hlabel, hunlabel )
4745import qualified Rel8.Schema.Kind as K
4846import Rel8.Schema.Name ( Col( N ), Name )
47+import Rel8.Schema.Result ( Col( R ) )
4948import Rel8.Schema.Spec ( Spec( Spec ) )
5049import Rel8.Table
5150 ( Table, Columns, Context, fromColumns, toColumns
52− , reify, unreify, coherence, congruence
51+ , FromExprs, fromResult, toResult
5352 )
5453import Rel8.Table.Bool ( bool )
5554import Rel8.Table.Eq ( EqTable, eqTable )
5655import Rel8.Table.Nullify ( Nullify, aggregateNullify, guard )
5756import Rel8.Table.Ord ( OrdTable, ordTable )
5857import Rel8.Table.Recontextualize ( Recontextualize )
59−import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
58+import Rel8.Table.Serialize ( ToExprs )
6059import Rel8.Table.Undefined ( undefined )
6160import Rel8.Type.Tag ( EitherTag( IsLeft, IsRight ), isLeft, isRight )
6261
@@ -112,12 +111,13 @@ instance (context ~ Expr, Table Expr a, Table Expr b) =>
112111
113112instance
114113 ( Table context a, Table context b
115− , Reifiable context, Abstract context, context ~ context'
114+ , Reifiable context, context ~ context'
116115 )
117116 => Table context' (EitherTable context a b)
118117 where
119118 type Columns (EitherTable context a b) = HEitherTable (Columns a) (Columns b)
120119 type Context (EitherTable context a b) = Context a
120+ type FromExprs (EitherTable context a b) = Either (FromExprs a) (FromExprs b)
121121
122122 toColumns EitherTable {tag, left, right} = HEitherTable
123123 { htag = hlabel $ HType tag
@@ -131,28 +131,29 @@ instance
131131 , right = fromColumns $ hunlabel hright
132132 }
133133
134− reify proof EitherTable {tag, left, right} = EitherTable
135− { tag
136− , left = reify proof left
137− , right = reify proof right
138− }
139−
140− unreify proof EitherTable {tag, left, right} = EitherTable
141− { tag
142− , left = unreify proof left
143− , right = unreify proof right
144− }
145−
146− coherence = coherence @context @a
147− congruence proof abstract =
148− id `apply`
149− congruence @context @a proof abstract `apply`
150− congruence @context @b proof abstract
134+ toResult = \case
135+ Left table -> HEitherTable
136+ { htag = hlabel (HType (R IsLeft))
137+ , hleft = hlabel (toResult @_ @(Nullify context a) (Just table))
138+ , hright = hlabel (toResult @_ @(Nullify context b) Nothing)
139+ }
140+ Right table -> HEitherTable
141+ { htag = hlabel (HType (R IsRight))
142+ , hleft = hlabel (toResult @_ @(Nullify context a) Nothing)
143+ , hright = hlabel (toResult @_ @(Nullify context b) (Just table))
144+ }
145+
146+ fromResult HEitherTable {htag, hleft, hright} = case hunlabel htag of
147+ HType (R tag) -> case tag of
148+ IsLeft -> maybe err Left $ fromResult @_ @(Nullify context a) (hunlabel hleft)
149+ IsRight -> maybe err Right $ fromResult @_ @(Nullify context b) (hunlabel hright)
150+ where
151+ err = error "Either.fromColumns: mismatch between tag and data"
151152
152153
153154instance
154− ( Reifiable from, Abstract from, from ~ from'
155− , Reifiable to, Abstract to, to ~ to'
155+ ( Reifiable from, from ~ from'
156+ , Reifiable to, to ~ to'
156157 , Recontextualize from to a1 b1
157158 , Recontextualize from to a2 b2
158159 )
@@ -179,19 +180,8 @@ instance (OrdTable a, OrdTable b, context ~ Expr) =>
179180 }
180181
181182
182−type instance FromExprs (EitherTable _context a b) =
183− Either (FromExprs a) (FromExprs b)
184−
185−
186183instance (ToExprs exprs1 a, ToExprs exprs2 b, x ~ EitherTable Expr exprs1 exprs2) =>
187184 ToExprs x (Either a b)
188− where
189− fromResult =
190− bimap (fromResult @exprs1) (fromResult @exprs2) .
191− fromColumns
192− toResult =
193− toColumns .
194− bimap (toResult @exprs1) (toResult @exprs2)
195185
196186
197187-- | Test if an 'EitherTable' is a 'leftTable'.
src/Rel8/Table/Eq.hs+6−12
@@ -33,11 +33,7 @@ import Rel8.Expr.Bool ( (||.), (&&.) )
3333import Rel8.Expr.Eq ( (==.), (/=.) )
3434import Rel8.FCF ( Eval, Exp )
3535import Rel8.Generic.Record ( Record )
36−import Rel8.Generic.Table
37− ( GGTable, GGColumns, ggtable
38− , GAlgebra
39− )
40−import Rel8.Kind.Algebra ( KnownAlgebra )
36+import Rel8.Generic.Table.Record ( GTable, GColumns, gtable )
4137import Rel8.Schema.Dict ( Dict( Dict ) )
4238import Rel8.Schema.HTable
4339 ( HTable, HConstrainTable
@@ -46,7 +42,7 @@ import Rel8.Schema.HTable
4642import Rel8.Schema.HTable.Identity ( HIdentity( HType ) )
4743import Rel8.Schema.Null ( Sql )
4844import Rel8.Schema.Spec.Constrain ( ConstrainSpec )
49−import Rel8.Table ( Table, Columns, toColumns, TColumns )
45+import Rel8.Table ( Table, Columns, toColumns, TColumns, TFromExprs )
5046import Rel8.Type.Eq ( DBEq )
5147
5248
@@ -58,19 +54,17 @@ class Table Expr a => EqTable a where
5854 eqTable :: Columns a (Dict (ConstrainSpec (Sql DBEq)))
5955
6056 default eqTable ::
61− ( KnownAlgebra (GAlgebra (Rep (Record a)))
62− , Eval (GGTable (GAlgebra (Rep (Record a))) TEqTable TColumns (Dict (ConstrainSpec (Sql DBEq))) (Rep (Record a)))
63− , Columns a ~ Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))
57+ ( GTable TEqTable TColumns TFromExprs (Rep (Record a))
58+ , Columns a ~ GColumns TColumns (Rep (Record a))
6459 )
6560 => Columns a (Dict (ConstrainSpec (Sql DBEq)))
6661 eqTable =
67− ggtable
68− @(GAlgebra (Rep (Record a)))
62+ gtable
6963 @TEqTable
7064 @TColumns
65+ @TFromExprs
7166 @(Rep (Record a))
7267 table
73− (\_ Dict -> Dict)
7468 where
7569 table (_ :: proxy x) = eqTable @x
7670
src/Rel8/Table/HKD.hs+64−106
@@ -13,7 +13,7 @@
1313
1414module Rel8.Table.HKD
1515 ( HKD( HKD )
16− , HKDable, fromHKD, toHKD, HKDT(..)
16+ , HKDable
1717 , BuildableHKD
1818 , BuildHKD, buildHKD
1919 , ConstructableHKD
@@ -27,9 +27,6 @@ where
2727
2828-- base
2929import Data.Kind ( Constraint, Type )
30−import Data.Proxy ( Proxy( Proxy ) )
31−import Data.Type.Equality ( (:~:)( Refl ) )
32−import Data.Void ( Void )
3330import GHC.Generics ( Generic, Rep, from, to )
3431import GHC.TypeLits ( Symbol )
3532import Prelude
@@ -49,35 +46,34 @@ import Rel8.Generic.Construction
4946 , GGName, ggname
5047 , GGAggregate, ggaggregate
5148 )
52−import Rel8.Generic.Map ( GMap, GMappable, gmap, gunmap )
53−import Rel8.Generic.Record ( GRecord, GRecordable, grecord, gunrecord )
49+import Rel8.Generic.Map ( GMap )
50+import Rel8.Generic.Record
51+ ( GRecord, GRecordable, grecord, gunrecord
52+ , Record( Record ), unrecord
53+ )
5454import Rel8.Generic.Rel8able
5555 ( Rel8able
5656 , GColumns, gfromColumns, gtoColumns
57− , greify, gunreify
58− , TUnreifyContext
57+ , GFromExprs, gfromResult, gtoResult
5958 )
6059import Rel8.Generic.Table
61− ( GGTable, GGColumns, GGContext, ggfromColumns, ggtoColumns
62− , GAlgebra
60+ ( GGTable, GGColumns, GAlgebra, ggfromResult, ggtoResult
6361 )
62+import Rel8.Generic.Table.Record ( GTable, GContext )
63+import qualified Rel8.Generic.Table.Record as G
6464import Rel8.Schema.Context ( Col )
6565import qualified Rel8.Schema.Kind as K
6666import Rel8.Schema.HTable ( HTable )
6767import Rel8.Schema.Name ( Name )
68−import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify, notReify )
69−import Rel8.Schema.Result ( Result )
7068import Rel8.Table
71− ( Table, Columns, Context, fromColumns, toColumns
72− , Unreify, reify, unreify, coherence, congruence
73− , TTable, TColumns, TUnreify
69+ ( Table, fromColumns, toColumns, fromResult, toResult
70+ , TTable, TColumns, TContext, TFromExprs
7471 )
75−import Rel8.Table.Serialize ( ToExprs, fromResult, toResult )
7672
7773
7874type GColumnsHKD :: Type -> K.HTable
7975type GColumnsHKD a =
80− Eval (GGColumns (GAlgebra (Rep a)) TColumns (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
76+ Eval (GGColumns (GAlgebra (Rep a)) TColumns (GRecord (GMap (TColumn Expr) (Rep a))))
8177
8278
8379type HKD :: Type -> K.Rel8able
@@ -86,128 +82,90 @@ newtype HKD a f = HKD (GColumnsHKD a (Col f))
8682
8783instance HKDable a => Rel8able (HKD a) where
8884 type GColumns (HKD a) = GColumnsHKD a
85+ type GFromExprs (HKD a) = a
8986
90− gfromColumns = HKD
91− gtoColumns (HKD a) = a
87+ gfromColumns _ = HKD
88+ gtoColumns _ (HKD a) = a
9289
93− greify (HKD a) = HKD (hreify a)
94− gunreify (HKD a) = HKD (hunreify a)
90+ gfromResult =
91+ unrecord .
92+ to .
93+ ggfromResult
94+ @(GAlgebra (Rep a))
95+ @(TTable Expr)
96+ @TColumns
97+ @TFromExprs
98+ @(Eval (HKDRep a Expr))
99+ (\(_ :: proxy x) -> fromResult @_ @x)
100+
101+ gtoResult =
102+ ggtoResult
103+ @(GAlgebra (Rep a))
104+ @(TTable Expr)
105+ @TColumns
106+ @TFromExprs
107+ @(Eval (HKDRep a Expr))
108+ (\(_ :: proxy x) -> toResult @_ @x) .
109+ from .
110+ Record
95111
96112
97113instance
98− ( KnownAlgebra (GAlgebra (Rep a))
99− , HTable (GColumnsHKD a)
100− , Eval (GGTable (GAlgebra (Rep a)) (TTable (Reify f)) TColumns (Col (Reify f)) (GRecord (GMap (TColumn (Reify f)) (Rep a))))
101− , Eval (GGColumns (GAlgebra (Rep a)) TColumns (GRecord (GMap (TColumn (Reify f)) (Rep a)))) ~ GColumnsHKD a
102− , Eval (GGContext (GAlgebra (Rep a)) TUnreifyContext (GRecord (GMap (TColumn (Reify f)) (Rep a)))) ~ f
103− , GRecordable (GMap (TColumn (Reify f)) (Rep a))
104− , GMappable (TTable (Reify f)) (GMap (TColumn (Reify f)) (Rep a))
105− , GMap TUnreify (GMap (TColumn (Reify f)) (Rep a)) ~ GMap (TColumn f) (Rep a)
114+ ( GTable (TTable f) TColumns TFromExprs (GRecord (GMap (TColumn f) (Rep a)))
115+ , G.GColumns TColumns (GRecord (GMap (TColumn f) (Rep a))) ~ GColumnsHKD a
116+ , GContext TContext (GRecord (GMap (TColumn f) (Rep a))) ~ f
117+ , GRecordable (GMap (TColumn f) (Rep a))
106118 )
107119 => Generic (HKD a f)
108120 where
109121 type Rep (HKD a f) = GMap (TColumn f) (Rep a)
110122
111123 from =
112− gmap @(TTable (Reify f)) (Proxy @TUnreify) (unreify Refl) .
113− gunrecord @(GMap (TColumn (Reify f)) (Rep a)) .
114− ggfromColumns
115− @(GAlgebra (Rep a))
116− @(TTable (Reify f))
124+ gunrecord @(GMap (TColumn f) (Rep a)) .
125+ G.gfromColumns
126+ @(TTable f)
117127 @TColumns
118− (\(Reify a) -> a)
119− Reify
128+ @TFromExprs
120129 fromColumns .
121− hreify .
122130 (\(HKD a) -> a)
123131
124132 to =
125133 HKD .
126− hunreify .
127− ggtoColumns
128− @(GAlgebra (Rep a))
129− @(TTable (Reify f))
134+ G.gtoColumns
135+ @(TTable f)
130136 @TColumns
131− (\(Reify a) -> a)
132− Reify
137+ @TFromExprs
133138 toColumns .
134− grecord @(GMap (TColumn (Reify f)) (Rep a)) .
135− gunmap @(TTable (Reify f)) (Proxy @TUnreify) (reify Refl)
136−
137−
138−type HKDT :: Type -> Type
139−newtype HKDT a = HKDT
140− { unHKDT :: a
141− }
142−
143−
144−instance HKDable a => Table Result (HKDT a) where
145− type Columns (HKDT a) = GColumnsHKD a
146− type Context (HKDT a) = Result
147− type Unreify (HKDT a) = Void
148−
149− fromColumns = HKDT . fromHKD . HKD
150− toColumns = (\(HKD a) -> a) . toHKD . (\(HKDT a) -> a)
151− reify = notReify
152− unreify = notReify
153− coherence = notReify
154− congruence = notReify
155−
156−
157−instance
158− ( Table Expr (HKD a Expr)
159− , Columns (HKD a Expr) ~ GColumns (HKD a)
160− , HKDable a
161− , x ~ HKD a Expr
162− )
163− => ToExprs x (HKDT a)
164− where
165− toResult = (\(HKD a) -> a) . toHKD . (\(HKDT a) -> a)
166− fromResult = HKDT . fromHKD . HKD
167−
168−
169−fromHKD :: HKDable a => HKD a Result -> a
170−fromHKD = to . gunmap @Top (Proxy @(TColumn Result)) id . from
171−
172−
173−toHKD :: HKDable a => a -> HKD a Result
174−toHKD = to . gmap @Top (Proxy @(TColumn Result)) id . from
175−
176−
177−class Top_
178−instance Top_
179−
180−
181−data Top :: Type -> Exp Constraint
182−type instance Eval (Top _) = Top_
139+ grecord @(GMap (TColumn f) (Rep a))
183140
184141
142+type HKDable :: Type -> Constraint
185143class
186− ( Generic a
144+ ( Generic (Record a)
187145 , HTable (GColumns (HKD a))
188146 , KnownAlgebra (GAlgebra (Rep a))
189− , Eval (GGTable (GAlgebra (Rep a)) (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
190− , Eval (GGContext (GAlgebra (Rep a)) TUnreifyContext (GRecord (GMap (TColumn (Reify Result)) (Rep a)))) ~ Result
191− , GRecordable (GMap (TColumn (Reify Result)) (Rep a))
192− , GMappable Top (Rep a)
193− , GMappable (TTable (Reify Result)) (GMap (TColumn (Reify Result)) (Rep a))
194− , GMap TUnreify (GMap (TColumn (Reify Result)) (Rep a)) ~ GMap (TColumn Result) (Rep a)
147+ , Eval (GGTable (GAlgebra (Rep a)) (TTable Expr) TColumns TFromExprs (Eval (HKDRep a Expr)))
148+ , GMap TFromExprs (GRecord (GMap (TColumn Expr) (Rep a))) ~ Rep (Record a)
195149 )
196150 => HKDable a
197151instance
198− ( Generic a
152+ ( Generic (Record a)
199153 , HTable (GColumns (HKD a))
200154 , KnownAlgebra (GAlgebra (Rep a))
201− , Eval (GGTable (GAlgebra (Rep a)) (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
202− , Eval (GGContext (GAlgebra (Rep a)) TUnreifyContext (GRecord (GMap (TColumn (Reify Result)) (Rep a)))) ~ Result
203− , GRecordable (GMap (TColumn (Reify Result)) (Rep a))
204− , GMappable Top (Rep a)
205− , GMappable (TTable (Reify Result)) (GMap (TColumn (Reify Result)) (Rep a))
206− , GMap TUnreify (GMap (TColumn (Reify Result)) (Rep a)) ~ GMap (TColumn Result) (Rep a)
155+ , Eval (GGTable (GAlgebra (Rep a)) (TTable Expr) TColumns TFromExprs (Eval (HKDRep a Expr)))
156+ , GMap TFromExprs (GRecord (GMap (TColumn Expr) (Rep a))) ~ Rep (Record a)
207157 )
208158 => HKDable a
209159
210160
161+class Top_
162+instance Top_
163+
164+
165+data Top :: Type -> Exp Constraint
166+type instance Eval (Top _) = Top_
167+
168+
211169type BuildableHKD :: Type -> Symbol -> Constraint
212170class GGBuildable (GAlgebra (Rep a)) name (HKDRep a) => BuildableHKD a name
213171instance GGBuildable (GAlgebra (Rep a)) name (HKDRep a) => BuildableHKD a name
src/Rel8/Table/List.hs+11−38
@@ -16,27 +16,24 @@ module Rel8.Table.List
1616where
1717
1818-- base
19−import Control.Category ( id )
2019import Data.Functor.Identity ( Identity( Identity ) )
2120import Data.Kind ( Type )
22−import Data.Type.Equality ( (:~:)( Refl ), apply )
23−import Prelude hiding ( id )
21+import Prelude
2422
2523-- rel8
2624import Rel8.Expr ( Expr, Col( E, unE ) )
2725import Rel8.Expr.Array ( sappend, sempty, slistOf )
28−import Rel8.Schema.Context.Abstract ( Abstract, exclusivity, virtual )
2926import Rel8.Schema.Dict ( Dict( Dict ) )
3027import Rel8.Schema.HTable.List ( HListTable )
31−import Rel8.Schema.HTable.Vectorize ( happend, hempty, hvectorize )
28+import Rel8.Schema.HTable.Vectorize ( happend, hempty, hvectorize, hunvectorize )
3229import qualified Rel8.Schema.Kind as K
3330import Rel8.Schema.Name ( Col( N ), Name( Name ) )
3431import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
32+import Rel8.Schema.Result ( vectorizer, unvectorizer )
3533import Rel8.Schema.Spec ( SSpec(..) )
36−import Rel8.Schema.Reify ( hreify, hunreify )
3734import Rel8.Table
3835 ( Table, Context, Columns, fromColumns, toColumns
39− , reify, unreify, coherence, congruence
36+ , FromExprs, fromResult, toResult
4037 )
4138import Rel8.Table.Alternative
4239 ( AltTable, (<|>:)
@@ -45,7 +42,7 @@ import Rel8.Table.Alternative
4542import Rel8.Table.Eq ( EqTable, eqTable )
4643import Rel8.Table.Ord ( OrdTable, ordTable )
4744import Rel8.Table.Recontextualize ( Recontextualize )
48−import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
45+import Rel8.Table.Serialize ( ToExprs )
4946
5047
5148-- | A @ListTable@ value contains zero or more instances of @a@. You construct
@@ -55,39 +52,21 @@ newtype ListTable context a =
5552 ListTable (HListTable (Columns a) (Col (Context a)))
5653
5754
58−instance (Table context a, Abstract context, context ~ context') =>
55+instance (Table context a, context ~ context') =>
5956 Table context' (ListTable context a)
6057 where
6158 type Columns (ListTable context a) = HListTable (Columns a)
6259 type Context (ListTable context a) = Context a
60+ type FromExprs (ListTable context a) = [FromExprs a]
6361
6462 fromColumns = ListTable
6563 toColumns (ListTable a) = a
64+ fromResult = fmap (fromResult @_ @a) . hunvectorize unvectorizer
65+ toResult = hvectorize vectorizer . fmap (toResult @_ @a)
6666
67− reify proof@Refl (ListTable a) =
68− case coherence @context @a proof abstract of
69− Refl -> case congruence @context @a proof abstract of
70− Refl -> ListTable (hreify a)
71− where
72− abstract = exclusivity virtual
7367
74− unreify proof@Refl (ListTable a) =
75− case coherence @context @a proof abstract of
76− Refl -> case congruence @context @a proof abstract of
77− Refl -> ListTable (hunreify a)
78− where
79− abstract = exclusivity virtual
80−
81− coherence = coherence @context @a
82− congruence proof abstract = id `apply` congruence @context @a proof abstract
83−
84−
85−instance
86− ( Recontextualize from to a b
87− , Abstract from, from ~ from'
88− , Abstract to, to ~ to'
89− )
90− => Recontextualize from to (ListTable from' a) (ListTable to' b)
68+instance (Recontextualize from to a b, from ~ from', to ~ to') =>
69+ Recontextualize from to (ListTable from' a) (ListTable to' b)
9170
9271
9372instance (EqTable a, context ~ Expr) => EqTable (ListTable context a) where
@@ -108,14 +87,8 @@ instance (OrdTable a, context ~ Expr) => OrdTable (ListTable context a) where
10887 (Identity (ordTable @a))
10988
11089
111−type instance FromExprs (ListTable _context a) = [FromExprs a]
112−
113−
11490instance (ToExprs exprs a, context ~ Expr) =>
11591 ToExprs (ListTable context exprs) [a]
116− where
117− fromResult = fmap (fromResult @exprs) . fromColumns
118− toResult = toColumns . fmap (toResult @exprs)
11992
12093
12194instance context ~ Expr => AltTable (ListTable context) where
src/Rel8/Table/Maybe.hs+22−25
@@ -22,11 +22,10 @@ module Rel8.Table.Maybe
2222where
2323
2424-- base
25−import Control.Category ( id )
25+import Data.Functor ( ($>) )
2626import Data.Kind ( Type )
27−import Data.Maybe ( isJust )
28−import Data.Type.Equality ( apply )
29−import Prelude hiding ( id, null, undefined )
27+import Data.Maybe ( fromMaybe, isJust )
28+import Prelude hiding ( null, undefined )
3029
3130-- comonad
3231import Control.Comonad ( extract )
@@ -38,7 +37,6 @@ import Rel8.Expr.Aggregate ( groupByExpr )
3837import Rel8.Expr.Bool ( boolExpr )
3938import Rel8.Expr.Null ( isNull, isNonNull, null, nullify )
4039import Rel8.Kind.Context ( Reifiable )
41−import Rel8.Schema.Context.Abstract ( Abstract )
4240import Rel8.Schema.Dict ( Dict( Dict ) )
4341import qualified Rel8.Schema.Kind as K
4442import Rel8.Schema.HTable.Identity ( HIdentity(..) )
@@ -47,10 +45,11 @@ import Rel8.Schema.HTable.Maybe ( HMaybeTable(..) )
4745import Rel8.Schema.Name ( Col( N ), Name )
4846import Rel8.Schema.Null ( Nullity( Null, NotNull ), Sql, nullable )
4947import qualified Rel8.Schema.Null as N
48+import Rel8.Schema.Result ( Col( R ) )
5049import Rel8.Schema.Spec ( Spec( Spec ) )
5150import Rel8.Table
5251 ( Table, Columns, Context, fromColumns, toColumns
53− , coherence, congruence, reify, unreify
52+ , FromExprs, fromResult, toResult
5453 )
5554import Rel8.Table.Alternative
5655 ( AltTable, (<|>:)
@@ -61,10 +60,10 @@ import Rel8.Table.Eq ( EqTable, eqTable )
6160import Rel8.Table.Ord ( OrdTable, ordTable )
6261import Rel8.Table.Nullify ( Nullify, aggregateNullify, guard )
6362import Rel8.Table.Recontextualize ( Recontextualize )
64−import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
63+import Rel8.Table.Serialize ( ToExprs )
6564import Rel8.Table.Undefined ( undefined )
6665import Rel8.Type ( DBType )
67−import Rel8.Type.Tag ( MaybeTag )
66+import Rel8.Type.Tag ( MaybeTag( IsJust ) )
6867
6968-- semigroupoids
7069import Data.Functor.Apply ( Apply, (<.>) )
@@ -129,14 +128,12 @@ instance (context ~ Expr, Table Expr a, Semigroup a) =>
129128 mempty = nothingTable
130129
131130
132−instance
133− ( Table context a
134− , Reifiable context, Abstract context, context ~ context'
135− )
136− => Table context' (MaybeTable context a)
131+instance (Table context a, Reifiable context, context ~ context') =>
132+ Table context' (MaybeTable context a)
137133 where
138134 type Columns (MaybeTable context a) = HMaybeTable (Columns a)
139135 type Context (MaybeTable context a) = Context a
136+ type FromExprs (MaybeTable context a) = Maybe (FromExprs a)
140137
141138 toColumns MaybeTable {tag, just} = HMaybeTable
142139 { htag = hlabel $ HIdentity tag
@@ -148,16 +145,22 @@ instance
148145 , just = fromColumns $ hunlabel hjust
149146 }
150147
151− reify proof (MaybeTable tag a) = MaybeTable tag (reify proof a)
152− unreify proof (MaybeTable tag a) = MaybeTable tag (unreify proof a)
153− coherence = coherence @context @a
154− congruence proof abstract = id `apply` congruence @context @a proof abstract
148+ toResult ma = HMaybeTable
149+ { htag = hlabel (HIdentity (R (IsJust <$ ma)))
150+ , hjust = hlabel (toResult @_ @(Nullify context a) ma)
151+ }
152+
153+ fromResult HMaybeTable {htag, hjust} = case hunlabel htag of
154+ HType (R tag) -> tag $>
155+ fromMaybe err (fromResult @_ @(Nullify context a) (hunlabel hjust))
156+ where
157+ err = error "Maybe.fromColumns: mismatch between tag and data"
155158
156159
157160instance
158161 ( Recontextualize from to a b
159− , Reifiable from, Abstract from, from ~ from'
160− , Reifiable to, Abstract to, to ~ to'
162+ , Reifiable from, from ~ from'
163+ , Reifiable to, to ~ to'
161164 )
162165 => Recontextualize from to (MaybeTable from' a) (MaybeTable to' b)
163166
@@ -176,14 +179,8 @@ instance (OrdTable a, context ~ Expr) => OrdTable (MaybeTable context a) where
176179 }
177180
178181
179−type instance FromExprs (MaybeTable _context a) = Maybe (FromExprs a)
180−
181−
182182instance (ToExprs exprs a, context ~ Expr) =>
183183 ToExprs (MaybeTable context exprs) (Maybe a)
184− where
185− fromResult = fmap (fromResult @exprs) . fromColumns
186− toResult = toColumns . fmap (toResult @exprs)
187184
188185
189186-- | Check if a @MaybeTable@ is absent of any row. Like 'Data.Maybe.isNothing'.
src/Rel8/Table/NonEmpty.hs+10−37
@@ -16,34 +16,31 @@ module Rel8.Table.NonEmpty
1616where
1717
1818-- base
19−import Control.Category ( id )
2019import Data.Functor.Identity ( Identity( Identity ) )
2120import Data.Kind ( Type )
2221import Data.List.NonEmpty ( NonEmpty )
23−import Data.Type.Equality ( (:~:)( Refl ), apply )
2422import Prelude hiding ( id )
2523
2624-- rel8
2725import Rel8.Expr ( Expr, Col( E, unE ) )
2826import Rel8.Expr.Array ( sappend1, snonEmptyOf )
29−import Rel8.Schema.Context.Abstract ( Abstract, exclusivity, virtual )
3027import Rel8.Schema.Dict ( Dict( Dict ) )
3128import Rel8.Schema.HTable.NonEmpty ( HNonEmptyTable )
32−import Rel8.Schema.HTable.Vectorize ( happend, hvectorize )
29+import Rel8.Schema.HTable.Vectorize ( happend, hvectorize, hunvectorize )
3330import qualified Rel8.Schema.Kind as K
3431import Rel8.Schema.Name ( Col( N ), Name( Name ) )
3532import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
36−import Rel8.Schema.Reify ( hreify, hunreify )
33+import Rel8.Schema.Result ( vectorizer, unvectorizer )
3734import Rel8.Schema.Spec ( SSpec(..) )
3835import Rel8.Table
3936 ( Table, Context, Columns, fromColumns, toColumns
40− , reify, unreify, coherence, congruence
37+ , FromExprs, fromResult, toResult
4138 )
4239import Rel8.Table.Alternative ( AltTable, (<|>:) )
4340import Rel8.Table.Eq ( EqTable, eqTable )
4441import Rel8.Table.Ord ( OrdTable, ordTable )
4542import Rel8.Table.Recontextualize ( Recontextualize )
46−import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
43+import Rel8.Table.Serialize ( ToExprs )
4744
4845
4946-- | A @NonEmptyTable@ value contains one or more instances of @a@. You
@@ -53,39 +50,21 @@ newtype NonEmptyTable context a =
5350 NonEmptyTable (HNonEmptyTable (Columns a) (Col (Context a)))
5451
5552
56−instance (Table context a, Abstract context, context ~ context') =>
53+instance (Table context a, context ~ context') =>
5754 Table context' (NonEmptyTable context a)
5855 where
5956 type Columns (NonEmptyTable context a) = HNonEmptyTable (Columns a)
6057 type Context (NonEmptyTable context a) = Context a
58+ type FromExprs (NonEmptyTable context a) = NonEmpty (FromExprs a)
6159
6260 fromColumns = NonEmptyTable
6361 toColumns (NonEmptyTable a) = a
62+ fromResult = fmap (fromResult @_ @a) . hunvectorize unvectorizer
63+ toResult = hvectorize vectorizer . fmap (toResult @_ @a)
6464
65− reify proof@Refl (NonEmptyTable a) =
66− case coherence @context @a proof abstract of
67− Refl -> case congruence @context @a proof abstract of
68− Refl -> NonEmptyTable (hreify a)
69− where
70− abstract = exclusivity virtual
7165
72− unreify proof@Refl (NonEmptyTable a) =
73− case coherence @context @a proof abstract of
74− Refl -> case congruence @context @a proof abstract of
75− Refl -> NonEmptyTable (hunreify a)
76− where
77− abstract = exclusivity virtual
78−
79− coherence = coherence @context @a
80− congruence proof abstract = id `apply` congruence @context @a proof abstract
81−
82−
83−instance
84− ( Recontextualize from to a b
85− , Abstract from, from ~ from'
86− , Abstract to, to ~ to'
87− )
88− => Recontextualize from to (NonEmptyTable from' a) (NonEmptyTable to' b)
66+instance (Recontextualize from to a b, from ~ from', to ~ to') =>
67+ Recontextualize from to (NonEmptyTable from' a) (NonEmptyTable to' b)
8968
9069
9170instance (EqTable a, context ~ Expr) =>
@@ -110,14 +89,8 @@ instance (OrdTable a, context ~ Expr) =>
11089 (Identity (ordTable @a))
11190
11291
113−type instance FromExprs (NonEmptyTable _context a) = NonEmpty (FromExprs a)
114−
115−
11692instance (ToExprs exprs a, context ~ Expr) =>
11793 ToExprs (NonEmptyTable context exprs) (NonEmpty a)
118− where
119− fromResult = fmap (fromResult @exprs) . fromColumns
120− toResult = toColumns . fmap (toResult @exprs)
12194
12295
12396instance context ~ Expr => AltTable (NonEmptyTable context) where
src/Rel8/Table/Nullify.hs+15−37
@@ -17,11 +17,9 @@ where
1717
1818-- base
1919import Control.Applicative ( liftA2 )
20−import Control.Category ( id )
2120import Data.Functor.Identity ( runIdentity )
2221import Data.Kind ( Type )
23−import Data.Type.Equality ( (:~:)( Refl ), apply )
24−import Prelude hiding ( id )
22+import Prelude
2523
2624-- comonad
2725import Control.Comonad ( Comonad, duplicate, extract, ComonadApply, (<@>) )
@@ -31,10 +29,9 @@ import Rel8.Aggregate ( Aggregate )
3129import Rel8.Expr ( Expr )
3230import Rel8.Kind.Context ( Reifiable, contextSing )
3331import Rel8.Schema.Context ( Col )
34−import Rel8.Schema.Context.Abstract ( Abstract, exclusivity, virtual )
3532import Rel8.Schema.Context.Nullify
3633 ( Nullifiability( NAggregate, NExpr )
37− , NonNullifiability( NNReify )
34+ , NonNullifiability
3835 , Nullifiable, nullifiability
3936 , nullifiableOrNot, absurd
4037 , guarder
@@ -43,13 +40,13 @@ import Rel8.Schema.Context.Nullify
4340 )
4441import Rel8.Schema.Dict ( Dict( Dict ) )
4542import Rel8.Schema.HTable ( HTable )
46−import Rel8.Schema.HTable.Nullify ( HNullify, hnullify, hunnullify, hguard )
43+import Rel8.Schema.HTable.Nullify ( HNullify, hnulls, hnullify, hunnullify, hguard )
4744import qualified Rel8.Schema.Kind as K
48−import Rel8.Schema.Reify ( hreify, hunreify )
45+import qualified Rel8.Schema.Result as R
4946import Rel8.Schema.Spec ( Spec( Spec ) )
5047import Rel8.Table
5148 ( Table, Columns, Context, toColumns, fromColumns
52− , reify, unreify, coherence, congruence
49+ , FromExprs, fromResult, toResult
5350 )
5451import Rel8.Table.Eq ( EqTable, eqTable )
5552import Rel8.Table.Ord ( OrdTable, ordTable )
@@ -124,14 +121,12 @@ instance Nullifiable context => ComonadApply (Nullify context) where
124121 (<@>) = (<.>)
125122
126123
127−instance
128− ( Table context a
129− , Reifiable context, Abstract context, context ~ context'
130− )
131− => Table context' (Nullify context a)
124+instance (Table context a, Reifiable context, context ~ context') =>
125+ Table context' (Nullify context a)
132126 where
133127 type Columns (Nullify context a) = HNullify (Columns a)
134128 type Context (Nullify context a) = Context a
129+ type FromExprs (Nullify context a) = Maybe (FromExprs a)
135130
136131 fromColumns = case nullifiableOrNot contextSing of
137132 Left notNullifiable -> Fields notNullifiable
@@ -145,34 +140,17 @@ instance
145140 Table nullifiable a -> hnullify (nullifier nullifiable) (toColumns a)
146141 Fields _ a -> a
147142
148− reify proof@Refl = \case
149− Table nullifiable a -> Table nullifiable (reify proof a)
150− Fields notNullifiable a -> case notNullifiable of
151− NNReify (_ :: NonNullifiability ctx) ->
152− case coherence @context @a proof abstract of
153− Refl -> case congruence @context @a proof abstract of
154− Refl -> Fields notNullifiable (hreify a)
155− where
156− abstract = exclusivity (virtual @ctx)
157−
158− unreify proof@Refl = \case
159− Table nullifiable a -> Table nullifiable (unreify proof a)
160− Fields notNullifiable a -> case notNullifiable of
161− NNReify (_ :: NonNullifiability ctx) ->
162− case coherence @context @a proof abstract of
163− Refl -> case congruence @context @a proof abstract of
164− Refl -> Fields notNullifiable (hunreify a)
165− where
166− abstract = exclusivity (virtual @ctx)
167−
168− coherence = coherence @context @a
169− congruence proof abstract = id `apply` congruence @context @a proof abstract
143+ fromResult = fmap (fromResult @_ @a) . hunnullify R.unnullifier
144+
145+ toResult =
146+ maybe (hnulls (const R.null)) (hnullify R.nullifier) .
147+ fmap (toResult @_ @a)
170148
171149
172150instance
173151 ( Recontextualize from to a b
174− , Reifiable from, Abstract from, from ~ from'
175− , Reifiable to, Abstract to, to ~ to'
152+ , Reifiable from, from ~ from'
153+ , Reifiable to, to ~ to'
176154 )
177155 => Recontextualize from' to' (Nullify from a) (Nullify to b)
178156
src/Rel8/Table/Ord.hs+6−12
@@ -31,11 +31,7 @@ import Rel8.Expr.Eq ( (==.) )
3131import Rel8.Expr.Ord ( (<.), (>.) )
3232import Rel8.FCF ( Eval, Exp )
3333import Rel8.Generic.Record ( Record )
34−import Rel8.Generic.Table
35− ( GGTable, GGColumns, ggtable
36− , GAlgebra
37− )
38−import Rel8.Kind.Algebra ( KnownAlgebra )
34+import Rel8.Generic.Table.Record ( GTable, GColumns, gtable )
3935import Rel8.Schema.Dict ( Dict( Dict ) )
4036import Rel8.Schema.HTable
4137 ( HTable, HConstrainTable
@@ -44,7 +40,7 @@ import Rel8.Schema.HTable
4440import Rel8.Schema.HTable.Identity ( HIdentity( HType ) )
4541import Rel8.Schema.Null (Sql)
4642import Rel8.Schema.Spec.Constrain ( ConstrainSpec )
47−import Rel8.Table ( Columns, toColumns, TColumns )
43+import Rel8.Table ( Columns, toColumns, TColumns, TFromExprs )
4844import Rel8.Table.Bool ( bool )
4945import Rel8.Table.Eq ( EqTable )
5046import Rel8.Type.Eq ( DBEq )
@@ -59,19 +55,17 @@ class EqTable a => OrdTable a where
5955 ordTable :: Columns a (Dict (ConstrainSpec (Sql DBOrd)))
6056
6157 default ordTable ::
62− ( KnownAlgebra (GAlgebra (Rep (Record a)))
63− , Eval (GGTable (GAlgebra (Rep (Record a))) TOrdTable TColumns (Dict (ConstrainSpec (Sql DBOrd))) (Rep (Record a)))
64− , Columns a ~ Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))
58+ ( GTable TOrdTable TColumns TFromExprs (Rep (Record a))
59+ , Columns a ~ GColumns TColumns (Rep (Record a))
6560 )
6661 => Columns a (Dict (ConstrainSpec (Sql DBOrd)))
6762 ordTable =
68− ggtable
69− @(GAlgebra (Rep (Record a)))
63+ gtable
7064 @TOrdTable
7165 @TColumns
66+ @TFromExprs
7267 @(Rep (Record a))
7368 table
74− (\_ Dict -> Dict)
7569 where
7670 table (_ :: proxy x) = ordTable @x
7771
src/Rel8/Table/Recontextualize.hs+1−40
@@ -12,23 +12,15 @@ module Rel8.Table.Recontextualize
1212where
1313
1414-- base
15−import Data.Functor.Identity ( Identity )
1615import Data.Kind ( Constraint, Type )
17−import Data.List.NonEmpty ( NonEmpty)
18−import Prelude
16+import Prelude ()
1917
2018-- rel8
2119import Rel8.Schema.Context ( Col )
2220import Rel8.Schema.HTable ( HTable )
2321import qualified Rel8.Schema.Kind as K
24−import Rel8.Schema.Null ( Sql )
25−import Rel8.Schema.Result ( Result )
2622import Rel8.Schema.Spec ( KnownSpec )
2723import Rel8.Table ( Table, Congruent )
28−import Rel8.Type ( DBType )
29−
30−-- these
31−import Data.These ( These)
3224
3325
3426-- | @Recontextualize from to a b@ is evidence that the types @a@ and @b@ are
@@ -49,43 +41,12 @@ class
4941 , b from -> a
5042
5143
52−instance Sql DBType a => Recontextualize Result Result (Identity a) (Identity a)
53−
54−
5544instance KnownSpec spec => Recontextualize from to (Col from spec) (Col to spec)
5645
5746
5847instance HTable t => Recontextualize from to (t (Col from)) (t (Col to))
5948
6049
61−instance
62− ( Recontextualize from to a1 b1
63− , Recontextualize from to a2 b2
64− , from ~ Result, to ~ Result
65− )
66− => Recontextualize from to (Either a1 a2) (Either b1 b2)
67−
68−
69−instance (Recontextualize from to a b, from ~ Result, to ~ Result) =>
70− Recontextualize from to [a] [b]
71−
72−
73−instance (Recontextualize from to a b, from ~ Result, to ~ Result) =>
74− Recontextualize from to (Maybe a) (Maybe b)
75−
76−
77−instance (Recontextualize from to a b, from ~ Result, to ~ Result) =>
78− Recontextualize from to (NonEmpty a) (NonEmpty b)
79−
80−
81−instance
82− ( Recontextualize from to a1 b1
83− , Recontextualize from to a2 b2
84− , from ~ Result, to ~ Result
85− )
86− => Recontextualize from to (These a1 a2) (These b1 b2)
87−
88−
8950instance
9051 ( Recontextualize from to a1 b1
9152 , Recontextualize from to a2 b2
src/Rel8/Table/Rel8able.hs+21−71
@@ -1,6 +1,6 @@
11{-# language DataKinds #-}
22{-# language FlexibleInstances #-}
3−{-# language FunctionalDependencies #-}
3+{-# language MultiParamTypeClasses #-}
44{-# language ScopedTypeVariables #-}
55{-# language StandaloneKindSignatures #-}
66{-# language TypeApplications #-}
@@ -15,71 +15,50 @@ module Rel8.Table.Rel8able
1515where
1616
1717-- base
18−import Data.Kind ( Constraint, Type )
19−import Data.Type.Equality ( (:~:)( Refl ) )
20−import Prelude
18+import Prelude ()
2119
2220-- rel8
2321import Rel8.Expr ( Expr )
2422import qualified Rel8.Kind.Algebra as K
25−import Rel8.Kind.Context
26− ( SContext( SReify )
27− , Reifiable, contextSing
28− , sReifiable
29− )
3023import Rel8.Generic.Rel8able
3124 ( Rel8able, Algebra
3225 , GColumns, gfromColumns, gtoColumns
33− , greify, gunreify
26+ , GFromExprs, gfromResult, gtoResult
3427 )
35−import Rel8.Schema.Context ( Col )
36−import Rel8.Schema.Dict ( Dict( Dict ) )
28+import Rel8.Schema.Context.Virtual ( Virtual, virtual )
3729import qualified Rel8.Schema.Kind as K
3830import Rel8.Schema.HTable ( HConstrainTable, hdicts )
3931import Rel8.Schema.Null ( Sql )
40−import Rel8.Schema.Reify ( hreify, hunreify, UnwrapReify )
4132import Rel8.Schema.Result ( Result )
4233import Rel8.Table
4334 ( Table, Columns, Context, Congruent, fromColumns, toColumns
44− , Unreify, reify, unreify, coherence, congruence
35+ , FromExprs, fromResult, toResult
4536 )
4637import Rel8.Schema.Spec.Constrain ( ConstrainSpec )
47−import Rel8.Table.ADT ( ADT( ADT ), ADTable, fromADT, toADT )
38+import Rel8.Table.ADT ( ADT )
4839import Rel8.Table.Eq ( EqTable, eqTable )
49−import Rel8.Table.HKD ( HKD )
5040import Rel8.Table.Ord ( OrdTable, ordTable )
5141import Rel8.Table.Recontextualize ( Recontextualize )
52−import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
42+import Rel8.Table.Serialize ( ToExprs )
5343import Rel8.Type.Eq ( DBEq )
5444import Rel8.Type.Ord ( DBOrd )
5545
5646
57−instance (Rel8able t, Reifiable context) =>
58− Table context (t context)
59− where
47+instance (Rel8able t, Virtual context) => Table context (t context) where
6048 type Columns (t context) = GColumns t
6149 type Context (t context) = context
62− type Unreify (t context) = t (UnwrapReify context)
63−
64− fromColumns = gunreify . gfromColumns . hreify
65− toColumns = hunreify . gtoColumns . greify
66−
67− reify Refl = case contextSing @context of
68− SReify context -> case sReifiable context of
69− Dict -> greify
70−
71− unreify Refl = case contextSing @context of
72− SReify context -> case sReifiable context of
73− Dict -> gunreify
50+ type FromExprs (t context) = GFromExprs t
7451
75− coherence Refl _ = Refl
76− congruence Refl _ = Refl
52+ fromColumns = gfromColumns virtual
53+ toColumns = gtoColumns virtual
54+ fromResult = gfromResult @t
55+ toResult = gtoResult @t
7756
7857
7958instance
8059 ( Rel8able t
81− , Reifiable from
82− , Reifiable to
60+ , Virtual from
61+ , Virtual to
8362 , Congruent (t from) (t to)
8463 )
8564 => Recontextualize from to (t from) (t to)
@@ -106,44 +85,15 @@ instance
10685 ordTable = hdicts @(Columns (t context)) @(ConstrainSpec (Sql DBOrd))
10786
10887
109−type instance FromExprs (t Expr) = FromExprs' t
110−
111−
11288instance
113− ( x ~ t' Expr
89+ ( Rel8able t', t' ~ Choose (Algebra t) t
90+ , x ~ t' Expr
11491 , result ~ Result
115− , ToExprs' (Algebra t) t' t
11692 )
11793 => ToExprs x (t result)
118− where
119− fromResult = fromResult' @(Algebra t) @t'
120− toResult = toResult' @(Algebra t) @t'
121−
12294
123−type FromExprs' :: K.Rel8able -> Type
124−type family FromExprs' t where
125− FromExprs' (ADT t) = t Result
126− FromExprs' (HKD a) = a
127− FromExprs' t = t Result
12895
129−
130−type ToExprs' :: K.Algebra -> K.Rel8able -> K.Rel8able -> Constraint
131−class (algebra ~ Algebra t, Rel8able t') =>
132− ToExprs' algebra t' t | algebra t -> t'
133− where
134− fromResult' :: GColumns t' (Col Result) -> t Result
135− toResult' :: t Result -> GColumns t' (Col Result)
136−
137−
138−instance (Algebra t ~ 'K.Product, Rel8able t, t ~ t') =>
139− ToExprs' 'K.Product t' t
140− where
141− fromResult' = fromColumns
142− toResult' = toColumns
143−
144−
145−instance (Algebra t ~ 'K.Sum, ADTable t, t' ~ ADT t) =>
146− ToExprs' 'K.Sum t' t
147− where
148− fromResult' = fromADT . ADT
149− toResult' = (\(ADT a) -> a) . toADT
96+type Choose :: K.Algebra -> K.Rel8able -> K.Rel8able
97+type family Choose algebra t where
98+ Choose 'K.Sum t = ADT t
99+ Choose 'K.Product t = t
src/Rel8/Table/Serialize.hs+12−105
@@ -1,7 +1,4 @@
11{-# language AllowAmbiguousTypes #-}
2−{-# language DataKinds #-}
3−{-# language DefaultSignatures #-}
4−{-# language DisambiguateRecordFields #-}
52{-# language FlexibleContexts #-}
63{-# language FlexibleInstances #-}
74{-# language FunctionalDependencies #-}
@@ -10,20 +7,17 @@
107{-# language StandaloneKindSignatures #-}
118{-# language TypeApplications #-}
129{-# language TypeFamilies #-}
13−{-# language TypeOperators #-}
1410{-# language UndecidableInstances #-}
1511
1612module Rel8.Table.Serialize
1713 ( Serializable, lit, parse
18− , ToExprs(..), FromExprs
19− , TToExprs
14+ , ToExprs
2015 )
2116where
2217
2318-- base
2419import Data.Kind ( Constraint, Type )
2520import Data.List.NonEmpty ( NonEmpty )
26−import GHC.Generics ( Generic, Rep, from, to )
2721import Prelude
2822
2923-- hasql
@@ -32,19 +26,11 @@ import qualified Hasql.Decoders as Hasql
3226-- rel8
3327import Rel8.Expr ( Expr, Col( E ) )
3428import Rel8.Expr.Serialize ( slitExpr, sparseValue )
35−import Rel8.FCF ( Eval, Exp )
36−import Rel8.Generic.Record ( Record(..) )
37−import Rel8.Generic.Table
38− ( GGToExprs, GGColumns, ggfromResult, ggtoResult
39− , GAlgebra
40− )
41−import Rel8.Kind.Algebra ( KnownAlgebra )
4229import Rel8.Schema.HTable ( HTable, htabulate, htabulateA, hfield, hspecs )
43−import Rel8.Schema.HTable.Identity ( HIdentity( HType ) )
4430import Rel8.Schema.Null ( NotNull, Sql )
4531import Rel8.Schema.Result ( Col( R ), Result )
4632import Rel8.Schema.Spec ( SSpec(..), KnownSpec )
47−import Rel8.Table ( Table, Columns, fromColumns, toColumns, TColumns )
33+import Rel8.Table ( Table, fromColumns, FromExprs, fromResult, toResult )
4834import Rel8.Type ( DBType )
4935
5036-- semigroupoids
@@ -53,71 +39,21 @@ import Data.Functor.Apply ( WrappedApplicative(..) )
5339
5440-- | @ToExprs exprs a@ is evidence that the types @exprs@ and @a@ describe
5541-- essentially the same type, but @exprs@ is in the 'Expr' context, and @a@ is
56−-- in the 'Result' context.
42+-- a normal Haskell type.
5743type ToExprs :: Type -> Type -> Constraint
58−class Table Expr exprs => ToExprs exprs a where
59− fromResult :: Columns exprs (Col Result) -> a
60− toResult :: a -> Columns exprs (Col Result)
61−
62− default fromResult ::
63− ( Generic (Record a)
64− , KnownAlgebra (GAlgebra (Rep (Record exprs)))
65− , Eval (GGToExprs (GAlgebra (Rep (Record exprs))) TToExprs TColumns (Rep (Record exprs)) (Rep (Record a)))
66− , Columns exprs ~ Eval (GGColumns (GAlgebra (Rep (Record exprs))) TColumns (Rep (Record exprs)))
67− )
68− => Columns exprs (Col Result) -> a
69− fromResult =
70− unrecord .
71− to .
72− ggfromResult
73− @(GAlgebra (Rep (Record exprs)))
74− @TToExprs
75− @TColumns
76− @(Rep (Record exprs))
77− (\(_ :: proxy expr) -> fromResult @expr)
78−
79− default toResult ::
80− ( Generic (Record a)
81− , KnownAlgebra (GAlgebra (Rep (Record exprs)))
82− , Eval (GGToExprs (GAlgebra (Rep (Record exprs))) TToExprs TColumns (Rep (Record exprs)) (Rep (Record a)))
83− , Columns exprs ~ Eval (GGColumns (GAlgebra (Rep (Record exprs))) TColumns (Rep (Record exprs)))
84− )
85− => a -> Columns exprs (Col Result)
86− toResult =
87− ggtoResult
88− @(GAlgebra (Rep (Record exprs)))
89− @TToExprs
90− @TColumns
91− @(Rep (Record exprs))
92− (\(_ :: proxy expr) -> toResult @expr) .
93− from .
94− Record
95−
96−
97−data TToExprs :: Type -> Type -> Exp Constraint
98−type instance Eval (TToExprs exprs a) = ToExprs exprs a
99−
100−
101−instance {-# OVERLAPPABLE #-} (Sql DBType a, x ~ Expr a) => ToExprs x a where
102− fromResult (HType (R a)) = a
103− toResult = HType . R
104−
105−
106−instance (Sql DBType a, x ~ [a]) => ToExprs (Expr x) [a] where
107− fromResult (HType (R a)) = a
108− toResult = HType . R
44+class Table Expr exprs => ToExprs exprs a
45+
46+
47+instance {-# OVERLAPPABLE #-} (Sql DBType a, x ~ Expr a) => ToExprs x a
48+
49+
50+instance (Sql DBType a, x ~ [a]) => ToExprs (Expr x) [a]
10951
11052
11153instance (Sql DBType a, NotNull a, x ~ Maybe a) => ToExprs (Expr x) (Maybe a)
112− where
113− fromResult (HType (R a)) = a
114− toResult = HType . R
11554
11655
11756instance (Sql DBType a, NotNull a, x ~ NonEmpty a) => ToExprs (Expr x) (NonEmpty a)
118− where
119− fromResult (HType (R a)) = a
120− toResult = HType . R
12157
12258
12359instance (ToExprs exprs1 a, ToExprs exprs2 b, x ~ (exprs1, exprs2)) =>
@@ -181,39 +117,10 @@ instance
181117
182118instance (HTable t, result ~ Col Result, x ~ t (Col Expr)) =>
183119 ToExprs x (t result)
184− where
185− fromResult = id
186− toResult = id
187120
188121
189122instance (KnownSpec spec, x ~ Col Expr spec) =>
190123 ToExprs x (Col Result spec)
191− where
192− fromResult = fromColumns
193− toResult = toColumns
194−
195−
196−-- | The @FromExprs@ type function maps a type in the @Expr@ context to the
197−-- corresponding type in the @Result@ context.
198−type FromExprs :: Type -> Type
199−type family FromExprs a
200−type instance FromExprs (Expr a) = a
201−type instance FromExprs (Col Expr spec) = Col Result spec
202−type instance FromExprs (a, b) = (FromExprs a, FromExprs b)
203−type instance FromExprs (a, b, c) = (FromExprs a, FromExprs b, FromExprs c)
204−type instance FromExprs (a, b, c, d) =
205− (FromExprs a, FromExprs b, FromExprs c, FromExprs d)
206−type instance FromExprs (a, b, c, d, e) =
207− (FromExprs a, FromExprs b, FromExprs c, FromExprs d, FromExprs e)
208−type instance FromExprs (a, b, c, d, e, f) =
209− ( FromExprs a, FromExprs b, FromExprs c, FromExprs d, FromExprs e
210− , FromExprs f
211− )
212−type instance FromExprs (a, b, c, d, e, f, g) =
213− ( FromExprs a, FromExprs b, FromExprs c, FromExprs d, FromExprs e
214− , FromExprs f, FromExprs g
215− )
216−type instance FromExprs (t (Col Expr)) = t (Col Result)
217124
218125
219126-- | @Serializable@ witnesses the one-to-one correspondence between the type
@@ -228,11 +135,11 @@ instance {-# OVERLAPPING #-} Sql DBType a => Serializable (Expr a) a
228135-- | Use @lit@ to turn literal Haskell values into expressions. @lit@ is
229136-- capable of lifting single @Expr@s to full tables.
230137lit :: forall exprs a. Serializable exprs a => a -> exprs
231−lit = fromColumns . litHTable . toResult @exprs
138+lit = fromColumns . litHTable . toResult @_ @exprs
232139
233140
234141parse :: forall exprs a. Serializable exprs a => Hasql.Row a
235−parse = fromResult @exprs <$> parseHTable
142+parse = fromResult @_ @exprs <$> parseHTable
236143
237144
238145litHTable :: HTable t => t (Col Result) -> t (Col Expr)
src/Rel8/Table/These.hs+45−36
@@ -26,12 +26,10 @@ module Rel8.Table.These
2626where
2727
2828-- base
29−import Control.Category ( id )
3029import Data.Bifunctor ( Bifunctor, bimap )
3130import Data.Kind ( Type )
3231import Data.Maybe ( isJust )
33−import Data.Type.Equality ( apply )
34−import Prelude hiding ( id, undefined )
32+import Prelude hiding ( undefined )
3533
3634-- rel8
3735import Rel8.Aggregate ( Aggregate )
@@ -39,17 +37,17 @@ import Rel8.Expr ( Expr )
3937import Rel8.Expr.Bool ( (&&.), not_ )
4038import Rel8.Expr.Null ( isNonNull )
4139import Rel8.Kind.Context ( Reifiable )
42−import Rel8.Schema.Context.Abstract ( Abstract )
4340import Rel8.Schema.Context.Nullify ( Nullifiable )
4441import Rel8.Schema.Dict ( Dict( Dict ) )
45−import Rel8.Schema.HTable.Label ( hlabel, hunlabel )
42+import Rel8.Schema.HTable.Label ( hlabel, hrelabel, hunlabel )
4643import Rel8.Schema.HTable.Identity ( HIdentity(..) )
44+import Rel8.Schema.HTable.Maybe ( HMaybeTable(..) )
4745import Rel8.Schema.HTable.These ( HTheseTable(..) )
4846import qualified Rel8.Schema.Kind as K
4947import Rel8.Schema.Name ( Name )
5048import Rel8.Table
5149 ( Table, Columns, Context, fromColumns, toColumns
52− , coherence, congruence, reify, unreify
50+ , FromExprs, fromResult, toResult
5351 )
5452import Rel8.Table.Eq ( EqTable, eqTable )
5553import Rel8.Table.Maybe
@@ -62,7 +60,7 @@ import Rel8.Table.Maybe
6260import Rel8.Table.Nullify ( Nullify, guard )
6361import Rel8.Table.Ord ( OrdTable, ordTable )
6462import Rel8.Table.Recontextualize ( Recontextualize )
65−import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
63+import Rel8.Table.Serialize ( ToExprs )
6664import Rel8.Table.Undefined ( undefined )
6765import Rel8.Type.Tag ( MaybeTag )
6866
@@ -71,7 +69,8 @@ import Data.Functor.Apply ( Apply, (<.>) )
7169import Data.Functor.Bind ( Bind, (>>-) )
7270
7371-- these
74−import Data.These ( These )
72+import Data.These ( These( This, That, These ) )
73+import Data.These.Combinators ( justHere, justThere )
7574
7675
7776-- | @TheseTable a b@ is a Rel8 table that contains either the table @a@, the
@@ -139,12 +138,14 @@ instance (context ~ Expr, Table Expr a, Table Expr b, Semigroup a, Semigroup b)
139138
140139instance
141140 ( Table context a, Table context b
142− , Reifiable context, Abstract context, context ~ context'
141+ , Reifiable context, context ~ context'
143142 )
144143 => Table context' (TheseTable context a b)
145144 where
146145 type Columns (TheseTable context a b) = HTheseTable (Columns a) (Columns b)
147146 type Context (TheseTable context a b) = Context a
147+ type FromExprs (TheseTable context a b) =
148+ These (FromExprs a) (FromExprs b)
148149
149150 toColumns TheseTable {here, there} = HTheseTable
150151 { hhereTag = hlabel $ HIdentity $ tag here
@@ -166,27 +167,46 @@ instance
166167 }
167168 }
168169
169− reify proof TheseTable {here, there} = TheseTable
170− { here = reify proof here
171− , there = reify proof there
170+ toResult tables = HTheseTable
171+ { hhereTag = hrelabel hhereTag
172+ , hhere = hrelabel hhere
173+ , hthereTag = hrelabel hthereTag
174+ , hthere = hrelabel hthere
172175 }
173− unreify proof TheseTable {here, there} = TheseTable
174− { here = unreify proof here
175− , there = unreify proof there
176− }
177−
178− coherence = coherence @context @a
179− congruence proof abstract =
180− id `apply`
181− congruence @context @a proof abstract `apply`
182− congruence @context @b proof abstract
176+ where
177+ HMaybeTable
178+ { htag = hhereTag
179+ , hjust = hhere
180+ } = toResult @_ @(MaybeTable context a) (justHere tables)
181+ HMaybeTable
182+ { htag = hthereTag
183+ , hjust = hthere
184+ } = toResult @_ @(MaybeTable context b) (justThere tables)
185+
186+ fromResult HTheseTable {hhereTag, hhere, hthereTag, hthere} =
187+ case (here, there) of
188+ (Just a, Nothing) -> This a
189+ (Nothing, Just b) -> That b
190+ (Just a, Just b) -> These a b
191+ _ -> error "These.fromColumns: mismatch between tags and data"
192+ where
193+ here = fromResult @_ @(MaybeTable context a) mhere
194+ there = fromResult @_ @(MaybeTable context b) mthere
195+ mhere = HMaybeTable
196+ { htag = hrelabel hhereTag
197+ , hjust = hrelabel hhere
198+ }
199+ mthere = HMaybeTable
200+ { htag = hrelabel hthereTag
201+ , hjust = hrelabel hthere
202+ }
183203
184204
185205instance
186− ( Reifiable from, Abstract from, from ~ from'
187− , Reifiable to, Abstract to, to ~ to'
188− , Recontextualize from to a1 b1
206+ ( Recontextualize from to a1 b1
189207 , Recontextualize from to a2 b2
208+ , Reifiable from, from ~ from'
209+ , Reifiable to, to ~ to'
190210 )
191211 => Recontextualize from to (TheseTable from' a1 a2) (TheseTable to' b1 b2)
192212
@@ -213,19 +233,8 @@ instance (OrdTable a, OrdTable b, context ~ Expr) =>
213233 }
214234
215235
216−type instance FromExprs (TheseTable _context a b) =
217− These (FromExprs a) (FromExprs b)
218−
219−
220236instance (ToExprs exprs1 a, ToExprs exprs2 b, x ~ TheseTable Expr exprs1 exprs2) =>
221237 ToExprs x (These a b)
222− where
223− fromResult =
224− bimap (fromResult @exprs1) (fromResult @exprs2) .
225− fromColumns
226− toResult =
227− toColumns .
228− bimap (toResult @exprs1) (toResult @exprs2)
229238
230239
231240-- | Test if a 'TheseTable' was constructed with 'thisTable'.
src/Rel8/Type/Composite.hs+10−10
@@ -32,14 +32,14 @@ import qualified Opaleye.Internal.HaskellDB.PrimQuery as Opaleye
3232-- rel8
3333import Rel8.Expr ( Col( E ), Expr )
3434import Rel8.Expr.Opaleye ( castExpr, fromPrimExpr, toPrimExpr )
35−import Rel8.Schema.HTable ( hfield, hspecs, htabulate, htabulateA )
35+import Rel8.Schema.HTable ( HTable, hfield, hspecs, htabulate, htabulateA )
3636import Rel8.Schema.Name ( Col( N ), Name( Name ) )
3737import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
3838import Rel8.Schema.Result ( Col( R ), Result )
3939import Rel8.Schema.Spec ( SSpec( SSpec, nullity, info ) )
40−import Rel8.Table ( Table, fromColumns, toColumns )
40+import Rel8.Table ( fromColumns, toColumns, fromResult, toResult )
4141import Rel8.Table.Eq ( EqTable )
42−import Rel8.Table.HKD ( HKD, HKDable, fromHKD, toHKD )
42+import Rel8.Table.HKD ( HKD, HKDable )
4343import Rel8.Table.Ord ( OrdTable )
4444import Rel8.Table.Rel8able ()
4545import Rel8.Table.Serialize ( lit )
@@ -67,8 +67,8 @@ newtype Composite a = Composite
6767
6868instance DBComposite a => DBType (Composite a) where
6969 typeInformation = TypeInformation
70− { decode = Hasql.composite (Composite . fromHKD <$> decoder)
71− , encode = encoder . lit . toColumns . toHKD . unComposite
70+ { decode = Hasql.composite (Composite . fromResult @_ @(HKD a Expr) <$> decoder)
71+ , encode = encoder . lit . toResult @_ @(HKD a Expr) . unComposite
7272 , typeName = compositeTypeName @a
7373 }
7474
@@ -103,7 +103,7 @@ class (DBType a, HKDable a) => DBComposite a where
103103-- single column expression, by combining them into a PostgreSQL composite
104104-- type.
105105compose :: DBComposite a => HKD a Expr -> Expr a
106−compose = castExpr . fromPrimExpr . encoder
106+compose = castExpr . fromPrimExpr . encoder . toColumns
107107
108108
109109-- | Expand a composite type into a 'HKD'.
@@ -118,8 +118,8 @@ decompose (toPrimExpr -> a) = fromColumns $ htabulate \field ->
118118 names = toColumns (compositeFields @a)
119119
120120
121−decoder :: Table Result a => Hasql.Composite a
122−decoder = fmap fromColumns $ unwrapApplicative $ htabulateA \field ->
121+decoder :: HTable t => Hasql.Composite (t (Col Result))
122+decoder = unwrapApplicative $ htabulateA \field ->
123123 case hfield hspecs field of
124124 SSpec {nullity, info} -> WrapApplicative $ R <$>
125125 case nullity of
@@ -127,8 +127,8 @@ decoder = fmap fromColumns $ unwrapApplicative $ htabulateA \field ->
127127 NotNull -> Hasql.field $ Hasql.nonNullable $ decode info
128128
129129
130−encoder :: Table Expr a => a -> Opaleye.PrimExpr
131−encoder (toColumns -> a) = Opaleye.FunExpr "ROW" exprs
130+encoder :: HTable t => t (Col Expr) -> Opaleye.PrimExpr
131+encoder a = Opaleye.FunExpr "ROW" exprs
132132 where
133133 exprs = getConst $ htabulateA \field -> case hfield a field of
134134 E (toPrimExpr -> expr) -> Const [expr]
src/Rel8/Type/Tag.hs+1−1
@@ -21,7 +21,7 @@ import Prelude
2121import qualified Opaleye.Internal.HaskellDB.PrimQuery as Opaleye
2222
2323-- rel8
24−import {-# SOURCE #-} Rel8.Expr ( Expr )
24+import Rel8.Expr ( Expr )
2525import Rel8.Expr.Eq ( (==.) )
2626import Rel8.Expr.Opaleye ( zipPrimExprsWith )
2727import Rel8.Expr.Serialize ( litExpr )
tests/Rel8/Generic/Rel8able/Test.hs+3−15
@@ -1,13 +1,11 @@
11{-# language DataKinds #-}
22{-# language DeriveAnyClass #-}
33{-# language DeriveGeneric #-}
4−{-# language DerivingVia #-}
4+{-# language DerivingStrategies #-}
55{-# language DuplicateRecordFields #-}
66{-# language FlexibleInstances #-}
77{-# language MultiParamTypeClasses #-}
8−{-# language StandaloneDeriving #-}
98{-# language TypeFamilies #-}
10−{-# language UndecidableInstances #-}
119
1210{-# options_ghc -O0 #-}
1311
@@ -98,24 +96,14 @@ data S3Object = S3Object
9896 deriving stock Generic
9997
10098
101−deriving via HKDT S3Object
102− instance Table Result S3Object
103−
104−
105−deriving via HKDT S3Object
106− instance x ~ HKD S3Object Expr => ToExprs x S3Object
99+instance x ~ HKD S3Object Expr => ToExprs x S3Object
107100
108101
109102data HKDSum = HKDSumA Text | HKDSumB Bool Char | HKDSumC
110103 deriving stock Generic
111104
112105
113−deriving via HKDT HKDSum
114− instance Table Result HKDSum
115−
116−
117−deriving via HKDT HKDSum
118− instance x ~ HKD HKDSum Expr => ToExprs x HKDSum
106+instance x ~ HKD HKDSum Expr => ToExprs x HKDSum
119107
120108
121109data HKDTest f = HKDTest