git.iko.soy/rel8
on master help sign in
Move FromExprs into the Table class and get rid of Unreify (#106)
7c5422fShane
rel8.cabal+2−4
compare with master
unifiedsplit
@@ -39,6 +39,7 @@ library
39 default-language:
39 default-language:
40 Haskell2010
40 Haskell2010
41 ghc-options:
41 ghc-options:
42+ -Werror=missing-methods -Werror=incomplete-patterns -Werror=missing-fields
42 -Weverything -Wno-unsafe -Wno-safe -Wno-missing-safe-haskell-mode
43 -Weverything -Wno-unsafe -Wno-safe -Wno-missing-safe-haskell-mode
43 -Wno-missing-import-lists -Wno-prepositive-qualified-module
44 -Wno-missing-import-lists -Wno-prepositive-qualified-module
44 -Wno-monomorphism-restriction
45 -Wno-monomorphism-restriction
@@ -82,13 +83,11 @@ library
82 Rel8.Kind.Algebra
83 Rel8.Kind.Algebra
83 Rel8.Kind.Context
84 Rel8.Kind.Context
84
85
85− Rel8.Generic.Coherence
86 Rel8.Generic.Construction
86 Rel8.Generic.Construction
87 Rel8.Generic.Construction.ADT
87 Rel8.Generic.Construction.ADT
88 Rel8.Generic.Construction.Record
88 Rel8.Generic.Construction.Record
89 Rel8.Generic.Map
89 Rel8.Generic.Map
90 Rel8.Generic.Record
90 Rel8.Generic.Record
91− Rel8.Generic.Reify
92 Rel8.Generic.Rel8able
91 Rel8.Generic.Rel8able
93 Rel8.Generic.Table
92 Rel8.Generic.Table
94 Rel8.Generic.Table.ADT
93 Rel8.Generic.Table.ADT
@@ -116,8 +115,8 @@ library
116 Rel8.Query.Values
115 Rel8.Query.Values
117
116
118 Rel8.Schema.Context
117 Rel8.Schema.Context
119− Rel8.Schema.Context.Abstract
120 Rel8.Schema.Context.Nullify
118 Rel8.Schema.Context.Nullify
119+ Rel8.Schema.Context.Virtual
121 Rel8.Schema.Dict
120 Rel8.Schema.Dict
122 Rel8.Schema.HTable
121 Rel8.Schema.HTable
123 Rel8.Schema.HTable.Either
122 Rel8.Schema.HTable.Either
@@ -134,7 +133,6 @@ library
134 Rel8.Schema.Kind
133 Rel8.Schema.Kind
135 Rel8.Schema.Name
134 Rel8.Schema.Name
136 Rel8.Schema.Null
135 Rel8.Schema.Null
137− Rel8.Schema.Reify
138 Rel8.Schema.Result
136 Rel8.Schema.Result
139 Rel8.Schema.Spec
137 Rel8.Schema.Spec
140 Rel8.Schema.Spec.Constrain
138 Rel8.Schema.Spec.Constrain
src/Rel8.hs+1−5
@@ -239,8 +239,7 @@ module Rel8
239
239
240 -- * IO
240 -- * IO
241 , Serializable
241 , Serializable
242− , ToExprs(..)
242+ , ToExprs
243− , FromExprs
244 , Result
243 , Result
245
244
246 -- * Running statements
245 -- * Running statements
@@ -272,9 +271,6 @@ module Rel8
272 -- ** Sequences
271 -- ** Sequences
273 , nextval
272 , nextval
274 , evaluate
273 , evaluate
275−
276− -- * Implementation details
277− , HKDT(..)
278 ) where
274 ) where
279
275
280-- base
276-- base
src/Rel8/Aggregate.hs+5−18
@@ -1,5 +1,4 @@
1{-# language DataKinds #-}
1{-# language DataKinds #-}
2−{-# language DerivingVia #-}
3{-# language FlexibleContexts #-}
2{-# language FlexibleContexts #-}
4{-# language FlexibleInstances #-}
3{-# language FlexibleInstances #-}
5{-# language GADTs #-}
4{-# language GADTs #-}
@@ -21,7 +20,6 @@ where
21
20
22-- base
21-- base
23import Data.Functor.Const ( Const( Const ), getConst )
22import Data.Functor.Const ( Const( Const ), getConst )
24−import Data.Functor.Identity ( Identity )
25import Data.Kind ( Constraint, Type )
23import Data.Kind ( Constraint, Type )
26import Prelude
24import Prelude
27
25
@@ -36,12 +34,11 @@ import Rel8.Schema.Context ( Interpretation(..) )
36import Rel8.Schema.HTable.Identity ( HIdentity(..), HType )
34import Rel8.Schema.HTable.Identity ( HIdentity(..), HType )
37import Rel8.Schema.Name ( Name )
35import Rel8.Schema.Name ( Name )
38import Rel8.Schema.Null ( Sql )
36import Rel8.Schema.Null ( Sql )
39−import Rel8.Schema.Reify ( notReify )
37+import Rel8.Schema.Result ( Col( R ) )
40−import Rel8.Schema.Result ( Result )
41import Rel8.Schema.Spec ( Spec( Spec ) )
38import Rel8.Schema.Spec ( Spec( Spec ) )
42import Rel8.Table
39import Rel8.Table
43 ( Table, Columns, Context, fromColumns, toColumns
40 ( Table, Columns, Context, fromColumns, toColumns
44− , reify, unreify, coherence, congruence
41+ , FromExprs, fromResult, toResult
45 )
42 )
46import Rel8.Table.Recontextualize ( Recontextualize )
43import Rel8.Table.Recontextualize ( Recontextualize )
47import Rel8.Type ( DBType )
44import Rel8.Type ( DBType )
@@ -67,14 +64,12 @@ instance Interpretation Aggregate where
67instance Sql DBType a => Table Aggregate (Aggregate a) where
64instance Sql DBType a => Table Aggregate (Aggregate a) where
68 type Columns (Aggregate a) = HType a
65 type Columns (Aggregate a) = HType a
69 type Context (Aggregate a) = Aggregate
66 type Context (Aggregate a) = Aggregate
67+ type FromExprs (Aggregate a) = a
70
68
71 toColumns = HIdentity . A
69 toColumns = HIdentity . A
72 fromColumns (HIdentity (A a)) = a
70 fromColumns (HIdentity (A a)) = a
73−
71+ toResult = HIdentity . R
74− reify = notReify
72+ fromResult (HIdentity (R a)) = a
75− unreify = notReify
76− coherence = notReify
77− congruence = notReify
78
73
79
74
80instance Sql DBType a =>
75instance Sql DBType a =>
@@ -85,10 +80,6 @@ instance Sql DBType a =>
85 Recontextualize Aggregate Expr (Aggregate a) (Expr a)
80 Recontextualize Aggregate Expr (Aggregate a) (Expr a)
86
81
87
82
88−instance Sql DBType a =>
89− Recontextualize Aggregate Result (Aggregate a) (Identity a)
90−
91−
92instance Sql DBType a =>
83instance Sql DBType a =>
93 Recontextualize Aggregate Name (Aggregate a) (Name a)
84 Recontextualize Aggregate Name (Aggregate a) (Name a)
94
85
@@ -97,10 +88,6 @@ instance Sql DBType a =>
97 Recontextualize Expr Aggregate (Expr a) (Aggregate a)
88 Recontextualize Expr Aggregate (Expr a) (Aggregate a)
98
89
99
90
100−instance Sql DBType a =>
101− Recontextualize Result Aggregate (Identity a) (Aggregate a)
102−
103−
104instance Sql DBType a =>
91instance Sql DBType a =>
105 Recontextualize Name Aggregate (Name a) (Aggregate a)
92 Recontextualize Name Aggregate (Name a) (Aggregate a)
106
93
src/Rel8/Column.hs+6−87
@@ -1,41 +1,24 @@
1{-# language DataKinds #-}
1{-# language DataKinds #-}
2−{-# language FlexibleContexts #-}
3−{-# language LambdaCase #-}
4−{-# language MultiParamTypeClasses #-}
5−{-# language ScopedTypeVariables #-}
6{-# language StandaloneKindSignatures #-}
2{-# language StandaloneKindSignatures #-}
7−{-# language TypeApplications #-}
8{-# language TypeFamilies #-}
3{-# language TypeFamilies #-}
9
4
10module Rel8.Column
5module Rel8.Column
11− ( Column, AColumn(..)
6+ ( Column
12 , TColumn
7 , TColumn
13 )
8 )
14where
9where
15
10
16-- base
11-- base
17import Data.Kind ( Type )
12import Data.Kind ( Type )
18−import Data.Type.Equality ( (:~:)( Refl ) )
19−import Prelude
13+import Prelude ()
20
14
21-- rel8
15-- rel8
22−import Rel8.Aggregate ( Aggregate, Col( A ) )
16+import Rel8.Aggregate ( Aggregate )
23−import Rel8.Expr ( Expr, Col( E ) )
17+import Rel8.Expr ( Expr )
24import Rel8.FCF ( Eval, Exp )
18import Rel8.FCF ( Eval, Exp )
25−import Rel8.Kind.Context ( SContext(..), Reifiable( contextSing ) )
26−import Rel8.Schema.HTable.Identity ( HIdentity(..), HType )
27import qualified Rel8.Schema.Kind as K
19import qualified Rel8.Schema.Kind as K
28−import Rel8.Schema.Name ( Name(..), Col( N ) )
20+import Rel8.Schema.Name ( Name(..) )
29−import Rel8.Schema.Null ( Sql )
30−import Rel8.Schema.Reify ( Reify, Col(..) )
21+import Rel8.Schema.Result ( Result )
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 )
39
22
40
23
41-- | This type family is used to specify columns in 'Rel8able's. In @Column f
24-- | This type family is used to specify columns in 'Rel8able's. In @Column f
@@ -43,75 +26,11 @@ import Rel8.Type ( DBType )
43-- 'Rel8able' definitions), and @a@ is the type of the column.
26-- 'Rel8able' definitions), and @a@ is the type of the column.
44type Column :: K.Context -> Type -> Type
27type Column :: K.Context -> Type -> Type
45type family Column context a where
28type family Column context a where
46− Column (Reify context) a = AColumn context a
47 Column Aggregate a = Aggregate a
29 Column Aggregate a = Aggregate a
48 Column Expr a = Expr a
30 Column Expr a = Expr a
49 Column Name a = Name a
31 Column Name a = Name a
50 Column Result a = a
32 Column Result a = a
51
33
52
34
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−
116data TColumn :: K.Context -> Type -> Exp Type
35data TColumn :: K.Context -> Type -> Exp Type
117type instance Eval (TColumn f a) = Column f a
36type instance Eval (TColumn f a) = Column f a
src/Rel8/Column/ADT.hs+4−87
@@ -1,106 +1,23 @@
1{-# language DataKinds #-}
1{-# language DataKinds #-}
2−{-# language LambdaCase #-}
3−{-# language MultiParamTypeClasses #-}
4−{-# language ScopedTypeVariables #-}
5{-# language StandaloneKindSignatures #-}
2{-# language StandaloneKindSignatures #-}
6−{-# language TypeApplications #-}
7{-# language TypeFamilies #-}
3{-# language TypeFamilies #-}
8−{-# language UndecidableInstances #-}
9
4
10module Rel8.Column.ADT
5module Rel8.Column.ADT
11− ( HADT, AHADT(..)
6+ ( HADT
12 )
7 )
13where
8where
14
9
15-- base
10-- base
16import Data.Kind ( Type )
11import Data.Kind ( Type )
17−import Data.Type.Equality ( (:~:)( Refl ) )
18−import Prelude
12+import Prelude ()
19
13
20-- rel8
14-- rel8
21−import Rel8.Generic.Rel8able ( GColumns )
22−import Rel8.Kind.Context ( SContext(..), Reifiable, contextSing )
23−import Rel8.Schema.Context ( Col )
24import qualified Rel8.Schema.Kind as K
15import qualified Rel8.Schema.Kind as K
25−import Rel8.Schema.Reify ( Reify, hreify, hunreify )
16+import Rel8.Schema.Result ( Result )
26−import Rel8.Schema.Result ( Result, absurd )
27−import Rel8.Table
17+import Rel8.Table.ADT ( ADT )
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 )
34
18
35
19
36type HADT :: K.Context -> K.Rel8able -> Type
20type HADT :: K.Context -> K.Rel8able -> Type
37type family HADT context t where
21type family HADT context t where
38− HADT (Reify context) t = AHADT context t
39 HADT Result t = t Result
22 HADT Result t = t Result
40 HADT context t = ADT t context
23 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 @@
1{-# language DataKinds #-}
1{-# language DataKinds #-}
2−{-# language FlexibleContexts #-}
3−{-# language LambdaCase #-}
4−{-# language MultiParamTypeClasses #-}
5−{-# language ScopedTypeVariables #-}
6{-# language StandaloneKindSignatures #-}
2{-# language StandaloneKindSignatures #-}
7−{-# language TypeApplications #-}
8{-# language TypeFamilyDependencies #-}
3{-# language TypeFamilyDependencies #-}
9−{-# language UndecidableInstances #-}
10
4
11module Rel8.Column.Either
5module Rel8.Column.Either
12− ( HEither, AHEither(..)
6+ ( HEither
13 )
7 )
14where
8where
15
9
16-- base
10-- base
17−import Control.Applicative ( liftA2 )
18−import Control.Category ( id )
19−import Data.Bifunctor ( Bifunctor, bimap )
20import Data.Kind ( Type )
11import Data.Kind ( Type )
21−import Data.Type.Equality ( (:~:)( Refl ), apply )
22−import Prelude hiding ( id )
12+import Prelude
23
13
24-- rel8
14-- rel8
25import Rel8.Aggregate ( Aggregate )
15import Rel8.Aggregate ( Aggregate )
26import Rel8.Expr ( Expr )
16import Rel8.Expr ( Expr )
27−import Rel8.Kind.Context ( SContext(..), Reifiable( contextSing ) )
28−import Rel8.Schema.Context ( Col )
29−import Rel8.Schema.HTable.Either ( HEitherTable )
30import qualified Rel8.Schema.Kind as K
17import qualified Rel8.Schema.Kind as K
31−import Rel8.Schema.Name ( Name(..) )
18+import Rel8.Schema.Name ( Name )
32−import Rel8.Schema.Reify ( Reify, hreify, hunreify )
19+import Rel8.Schema.Result ( Result )
33−import Rel8.Schema.Result ( Result, absurd )
34−import Rel8.Table
35− ( Table, Columns, Context, fromColumns, toColumns
36− , Unreify, reify, unreify, coherence, congruence
37− )
38import Rel8.Table.Either ( EitherTable )
20import Rel8.Table.Either ( EitherTable )
39−import Rel8.Table.Recontextualize ( Recontextualize )
40
21
41
22
42-- | Nest an 'Either' value within a 'Rel8able'. @HEither f a b@ will produce a
23-- | Nest an 'Either' value within a 'Rel8able'. @HEither f a b@ will produce a
@@ -44,149 +25,7 @@ import Rel8.Table.Recontextualize ( Recontextualize )
44-- 'Result' context.
25-- 'Result' context.
45type HEither :: K.Context -> Type -> Type -> Type
26type HEither :: K.Context -> Type -> Type -> Type
46type family HEither context = either | either -> context where
27type family HEither context = either | either -> context where
47− HEither (Reify context) = AHEither context
48 HEither Aggregate = EitherTable Aggregate
28 HEither Aggregate = EitherTable Aggregate
49 HEither Expr = EitherTable Expr
29 HEither Expr = EitherTable Expr
50 HEither Name = EitherTable Name
30 HEither Name = EitherTable Name
51 HEither Result = Either
31 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 @@
1{-# language DataKinds #-}
1{-# language DataKinds #-}
2−{-# language LambdaCase #-}
3−{-# language MultiParamTypeClasses #-}
4−{-# language ScopedTypeVariables #-}
5{-# language StandaloneKindSignatures #-}
2{-# language StandaloneKindSignatures #-}
6−{-# language TypeApplications #-}
7{-# language TypeFamilies #-}
3{-# language TypeFamilies #-}
8
4
9module Rel8.Column.Lift
5module Rel8.Column.Lift
10− ( Lift, ALift(..)
6+ ( Lift
11 )
7 )
12where
8where
13
9
14-- base
10-- base
15import Data.Kind ( Type )
11import Data.Kind ( Type )
16−import Data.Type.Equality ( (:~:)( Refl ) )
17−import Prelude
12+import Prelude ()
18
13
19-- rel8
14-- rel8
20−import Rel8.Generic.Rel8able ( GColumns )
21−import Rel8.Kind.Context ( Reifiable(..), SContext(..) )
22−import Rel8.Schema.Context ( Col )
23import qualified Rel8.Schema.Kind as K
15import qualified Rel8.Schema.Kind as K
24−import Rel8.Schema.Reify ( Reify, hreify, hunreify )
16+import Rel8.Schema.Result ( Result )
25−import Rel8.Schema.Result ( Result, absurd )
26−import Rel8.Table
17+import Rel8.Table.HKD ( HKD )
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 )
33
18
34
19
35type Lift :: K.Context -> Type -> Type
20type Lift :: K.Context -> Type -> Type
36type family Lift context a where
21type family Lift context a where
37− Lift (Reify context) a = ALift context a
38 Lift Result a = a
22 Lift Result a = a
39 Lift context a = HKD a context
23 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 @@
1{-# language DataKinds #-}
1{-# language DataKinds #-}
2−{-# language FlexibleContexts #-}
3−{-# language LambdaCase #-}
4−{-# language MultiParamTypeClasses #-}
5−{-# language RankNTypes #-}
6−{-# language ScopedTypeVariables #-}
7{-# language StandaloneKindSignatures #-}
2{-# language StandaloneKindSignatures #-}
8−{-# language TypeApplications #-}
9{-# language TypeFamilyDependencies #-}
3{-# language TypeFamilyDependencies #-}
10−{-# language UndecidableInstances #-}
11
4
12module Rel8.Column.List
5module Rel8.Column.List
13− ( HList, AHList(..)
6+ ( HList
14 )
7 )
15where
8where
16
9
17-- base
10-- base
18−import Control.Category ( id )
19import Data.Kind ( Type )
11import Data.Kind ( Type )
20−import Data.Type.Equality ( (:~:)( Refl ), apply )
21−import Prelude hiding ( id )
12+import Prelude ()
22
13
23-- rel8
14-- rel8
24import Rel8.Aggregate ( Aggregate )
15import Rel8.Aggregate ( Aggregate )
25import Rel8.Expr ( Expr )
16import 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 )
30import qualified Rel8.Schema.Kind as K
17import qualified Rel8.Schema.Kind as K
31import Rel8.Schema.Name ( Name )
18import Rel8.Schema.Name ( Name )
32−import Rel8.Schema.Reify ( Reify, hreify, hunreify )
19+import Rel8.Schema.Result ( Result )
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 ) )
20+import Rel8.Table.List ( ListTable )
39−import Rel8.Table.Recontextualize ( Recontextualize )
40
21
41
22
42-- | Nest a list within a 'Rel8able'. @HList f a@ will produce a 'ListTable'
23-- | Nest a list within a 'Rel8able'. @HList f a@ will produce a 'ListTable'
43-- @a@ in the 'Expr' context, and a @[a]@ in the 'Result' context.
24-- @a@ in the 'Expr' context, and a @[a]@ in the 'Result' context.
44type HList :: K.Context -> Type -> Type
25type HList :: K.Context -> Type -> Type
45type family HList context = list | list -> context where
26type family HList context = list | list -> context where
46− HList (Reify context) = AHList context
47 HList Aggregate = ListTable Aggregate
27 HList Aggregate = ListTable Aggregate
48 HList Expr = ListTable Expr
28 HList Expr = ListTable Expr
49 HList Name = ListTable Name
29 HList Name = ListTable Name
50 HList Result = []
30 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 @@
1{-# language DataKinds #-}
1{-# language DataKinds #-}
2−{-# language FlexibleContexts #-}
3−{-# language GADTs #-}
4−{-# language LambdaCase #-}
5−{-# language MultiParamTypeClasses #-}
6−{-# language ScopedTypeVariables #-}
7{-# language StandaloneKindSignatures #-}
2{-# language StandaloneKindSignatures #-}
8−{-# language TypeApplications #-}
9{-# language TypeFamilyDependencies #-}
3{-# language TypeFamilyDependencies #-}
10−{-# language UndecidableInstances #-}
11
4
12module Rel8.Column.Maybe
5module Rel8.Column.Maybe
13− ( HMaybe, AHMaybe(..)
6+ ( HMaybe
14 )
7 )
15where
8where
16
9
17-- base
10-- base
18−import Control.Category ( id )
19import Data.Kind ( Type )
11import Data.Kind ( Type )
20−import Data.Type.Equality ( (:~:)( Refl ), apply )
21−import Prelude hiding ( id )
12+import Prelude
22
13
23-- rel8
14-- rel8
24import Rel8.Aggregate ( Aggregate )
15import Rel8.Aggregate ( Aggregate )
25import Rel8.Expr ( Expr )
16import Rel8.Expr ( Expr )
26−import Rel8.Kind.Context ( SContext(..), Reifiable( contextSing ) )
27−import Rel8.Schema.Context ( Col )
28−import Rel8.Schema.HTable.Maybe ( HMaybeTable )
29import qualified Rel8.Schema.Kind as K
17import qualified Rel8.Schema.Kind as K
30import Rel8.Schema.Name ( Name )
18import Rel8.Schema.Name ( Name )
31−import Rel8.Schema.Reify ( Reify, hreify, hunreify )
19+import Rel8.Schema.Result ( Result )
32−import Rel8.Schema.Result ( Result, absurd )
33−import Rel8.Table
34− ( Table, Columns, Context, fromColumns, toColumns
35− , Unreify, reify, unreify, coherence, congruence
36− )
37import Rel8.Table.Maybe ( MaybeTable )
20import Rel8.Table.Maybe ( MaybeTable )
38−import Rel8.Table.Recontextualize ( Recontextualize )
39
21
40
22
41-- | Nest a 'Maybe' value within a 'Rel8able'. @HMaybe f a@ will produce a
23-- | Nest a 'Maybe' value within a 'Rel8able'. @HMaybe f a@ will produce a
@@ -43,103 +25,7 @@ import Rel8.Table.Recontextualize ( Recontextualize )
43-- context.
25-- context.
44type HMaybe :: K.Context -> Type -> Type
26type HMaybe :: K.Context -> Type -> Type
45type family HMaybe context = maybe | maybe -> context where
27type family HMaybe context = maybe | maybe -> context where
46− HMaybe (Reify context) = AHMaybe context
47 HMaybe Aggregate = MaybeTable Aggregate
28 HMaybe Aggregate = MaybeTable Aggregate
48 HMaybe Expr = MaybeTable Expr
29 HMaybe Expr = MaybeTable Expr
49 HMaybe Name = MaybeTable Name
30 HMaybe Name = MaybeTable Name
50 HMaybe Result = Maybe
31 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 @@
1{-# language DataKinds #-}
1{-# language DataKinds #-}
2−{-# language FlexibleContexts #-}
3−{-# language LambdaCase #-}
4−{-# language MultiParamTypeClasses #-}
5−{-# language ScopedTypeVariables #-}
6{-# language StandaloneKindSignatures #-}
2{-# language StandaloneKindSignatures #-}
7−{-# language TypeApplications #-}
8{-# language TypeFamilyDependencies #-}
3{-# language TypeFamilyDependencies #-}
9−{-# language UndecidableInstances #-}
10
4
11module Rel8.Column.NonEmpty
5module Rel8.Column.NonEmpty
12− ( HNonEmpty, AHNonEmpty(..)
6+ ( HNonEmpty
13 )
7 )
14where
8where
15
9
16-- base
10-- base
17−import Control.Category ( id )
18import Data.Kind ( Type )
11import Data.Kind ( Type )
19import Data.List.NonEmpty ( NonEmpty )
12import Data.List.NonEmpty ( NonEmpty )
20−import Data.Type.Equality ( (:~:)( Refl ), apply )
21−import Prelude hiding ( id )
13+import Prelude ()
22
14
23-- rel8
15-- rel8
24import Rel8.Aggregate ( Aggregate )
16import Rel8.Aggregate ( Aggregate )
25import Rel8.Expr ( Expr )
17import 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 )
30import qualified Rel8.Schema.Kind as K
18import qualified Rel8.Schema.Kind as K
31import Rel8.Schema.Name ( Name )
19import Rel8.Schema.Name ( Name )
32−import Rel8.Schema.Reify ( Reify, hreify, hunreify )
20+import Rel8.Schema.Result ( Result )
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 ) )
21+import Rel8.Table.NonEmpty ( NonEmptyTable )
39−import Rel8.Table.Recontextualize ( Recontextualize )
40
22
41
23
42-- | Nest a 'NonEmpty' list within a 'Rel8able'. @HNonEmpty f a@ will produce a
24-- | Nest a 'NonEmpty' list within a 'Rel8able'. @HNonEmpty f a@ will produce a
@@ -44,131 +26,7 @@ import Rel8.Table.Recontextualize ( Recontextualize )
44-- 'Result' context.
26-- 'Result' context.
45type HNonEmpty :: K.Context -> Type -> Type
27type HNonEmpty :: K.Context -> Type -> Type
46type family HNonEmpty context = nonEmpty | nonEmpty -> context where
28type family HNonEmpty context = nonEmpty | nonEmpty -> context where
47− HNonEmpty (Reify context) = AHNonEmpty context
48 HNonEmpty Aggregate = NonEmptyTable Aggregate
29 HNonEmpty Aggregate = NonEmptyTable Aggregate
49 HNonEmpty Expr = NonEmptyTable Expr
30 HNonEmpty Expr = NonEmptyTable Expr
50 HNonEmpty Name = NonEmptyTable Name
31 HNonEmpty Name = NonEmptyTable Name
51 HNonEmpty Result = NonEmpty
32 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 @@
1{-# language DataKinds #-}
1{-# language DataKinds #-}
2−{-# language FlexibleContexts #-}
3−{-# language GADTs #-}
4−{-# language LambdaCase #-}
5−{-# language MultiParamTypeClasses #-}
6−{-# language ScopedTypeVariables #-}
7{-# language StandaloneKindSignatures #-}
2{-# language StandaloneKindSignatures #-}
8−{-# language TypeApplications #-}
9{-# language TypeFamilyDependencies #-}
3{-# language TypeFamilyDependencies #-}
10−{-# language UndecidableInstances #-}
11
4
12module Rel8.Column.These
5module Rel8.Column.These
13− ( HThese, AHThese(..)
6+ ( HThese
14 )
7 )
15where
8where
16
9
17-- base
10-- base
18−import Control.Applicative ( liftA2 )
19−import Control.Category ( id )
20−import Data.Bifunctor ( Bifunctor, bimap )
21import Data.Kind ( Type )
11import Data.Kind ( Type )
22−import Data.Type.Equality ( (:~:)( Refl ), apply )
23−import Prelude hiding ( id )
12+import Prelude ()
24
13
25-- rel8
14-- rel8
26import Rel8.Aggregate ( Aggregate )
15import Rel8.Aggregate ( Aggregate )
27import Rel8.Expr ( Expr )
16import Rel8.Expr ( Expr )
28−import Rel8.Kind.Context ( SContext(..), Reifiable( contextSing ) )
29−import Rel8.Schema.Context ( Col )
30−import Rel8.Schema.HTable.These ( HTheseTable )
31import qualified Rel8.Schema.Kind as K
17import qualified Rel8.Schema.Kind as K
32import Rel8.Schema.Name ( Name )
18import Rel8.Schema.Name ( Name )
33−import Rel8.Schema.Reify ( Reify, hreify, hunreify )
19+import Rel8.Schema.Result ( Result )
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 )
40import Rel8.Table.These ( TheseTable )
20import Rel8.Table.These ( TheseTable )
41
21
42-- these
22-- these
@@ -48,149 +28,7 @@ import Data.These ( These )
48-- 'Result' context.
28-- 'Result' context.
49type HThese :: K.Context -> Type -> Type -> Type
29type HThese :: K.Context -> Type -> Type -> Type
50type family HThese context = these | these -> context where
30type family HThese context = these | these -> context where
51− HThese (Reify context) = AHThese context
52 HThese Aggregate = TheseTable Aggregate
31 HThese Aggregate = TheseTable Aggregate
53 HThese Expr = TheseTable Expr
32 HThese Expr = TheseTable Expr
54 HThese Name = TheseTable Name
33 HThese Name = TheseTable Name
55 HThese Result = These
34 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
20where
20where
21
21
22-- base
22-- base
23−import Data.Functor.Identity ( Identity )
24import Data.Kind ( Type )
23import Data.Kind ( Type )
25import Data.String ( IsString, fromString )
24import Data.String ( IsString, fromString )
26import Prelude hiding ( null )
25import Prelude hiding ( null )
@@ -41,12 +40,11 @@ import Rel8.Expr.Serialize ( litExpr )
41import Rel8.Schema.Context ( Interpretation, Col )
40import Rel8.Schema.Context ( Interpretation, Col )
42import Rel8.Schema.HTable.Identity ( HIdentity( HType ), HType )
41import Rel8.Schema.HTable.Identity ( HIdentity( HType ), HType )
43import Rel8.Schema.Null ( Nullity( Null, NotNull ), Sql, nullable )
42import Rel8.Schema.Null ( Nullity( Null, NotNull ), Sql, nullable )
44−import Rel8.Schema.Reify ( notReify )
43+import Rel8.Schema.Result ( Col( R ) )
45−import Rel8.Schema.Result ( Result )
46import Rel8.Schema.Spec ( Spec( Spec ) )
44import Rel8.Schema.Spec ( Spec( Spec ) )
47import Rel8.Table
45import Rel8.Table
48 ( Table, Columns, Context, fromColumns, toColumns
46 ( Table, Columns, Context, fromColumns, toColumns
49− , reify, unreify, coherence, congruence
47+ , FromExprs, fromResult, toResult
50 )
48 )
51import Rel8.Table.Recontextualize ( Recontextualize )
49import Rel8.Table.Recontextualize ( Recontextualize )
52import Rel8.Type ( DBType )
50import Rel8.Type ( DBType )
@@ -134,19 +132,12 @@ instance Interpretation Expr where
134instance Sql DBType a => Table Expr (Expr a) where
132instance Sql DBType a => Table Expr (Expr a) where
135 type Columns (Expr a) = HType a
133 type Columns (Expr a) = HType a
136 type Context (Expr a) = Expr
134 type Context (Expr a) = Expr
135+ type FromExprs (Expr a) = a
137
136
138 toColumns a = HType (E a)
137 toColumns a = HType (E a)
139 fromColumns (HType (E a)) = a
138 fromColumns (HType (E a)) = a
140− reify = notReify
139+ toResult a = HType (R a)
141− unreify = notReify
140+ fromResult (HType (R a)) = a
142− coherence = notReify
143− congruence = notReify
144
141
145
142
146instance Sql DBType a => Recontextualize Expr Expr (Expr a) (Expr a)
143instance 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
22import qualified Opaleye.Internal.HaskellDB.PrimQuery as Opaleye
22import qualified Opaleye.Internal.HaskellDB.PrimQuery as Opaleye
23
23
24-- rel8
24-- rel8
25−import {-# SOURCE #-} Rel8.Expr ( Expr )
25+import Rel8.Expr ( Expr )
26import Rel8.Expr.Bool ( (&&.), (||.), false, or_, coalesce )
26import Rel8.Expr.Bool ( (&&.), (||.), false, or_, coalesce )
27import Rel8.Expr.Null ( isNull, unsafeLiftOpNull )
27import Rel8.Expr.Null ( isNull, unsafeLiftOpNull )
28import Rel8.Expr.Opaleye ( fromPrimExpr, toPrimExpr, zipPrimExprsWith )
28import Rel8.Expr.Opaleye ( fromPrimExpr, toPrimExpr, zipPrimExprsWith )
src/Rel8/FCF.hs+3−3
@@ -5,7 +5,7 @@
5
5
6module Rel8.FCF
6module Rel8.FCF
7 ( Exp, Eval
7 ( Exp, Eval
8− , Compose
8+ , Id
9 )
9 )
10where
10where
11
11
@@ -22,5 +22,5 @@ type Eval :: Exp e -> e
22type family Eval a
22type family Eval a
23
23
24
24
25−data Compose :: (Type -> Type) -> (Type -> Exp Type) -> Type -> Exp Type
25+data Id :: a -> Exp a
26−type instance Eval (Compose f g a) = f (Eval (g 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 @@
2{-# language ConstraintKinds #-}
2{-# language ConstraintKinds #-}
3{-# language DataKinds #-}
3{-# language DataKinds #-}
4{-# language FlexibleContexts #-}
4{-# language FlexibleContexts #-}
5−{-# language FlexibleInstances #-}
6−{-# language MultiParamTypeClasses #-}
7{-# language NamedFieldPuns #-}
5{-# language NamedFieldPuns #-}
8{-# language ScopedTypeVariables #-}
6{-# language ScopedTypeVariables #-}
9{-# language StandaloneKindSignatures #-}
7{-# language StandaloneKindSignatures #-}
@@ -27,7 +25,6 @@ where
27import Data.Bifunctor ( first )
25import Data.Bifunctor ( first )
28import Data.Kind ( Constraint, Type )
26import Data.Kind ( Constraint, Type )
29import Data.List.NonEmpty ( NonEmpty( (:|) ) )
27import Data.List.NonEmpty ( NonEmpty( (:|) ) )
30−import Data.Type.Equality ( (:~:)( Refl ) )
31import GHC.TypeLits ( Symbol )
28import GHC.TypeLits ( Symbol )
32import Prelude
29import Prelude
33
30
@@ -38,7 +35,7 @@ import Rel8.Expr.Aggregate ( groupByExpr )
38import Rel8.Expr.Eq ( (==.) )
35import Rel8.Expr.Eq ( (==.) )
39import Rel8.Expr.Null ( nullify, snull, unsafeUnnullify )
36import Rel8.Expr.Null ( nullify, snull, unsafeUnnullify )
40import Rel8.Expr.Serialize ( litExpr )
37import Rel8.Expr.Serialize ( litExpr )
41−import Rel8.FCF ( Eval, Exp )
38+import Rel8.FCF ( Eval, Exp, Id )
42import Rel8.Generic.Construction.ADT
39import Rel8.Generic.Construction.ADT
43 ( GConstructorADT, GMakeableADT, gmakeADT
40 ( GConstructorADT, GMakeableADT, gmakeADT
44 , GConstructableADT
41 , GConstructableADT
@@ -65,11 +62,9 @@ import qualified Rel8.Schema.Kind as K
65import Rel8.Schema.Name ( Col( N ), Name( Name ) )
62import Rel8.Schema.Name ( Col( N ), Name( Name ) )
66import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
63import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
67import Rel8.Schema.Spec ( SSpec( SSpec, nullity, info ) )
64import Rel8.Schema.Spec ( SSpec( SSpec, nullity, info ) )
68−import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify )
69−import Rel8.Schema.Result ( Result )
70import Rel8.Table
65import Rel8.Table
71− ( TTable, TColumns, TUnreify
66+ ( TTable, TColumns
72− , Table, fromColumns, toColumns, reify, unreify
67+ , Table, fromColumns, toColumns
73 )
68 )
74import Rel8.Table.Bool ( case_ )
69import Rel8.Table.Bool ( case_ )
75import Rel8.Type.Tag ( Tag )
70import Rel8.Type.Tag ( Tag )
@@ -78,10 +73,10 @@ import Rel8.Type.Tag ( Tag )
78type GGBuildable :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Constraint
73type GGBuildable :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Constraint
79type GGBuildable algebra name rep =
74type GGBuildable algebra name rep =
80 ( KnownAlgebra algebra
75 ( KnownAlgebra algebra
81− , Eval (GGColumns algebra TColumns (Eval (rep (Reify Aggregate)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
76+ , Eval (GGColumns algebra TColumns (Eval (rep Aggregate))) ~ Eval (GGColumns algebra TColumns (Eval (rep Expr)))
82− , Eval (GGColumns algebra TColumns (Eval (rep (Reify Expr)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
77+ , Eval (GGColumns algebra TColumns (Eval (rep Expr))) ~ Eval (GGColumns algebra TColumns (Eval (rep Expr)))
83− , Eval (GGColumns algebra TColumns (Eval (rep (Reify Name)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
78+ , Eval (GGColumns algebra TColumns (Eval (rep Name))) ~ Eval (GGColumns algebra TColumns (Eval (rep Expr)))
84− , HTable (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))))
79+ , HTable (Eval (GGColumns algebra TColumns (Eval (rep Expr))))
85 , GGBuildable' algebra name rep
80 , GGBuildable' algebra name rep
86 )
81 )
87
82
@@ -89,65 +84,63 @@ type GGBuildable algebra name rep =
89type GGBuildable' :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Constraint
84type GGBuildable' :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Constraint
90type family GGBuildable' algebra name rep where
85type family GGBuildable' algebra name rep where
91 GGBuildable' 'K.Product name rep =
86 GGBuildable' 'K.Product name rep =
92− ( name ~ GConstructor (Eval (rep (Reify Expr)))
87+ ( name ~ GConstructor (Eval (rep Expr))
93− , Representable TUnreify (Eval (rep (Reify Expr)))
88+ , Representable Id (Eval (rep Expr))
94− , GConstructable (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (Eval (rep (Reify Expr)))
89+ , GConstructable (TTable Expr) TColumns Id (Col Expr) (Eval (rep Expr))
95 )
90 )
96 GGBuildable' 'K.Sum name rep =
91 GGBuildable' 'K.Sum name rep =
97− ( Representable TUnreify (GConstructorADT name (Eval (rep (Reify Expr))))
92+ ( Representable Id (GConstructorADT name (Eval (rep Expr)))
98− , GMakeableADT (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) name (Eval (rep (Reify Expr)))
93+ , GMakeableADT (TTable Expr) TColumns Id (Col Expr) name (Eval (rep Expr))
99 )
94 )
100
95
101
96
102type GGBuild :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
97type GGBuild :: K.Algebra -> Symbol -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
103type family GGBuild algebra name rep r where
98type family GGBuild algebra name rep r where
104 GGBuild 'K.Product _name rep r =
99 GGBuild 'K.Product _name rep r =
105− GConstruct TUnreify (Eval (rep (Reify Expr))) r
100+ GConstruct Id (Eval (rep Expr)) r
106 GGBuild 'K.Sum name rep r =
101 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
108
103
109
104
110ggbuild :: forall algebra name rep a. GGBuildable algebra name rep
105ggbuild :: 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)
112 -> GGBuild algebra name rep a
107 -> GGBuild algebra name rep a
113ggbuild gfromColumns = case algebraSing @algebra of
108ggbuild gfromColumns = case algebraSing @algebra of
114 SProduct ->
109 SProduct ->
115− gtabulate @TUnreify @(Eval (rep (Reify Expr))) @a $
110+ gtabulate @Id @(Eval (rep Expr)) @a $
116 gfromColumns .
111 gfromColumns .
117− hunreify .
118 gconstruct
112 gconstruct
119− @(TTable (Reify Expr))
113+ @(TTable Expr)
120 @TColumns
114 @TColumns
121− @TUnreify
115+ @Id
122− @(Col (Reify Expr))
116+ @(Col Expr)
123− @(Eval (rep (Reify Expr)))
117+ @(Eval (rep Expr))
124− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
118+ (const toColumns)
125 SSum ->
119 SSum ->
126− gtabulate @TUnreify @(GConstructorADT name (Eval (rep (Reify Expr)))) @a $
120+ gtabulate @Id @(GConstructorADT name (Eval (rep Expr))) @a $
127 gfromColumns .
121 gfromColumns .
128− hunreify .
129 gmakeADT
122 gmakeADT
130− @(TTable (Reify Expr))
123+ @(TTable Expr)
131 @TColumns
124 @TColumns
132− @TUnreify
125+ @Id
133− @(Col (Reify Expr))
126+ @(Col Expr)
134 @name
127 @name
135− @(Eval (rep (Reify Expr)))
128+ @(Eval (rep Expr))
136− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
129+ (const toColumns)
137− (\SSpec {info} -> Reify (E (snull info)))
130+ (\SSpec {info} -> E (snull info))
138 (\SSpec {nullity} -> case nullity of
131 (\SSpec {nullity} -> case nullity of
139 Null -> id
132 Null -> id
140− NotNull -> \(Reify (E a)) -> Reify (E (nullify a)))
133+ NotNull -> \(E a) -> E (nullify a))
141− (HType . Reify . E . litExpr)
134+ (HType . E . litExpr)
142
135
143
136
144type GGConstructable :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
137type GGConstructable :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
145type GGConstructable algebra rep =
138type GGConstructable algebra rep =
146 ( KnownAlgebra algebra
139 ( KnownAlgebra algebra
147− , Eval (GGColumns algebra TColumns (Eval (rep (Reify Aggregate)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
140+ , Eval (GGColumns algebra TColumns (Eval (rep Aggregate))) ~ Eval (GGColumns algebra TColumns (Eval (rep Expr)))
148− , Eval (GGColumns algebra TColumns (Eval (rep (Reify Expr)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
141+ , Eval (GGColumns algebra TColumns (Eval (rep Expr))) ~ Eval (GGColumns algebra TColumns (Eval (rep Expr)))
149− , Eval (GGColumns algebra TColumns (Eval (rep (Reify Name)))) ~ Eval (GGColumns algebra TColumns (Eval (rep (Reify Result))))
142+ , Eval (GGColumns algebra TColumns (Eval (rep Name))) ~ Eval (GGColumns algebra TColumns (Eval (rep Expr)))
150− , HTable (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))))
143+ , HTable (Eval (GGColumns algebra TColumns (Eval (rep Expr))))
151 , GGConstructable' algebra rep
144 , GGConstructable' algebra rep
152 )
145 )
153
146
@@ -155,105 +148,100 @@ type GGConstructable algebra rep =
155type GGConstructable' :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
148type GGConstructable' :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Constraint
156type family GGConstructable' algebra rep where
149type family GGConstructable' algebra rep where
157 GGConstructable' 'K.Product rep =
150 GGConstructable' 'K.Product rep =
158− ( Representable TUnreify (Eval (rep (Reify Aggregate)))
151+ ( Representable Id (Eval (rep Aggregate))
159− , Representable TUnreify (Eval (rep (Reify Expr)))
152+ , Representable Id (Eval (rep Expr))
160− , Representable TUnreify (Eval (rep (Reify Name)))
153+ , Representable Id (Eval (rep Name))
161− , GConstructable (TTable (Reify Aggregate)) TColumns TUnreify (Col (Reify Aggregate)) (Eval (rep (Reify Aggregate)))
154+ , GConstructable (TTable Aggregate) TColumns Id (Col Aggregate) (Eval (rep Aggregate))
162− , GConstructable (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (Eval (rep (Reify Expr)))
155+ , GConstructable (TTable Expr) TColumns Id (Col Expr) (Eval (rep Expr))
163− , GConstructable (TTable (Reify Name)) TColumns TUnreify (Col (Reify Name)) (Eval (rep (Reify Name)))
156+ , GConstructable (TTable Name) TColumns Id (Col Name) (Eval (rep Name))
164 )
157 )
165 GGConstructable' 'K.Sum rep =
158 GGConstructable' 'K.Sum rep =
166− ( RepresentableConstructors TUnreify (Eval (rep (Reify Expr)))
159+ ( RepresentableConstructors Id (Eval (rep Expr))
167− , RepresentableFields TUnreify (Eval (rep (Reify Aggregate)))
160+ , RepresentableFields Id (Eval (rep Aggregate))
168− , RepresentableFields TUnreify (Eval (rep (Reify Expr)))
161+ , RepresentableFields Id (Eval (rep Expr))
169− , RepresentableFields TUnreify (Eval (rep (Reify Name)))
162+ , RepresentableFields Id (Eval (rep Name))
170− , Functor (GConstructors TUnreify (Eval (rep (Reify Expr))))
163+ , Functor (GConstructors Id (Eval (rep Expr)))
171− , GConstructableADT (TTable (Reify Aggregate)) TColumns TUnreify (Col (Reify Aggregate)) (Eval (rep (Reify Aggregate)))
164+ , GConstructableADT (TTable Aggregate) TColumns Id (Col Aggregate) (Eval (rep Aggregate))
172− , GConstructableADT (TTable (Reify Expr)) TColumns TUnreify (Col (Reify Expr)) (Eval (rep (Reify Expr)))
165+ , GConstructableADT (TTable Expr) TColumns Id (Col Expr) (Eval (rep Expr))
173− , GConstructableADT (TTable (Reify Name)) TColumns TUnreify (Col (Reify Name)) (Eval (rep (Reify Name)))
166+ , GConstructableADT (TTable Name) TColumns Id (Col Name) (Eval (rep Name))
174 )
167 )
175
168
176
169
177type GGConstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
170type GGConstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
178type family GGConstruct algebra rep r where
171type family GGConstruct algebra rep r where
179− GGConstruct 'K.Product rep r =
172+ GGConstruct 'K.Product rep r = GConstruct Id (Eval (rep Expr)) r -> 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
173+ GGConstruct 'K.Sum rep r = GConstructADT Id (Eval (rep Expr)) r r
183
174
184
175
185ggconstruct :: forall algebra rep a. GGConstructable algebra rep
176ggconstruct :: 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)
187 -> GGConstruct algebra rep a -> a
178 -> GGConstruct algebra rep a -> a
188ggconstruct gfromColumns f = case algebraSing @algebra of
179ggconstruct gfromColumns f = case algebraSing @algebra of
189 SProduct ->
180 SProduct ->
190 f $
181 f $
191− gtabulate @TUnreify @(Eval (rep (Reify Expr))) @a $
182+ gtabulate @Id @(Eval (rep Expr)) @a $
192 gfromColumns .
183 gfromColumns .
193− hunreify .
194 gconstruct
184 gconstruct
195− @(TTable (Reify Expr))
185+ @(TTable Expr)
196 @TColumns
186 @TColumns
197− @TUnreify
187+ @Id
198− @(Col (Reify Expr))
188+ @(Col Expr)
199− @(Eval (rep (Reify Expr)))
189+ @(Eval (rep Expr))
200− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
190+ (const toColumns)
201 SSum ->
191 SSum ->
202− gcindex @TUnreify @(Eval (rep (Reify Expr))) @a f $
192+ gcindex @Id @(Eval (rep Expr)) @a f $
203− fmap (gfromColumns . hunreify) $
193+ fmap gfromColumns $
204 gconstructADT
194 gconstructADT
205− @(TTable (Reify Expr))
195+ @(TTable Expr)
206 @TColumns
196 @TColumns
207− @TUnreify
197+ @Id
208− @(Col (Reify Expr))
198+ @(Col Expr)
209− @(Eval (rep (Reify Expr)))
199+ @(Eval (rep Expr))
210− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
200+ (const toColumns)
211− (\SSpec {info} -> Reify (E (snull info)))
201+ (\SSpec {info} -> E (snull info))
212 (\SSpec {nullity} -> case nullity of
202 (\SSpec {nullity} -> case nullity of
213 Null -> id
203 Null -> id
214− NotNull -> \(Reify (E a)) -> Reify (E (nullify a)))
204+ NotNull -> \(E a) -> E (nullify a))
215− (HType . Reify . E . litExpr)
205+ (HType . E . litExpr)
216
206
217
207
218type GGDeconstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type -> Type
208type GGDeconstruct :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type -> Type
219type family GGDeconstruct algebra rep a r where
209type family GGDeconstruct algebra rep a r where
220 GGDeconstruct 'K.Product rep a r =
210 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
222 GGDeconstruct 'K.Sum rep a r =
212 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)
224
214
225
215
226ggdeconstruct :: forall algebra rep a r. (GGConstructable algebra rep, Table Expr r)
216ggdeconstruct :: 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))
228 -> GGDeconstruct algebra rep a r
218 -> GGDeconstruct algebra rep a r
229ggdeconstruct gtoColumns = case algebraSing @algebra of
219ggdeconstruct gtoColumns = case algebraSing @algebra of
230 SProduct -> \build ->
220 SProduct -> \build ->
231− gindex @TUnreify @(Eval (rep (Reify Expr))) @r build .
221+ gindex @Id @(Eval (rep Expr)) @r build .
232 gdeconstruct
222 gdeconstruct
233− @(TTable (Reify Expr))
223+ @(TTable Expr)
234 @TColumns
224 @TColumns
235− @TUnreify
225+ @Id
236− @(Col (Reify Expr))
226+ @(Col Expr)
237− @(Eval (rep (Reify Expr)))
227+ @(Eval (rep Expr))
238− (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns) .
228+ (const fromColumns) .
239− hreify .
240 gtoColumns
229 gtoColumns
241 SSum ->
230 SSum ->
242− gctabulate @TUnreify @(Eval (rep (Reify Expr))) @r @(a -> r) $ \constructors as ->
231+ gctabulate @Id @(Eval (rep Expr)) @r @(a -> r) $ \constructors as ->
243 let
232 let
244− (HType (Reify (E tag)), cases) =
233+ (HType (E tag), cases) =
245 gdeconstructADT
234 gdeconstructADT
246− @(TTable (Reify Expr))
235+ @(TTable Expr)
247 @TColumns
236 @TColumns
248− @TUnreify
237+ @Id
249− @(Col (Reify Expr))
238+ @(Col Expr)
250− @(Eval (rep (Reify Expr)))
239+ @(Eval (rep Expr))
251− (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns)
240+ (const fromColumns)
252 (\SSpec {nullity} -> case nullity of
241 (\SSpec {nullity} -> case nullity of
253 Null -> id
242 Null -> id
254− NotNull -> \(Reify (E a)) -> Reify (E (unsafeUnnullify a)))
243+ NotNull -> \(E a) -> E (unsafeUnnullify a))
255 constructors $
244 constructors $
256− hreify $
257 gtoColumns as
245 gtoColumns as
258 in
246 in
259 case cases of
247 case cases of
@@ -263,108 +251,102 @@ ggdeconstruct gtoColumns = case algebraSing @algebra of
263
251
264type GGName :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
252type GGName :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
265type family GGName algebra rep a where
253type family GGName algebra rep a where
266− GGName 'K.Product rep a = GConstruct TUnreify (Eval (rep (Reify Name))) a
254+ GGName 'K.Product rep a = GConstruct Id (Eval (rep Name)) a
267− GGName 'K.Sum rep a = Name Tag -> GBuildADT TUnreify (Eval (rep (Reify Name))) a
255+ GGName 'K.Sum rep a = Name Tag -> GBuildADT Id (Eval (rep Name)) a
268
256
269
257
270ggname :: forall algebra rep a. GGConstructable algebra rep
258ggname :: 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)
272 -> GGName algebra rep a
260 -> GGName algebra rep a
273ggname gfromColumns = case algebraSing @algebra of
261ggname gfromColumns = case algebraSing @algebra of
274 SProduct ->
262 SProduct ->
275− gtabulate @TUnreify @(Eval (rep (Reify Name))) @a $
263+ gtabulate @Id @(Eval (rep Name)) @a $
276 gfromColumns .
264 gfromColumns .
277− hunreify .
278 gconstruct
265 gconstruct
279− @(TTable (Reify Name))
266+ @(TTable Name)
280 @TColumns
267 @TColumns
281− @TUnreify
268+ @Id
282− @(Col (Reify Name))
269+ @(Col Name)
283− @(Eval (rep (Reify Name)))
270+ @(Eval (rep Name))
284− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
271+ (const toColumns)
285 SSum -> \tag ->
272 SSum -> \tag ->
286− gftabulate @TUnreify @(Eval (rep (Reify Name))) @a $
273+ gftabulate @Id @(Eval (rep Name)) @a $
287 gfromColumns .
274 gfromColumns .
288− hunreify .
289 gbuildADT
275 gbuildADT
290− @(TTable (Reify Name))
276+ @(TTable Name)
291 @TColumns
277 @TColumns
292− @TUnreify
278+ @Id
293− @(Col (Reify Name))
279+ @(Col Name)
294− @(Eval (rep (Reify Name)))
280+ @(Eval (rep Name))
295− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
281+ (const toColumns)
296− (\_ _ (Reify (N (Name a))) -> Reify (N (Name a)))
282+ (\_ _ (N (Name a)) -> N (Name a))
297− (HType (Reify (N tag)))
283+ (HType (N tag))
298
284
299
285
300type GGAggregate :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
286type GGAggregate :: K.Algebra -> (K.Context -> Exp (Type -> Type)) -> Type -> Type
301type family GGAggregate algebra rep r where
287type family GGAggregate algebra rep r where
302 GGAggregate 'K.Product rep r =
288 GGAggregate 'K.Product rep r =
303− GConstruct TUnreify (Eval (rep (Reify Aggregate))) r ->
289+ GConstruct Id (Eval (rep Aggregate)) r ->
304− GConstruct TUnreify (Eval (rep (Reify Expr))) r
290+ GConstruct Id (Eval (rep Expr)) r
305 GGAggregate 'K.Sum rep r =
291 GGAggregate 'K.Sum rep r =
306− GBuildADT TUnreify (Eval (rep (Reify Aggregate))) r ->
292+ GBuildADT Id (Eval (rep Aggregate)) r ->
307− GBuildADT TUnreify (Eval (rep (Reify Expr))) r
293+ GBuildADT Id (Eval (rep Expr)) r
308
294
309
295
310ggaggregate :: forall algebra rep exprs agg. GGConstructable algebra rep
296ggaggregate :: forall algebra rep exprs agg. GGConstructable algebra rep
311− => (Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Aggregate) -> agg)
297+ => (Eval (GGColumns algebra TColumns (Eval (rep Expr))) (Col Aggregate) -> agg)
312− -> (exprs -> Eval (GGColumns algebra TColumns (Eval (rep (Reify Result)))) (Col Expr))
298+ -> (exprs -> Eval (GGColumns algebra TColumns (Eval (rep Expr))) (Col Expr))
313 -> GGAggregate algebra rep agg -> exprs -> agg
299 -> GGAggregate algebra rep agg -> exprs -> agg
314ggaggregate gfromColumns gtoColumns agg es = case algebraSing @algebra of
300ggaggregate gfromColumns gtoColumns agg es = case algebraSing @algebra of
315 SProduct -> flip f exprs $
301 SProduct -> flip f exprs $
316 gfromColumns .
302 gfromColumns .
317− hunreify .
318 gconstruct
303 gconstruct
319− @(TTable (Reify Aggregate))
304+ @(TTable Aggregate)
320 @TColumns
305 @TColumns
321− @TUnreify
306+ @Id
322− @(Col (Reify Aggregate))
307+ @(Col Aggregate)
323− @(Eval (rep (Reify Aggregate)))
308+ @(Eval (rep Aggregate))
324− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
309+ (const toColumns)
325 where
310 where
326 f =
311 f =
327− gindex @TUnreify @(Eval (rep (Reify Expr))) @agg .
312+ gindex @Id @(Eval (rep Expr)) @agg .
328 agg .
313 agg .
329− gtabulate @TUnreify @(Eval (rep (Reify Aggregate))) @agg
314+ gtabulate @Id @(Eval (rep Aggregate)) @agg
330 exprs =
315 exprs =
331 gdeconstruct
316 gdeconstruct
332− @(TTable (Reify Expr))
317+ @(TTable Expr)
333 @TColumns
318 @TColumns
334− @TUnreify
319+ @Id
335− @(Col (Reify Expr))
320+ @(Col Expr)
336− @(Eval (rep (Reify Expr)))
321+ @(Eval (rep Expr))
337− (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns) $
322+ (const fromColumns) $
338− hreify $
339 gtoColumns es
323 gtoColumns es
340 SSum -> flip f exprs $
324 SSum -> flip f exprs $
341 gfromColumns .
325 gfromColumns .
342− hunreify .
343 gbuildADT
326 gbuildADT
344− @(TTable (Reify Aggregate))
327+ @(TTable Aggregate)
345 @TColumns
328 @TColumns
346− @TUnreify
329+ @Id
347− @(Col (Reify Aggregate))
330+ @(Col Aggregate)
348− @(Eval (rep (Reify Aggregate)))
331+ @(Eval (rep Aggregate))
349− (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)
332+ (const toColumns)
350− (\tag' SSpec {nullity} (Reify (A (Aggregate a))) ->
333+ (\tag' SSpec {nullity} (A (Aggregate a)) ->
351− Reify $ A $ Aggregate $ sguard (tag ==. litExpr tag') . snullify nullity <$> a)
334+ A $ Aggregate $ sguard (tag ==. litExpr tag') . snullify nullity <$> a)
352− (HType (Reify (A (groupByExpr tag))))
335+ (HType (A (groupByExpr tag)))
353 where
336 where
354 f =
337 f =
355− gfindex @TUnreify @(Eval (rep (Reify Expr))) @agg .
338+ gfindex @Id @(Eval (rep Expr)) @agg .
356 agg .
339 agg .
357− gftabulate @TUnreify @(Eval (rep (Reify Aggregate))) @agg
340+ gftabulate @Id @(Eval (rep Aggregate)) @agg
358− (HType (Reify (E tag)), exprs) =
341+ (HType (E tag), exprs) =
359 gunbuildADT
342 gunbuildADT
360− @(TTable (Reify Expr))
343+ @(TTable Expr)
361 @TColumns
344 @TColumns
362− @TUnreify
345+ @Id
363− @(Col (Reify Expr))
346+ @(Col Expr)
364− @(Eval (rep (Reify Expr)))
347+ @(Eval (rep Expr))
365− (\(_ :: proxy x) -> unreify @_ @x Refl . fromColumns)
348+ (const fromColumns)
366 (\SSpec {nullity} -> case nullity of
349 (\SSpec {nullity} -> case nullity of
367 Null -> id
350 Null -> id
368− NotNull -> \(Reify (E a)) -> Reify (E (unsafeUnnullify a))) $
351+ NotNull -> \(E a) -> E (unsafeUnnullify a)) $
369− hreify $
370 gtoColumns es
352 gtoColumns es
src/Rel8/Generic/Map.hs+3−67
@@ -1,26 +1,17 @@
1−{-# language AllowAmbiguousTypes #-}
2{-# language DataKinds #-}
1{-# language DataKinds #-}
3−{-# language EmptyCase #-}
4−{-# language FlexibleInstances #-}
5−{-# language LambdaCase #-}
6−{-# language MultiParamTypeClasses #-}
7−{-# language RankNTypes #-}
8−{-# language ScopedTypeVariables #-}
9{-# language StandaloneKindSignatures #-}
2{-# language StandaloneKindSignatures #-}
10−{-# language TypeApplications #-}
11{-# language TypeFamilies #-}
3{-# language TypeFamilies #-}
12{-# language TypeOperators #-}
4{-# language TypeOperators #-}
13−{-# language UndecidableInstances #-}
14
5
15module Rel8.Generic.Map
6module Rel8.Generic.Map
16− ( GMap, GMappable (gmap, gunmap)
7+ ( GMap
17 )
8 )
18where
9where
19
10
20-- base
11-- base
21−import Data.Kind ( Constraint, Type )
12+import Data.Kind ( Type )
22import GHC.Generics
13import GHC.Generics
23− ( (:+:)( L1, R1 ), (:*:)( (:*:) ), K1( K1 ), M1( M1 ), U1( U1 ), V1
14+ ( (:+:), (:*:), K1, M1, U1, V1
24 )
15 )
25import Prelude ()
16import Prelude ()
26
17
@@ -36,58 +27,3 @@ type family GMap f rep where
36 GMap _ U1 = U1
27 GMap _ U1 = U1
37 GMap f (rep1 :*: rep2) = GMap f rep1 :*: GMap f rep2
28 GMap f (rep1 :*: rep2) = GMap f rep1 :*: GMap f rep2
38 GMap f (K1 i a) = K1 i (Eval (f a))
29 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 @@
1{-# language AllowAmbiguousTypes #-}
1{-# language AllowAmbiguousTypes #-}
2+{-# language ConstraintKinds #-}
2{-# language DataKinds #-}
3{-# language DataKinds #-}
3{-# language DefaultSignatures #-}
4{-# language DefaultSignatures #-}
4{-# language FlexibleContexts #-}
5{-# language FlexibleContexts #-}
5−{-# language FlexibleInstances #-}
6+{-# language LambdaCase #-}
6−{-# language MultiParamTypeClasses #-}
7{-# language ScopedTypeVariables #-}
7{-# language ScopedTypeVariables #-}
8{-# language StandaloneKindSignatures #-}
8{-# language StandaloneKindSignatures #-}
9{-# language TypeApplications #-}
9{-# language TypeApplications #-}
@@ -15,34 +15,32 @@ module Rel8.Generic.Rel8able
15 , Algebra
15 , Algebra
16 , GRep
16 , GRep
17 , GColumns, gfromColumns, gtoColumns
17 , GColumns, gfromColumns, gtoColumns
18− , greify, gunreify
18+ , GFromExprs, gfromResult, gtoResult
19− , TUnreifyContext
20 )
19 )
21where
20where
22
21
23-- base
22-- base
24import Data.Kind ( Constraint, Type )
23import Data.Kind ( Constraint, Type )
25−import Data.Proxy ( Proxy( Proxy ) )
26−import Data.Type.Equality ( (:~:)( Refl ) )
27import GHC.Generics ( Generic, Rep, from, to )
24import GHC.Generics ( Generic, Rep, from, to )
28import Prelude
25import Prelude
29
26
30-- rel8
27-- rel8
31−import Rel8.Kind.Context ( Reifiable )
28+import Rel8.Aggregate ( Aggregate )
32−import Rel8.FCF ( Eval, Exp )
29+import Rel8.Expr ( Expr )
33−import Rel8.Generic.Map ( GMap, GMappable, gmap, gunmap )
30+import Rel8.Generic.Map ( GMap )
34import Rel8.Generic.Record ( Record(..) )
31import Rel8.Generic.Record ( Record(..) )
35import Rel8.Generic.Table ( GAlgebra )
32import Rel8.Generic.Table ( GAlgebra )
36import qualified Rel8.Generic.Table.Record as G
33import qualified Rel8.Generic.Table.Record as G
37import qualified Rel8.Kind.Algebra as K ( Algebra(..) )
34import qualified Rel8.Kind.Algebra as K ( Algebra(..) )
38import Rel8.Schema.Context ( Col )
35import Rel8.Schema.Context ( Col )
36+import Rel8.Schema.Context.Virtual ( Abstract(..) )
39import Rel8.Schema.HTable ( HTable )
37import Rel8.Schema.HTable ( HTable )
40import qualified Rel8.Schema.Kind as K
38import qualified Rel8.Schema.Kind as K
41−import Rel8.Schema.Reify ( Reify, UnwrapReify )
39+import Rel8.Schema.Name ( Name )
42import Rel8.Schema.Result ( Result )
40import Rel8.Schema.Result ( Result )
43import Rel8.Table
41import Rel8.Table
44− ( fromColumns, toColumns, reify, unreify
42+ ( fromColumns, toColumns, fromResult, toResult
45− , TTable, TColumns, TContext, TUnreify
43+ , TTable, TColumns, TFromExprs
46 )
44 )
47
45
48
46
@@ -96,79 +94,103 @@ type KRel8able = K.Rel8able
96type Rel8able :: K.Rel8able -> Constraint
94type Rel8able :: K.Rel8able -> Constraint
97class HTable (GColumns t) => Rel8able t where
95class HTable (GColumns t) => Rel8able t where
98 type GColumns t :: K.HTable
96 type GColumns t :: K.HTable
97+ type GFromExprs t :: Type
99
98
100− gfromColumns :: Reifiable context
99+ gfromColumns :: Abstract context -> GColumns t (Col context) -> t context
101− => GColumns t (Col (Reify context)) -> t (Reify context)
100+ gtoColumns :: Abstract context -> t context -> GColumns t (Col context)
102
101
103− gtoColumns :: Reifiable context
102+ gfromResult :: GColumns t (Col Result) -> GFromExprs t
104− => t (Reify context) -> GColumns t (Col (Reify context))
103+ gtoResult :: GFromExprs t -> GColumns t (Col Result)
105
104
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
113
107
114 default gfromColumns :: forall context.
108 default gfromColumns :: forall context.
115− ( Generic (Record (t (Reify context)))
109+ ( VRel8able t Aggregate
116− , G.GTable (TTable (Reify context)) TColumns (Col (Reify context)) (GRep t (Reify context))
110+ , VRel8able t Expr
117− , G.GColumns TColumns (GRep t (Reify context)) ~ GColumns t
111+ , VRel8able t Name
118 )
112 )
119− => GColumns t (Col (Reify context)) -> t (Reify context)
113+ => Abstract context -> GColumns t (Col context) -> t context
120− gfromColumns =
114+ gfromColumns = \case
121− unrecord .
115+ VAggregate -> vfromColumns
122− to .
116+ VExpr -> vfromColumns
123− G.gfromColumns @(TTable (Reify context)) @TColumns fromColumns
117+ VName -> vfromColumns
124
118
125 default gtoColumns :: forall context.
119 default gtoColumns :: forall context.
126− ( Generic (Record (t (Reify context)))
120+ ( VRel8able t Aggregate
127− , G.GTable (TTable (Reify context)) TColumns (Col (Reify context)) (GRep t (Reify context))
121+ , VRel8able t Expr
128− , G.GColumns TColumns (GRep t (Reify context)) ~ GColumns t
122+ , VRel8able t Name
129 )
123 )
130− => t (Reify context) -> GColumns t (Col (Reify context))
124+ => Abstract context -> t context -> GColumns t (Col context)
131− gtoColumns =
125+ gtoColumns = \case
132− G.gtoColumns @(TTable (Reify context)) @TColumns toColumns .
126+ VAggregate -> vtoColumns
133− from .
127+ VExpr -> vtoColumns
134− Record
128+ VName -> vtoColumns
135−
129+
136− default greify :: forall context.
130+ default gfromResult ::
137− ( Generic (Record (t context))
131+ ( Generic (Record (t Result))
138− , Generic (Record (t (Reify context)))
132+ , G.GTable (TTable Expr) TColumns TFromExprs (GRep t Expr)
139− , GMappable (TTable (Reify context)) (GRep t (Reify context))
133+ , G.GColumns TColumns (GRep t Expr) ~ GColumns t
140− , GRep t context ~ GMap TUnreify (GRep t (Reify context))
134+ , Rep (Record (t Result)) ~ GMap TFromExprs (GRep t Expr)
135+ , GFromExprs t ~ t Result
141 )
136 )
142− => t context -> t (Reify context)
137+ => GColumns t (Col Result) -> GFromExprs t
143− greify =
138+ gfromResult =
144 unrecord .
139 unrecord .
145 to .
140 to .
146− gunmap @(TTable (Reify context)) (Proxy @TUnreify) (reify Refl) .
141+ G.gfromResult
147− from .
142+ @(TTable Expr)
148− Record
143+ @TColumns
149−
144+ @TFromExprs
150− default gunreify :: forall context.
145+ @(GRep t Expr)
146+ (\(_ :: proxy x) -> fromResult @Expr @x)
147+
148+ default gtoResult ::
151− ( Generic (Record (t context))
149+ ( Generic (Record (t Result))
152− , Generic (Record (t (Reify context)))
150+ , G.GTable (TTable Expr) TColumns TFromExprs (GRep t Expr)
153− , GMappable (TTable (Reify context)) (GRep t (Reify context))
151+ , G.GColumns TColumns (GRep t Expr) ~ GColumns t
154− , GRep t context ~ GMap TUnreify (GRep t (Reify context))
152+ , Rep (Record (t Result)) ~ GMap TFromExprs (GRep t Expr)
153+ , GFromExprs t ~ t Result
155 )
154 )
156− => t (Reify context) -> t context
155+ => GFromExprs t -> GColumns t (Col Result)
157− gunreify =
156+ gtoResult =
158− unrecord .
157+ G.gtoResult
159− to .
158+ @(TTable Expr)
160− gmap @(TTable (Reify context)) (Proxy @TUnreify) (unreify Refl) .
159+ @TColumns
160+ @TFromExprs
161+ @(GRep t Expr)
162+ (\(_ :: proxy x) -> toResult @Expr @x) .
161 from .
163 from .
162 Record
164 Record
163
165
164
166
165type Algebra :: K.Rel8able -> K.Algebra
167type Algebra :: K.Rel8able -> K.Algebra
166−type Algebra t = GAlgebra (GRep t (Reify Result))
168+type Algebra t = GAlgebra (GRep t Expr)
167
169
168
170
169type GRep :: K.Rel8able -> K.Context -> Type -> Type
171type GRep :: K.Rel8able -> K.Context -> Type -> Type
170type GRep t context = Rep (Record (t context))
172type GRep t context = Rep (Record (t context))
171
173
172
174
173−data TUnreifyContext :: Type -> Exp K.Context
175+type VRel8able :: K.Rel8able -> K.Context -> Constraint
174−type instance Eval (TUnreifyContext a) = UnwrapReify (Eval (TContext a))
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 @@
12{-# language UndecidableInstances #-}
12{-# language UndecidableInstances #-}
13
13
14module Rel8.Generic.Table
14module Rel8.Generic.Table
15− ( GGTable, GGColumns, GGContext, ggfromColumns, ggtoColumns, ggtable
16− , GGToExprs, ggfromResult, ggtoResult
15+ ( GGTable, GGColumns, ggfromResult, ggtoResult
17 , GAlgebra
16 , GAlgebra
18 )
17 )
19where
18where
@@ -25,14 +24,11 @@ import Prelude ()
25
24
26-- rel8
25-- rel8
27import Rel8.FCF ( Eval, Exp )
26import Rel8.FCF ( Eval, Exp )
27+import Rel8.Generic.Map ( GMap )
28import Rel8.Generic.Table.ADT
28import Rel8.Generic.Table.ADT
29− ( GTableADT, GColumnsADT, gfromColumnsADT, gtoColumnsADT, gtableADT
30− , GToExprsADT, gtoResultADT, gfromResultADT
29+ ( GTableADT, GColumnsADT, gtoResultADT, gfromResultADT
31− )
32−import Rel8.Generic.Table.Record
33− ( GTable, GColumns, GContext, gfromColumns, gtoColumns, gtable
34− , GToExprs, gtoResult, gfromResult
35 )
30 )
31+import Rel8.Generic.Table.Record ( GTable, GColumns, gtoResult, gfromResult )
36import Rel8.Kind.Algebra
32import Rel8.Kind.Algebra
37 ( Algebra( Product, Sum )
33 ( Algebra( Product, Sum )
38 , SAlgebra( SProduct, SSum )
34 , SAlgebra( SProduct, SSum )
@@ -40,8 +36,6 @@ import Rel8.Kind.Algebra
40 )
36 )
41import Rel8.Schema.Context ( Col )
37import Rel8.Schema.Context ( Col )
42import qualified Rel8.Schema.Kind as K
38import qualified Rel8.Schema.Kind as K
43−import Rel8.Schema.Null ( Nullify )
44−import Rel8.Schema.Spec ( Spec( Spec ), SSpec )
45import Rel8.Schema.Result ( Result )
39import Rel8.Schema.Result ( Result )
46
40
47
41
@@ -49,34 +43,17 @@ data GGTable
49 :: Algebra
43 :: Algebra
50 -> (Type -> Exp Constraint)
44 -> (Type -> Exp Constraint)
51 -> (Type -> Exp K.HTable)
45 -> (Type -> Exp K.HTable)
52− -> K.HContext
46+ -> (Type -> Exp Type)
53 -> (Type -> Type)
47 -> (Type -> Type)
54 -> Exp Constraint
48 -> Exp Constraint
55
49
56
50
57−type instance Eval (GGTable 'Product _Table _Columns context rep) =
51+type instance Eval (GGTable 'Product _Table _Columns _FromExprs rep) =
58− GTable _Table _Columns context rep
52+ GTable _Table _Columns _FromExprs rep
59−
60
53
61−type instance Eval (GGTable 'Sum _Table _Columns context rep) =
62− GTableADT _Table _Columns context rep
63
54
64−
55+type instance Eval (GGTable 'Sum _Table _Columns _FromExprs rep) =
65−data GGToExprs
56+ GTableADT _Table _Columns _FromExprs rep
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
80
57
81
58
82data GGColumns
59data GGColumns
@@ -92,19 +69,6 @@ type instance Eval (GGColumns 'Product _Columns rep) = GColumns _Columns rep
92type instance Eval (GGColumns 'Sum _Columns rep) = GColumnsADT _Columns rep
69type instance Eval (GGColumns 'Sum _Columns rep) = GColumnsADT _Columns rep
93
70
94
71
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−
108type GAlgebra :: (Type -> Type) -> Algebra
72type GAlgebra :: (Type -> Type) -> Algebra
109type family GAlgebra rep where
73type family GAlgebra rep where
110 GAlgebra (M1 _ _ rep) = GAlgebra rep
74 GAlgebra (M1 _ _ rep) = GAlgebra rep
@@ -115,74 +79,27 @@ type family GAlgebra rep where
115 GAlgebra (K1 _ _) = 'Product
79 GAlgebra (K1 _ _) = 'Product
116
80
117
81
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.
162 ( KnownAlgebra algebra
83 ( KnownAlgebra algebra
163− , Eval (GGToExprs algebra _ToExprs _Columns exprs rep)
84+ , Eval (GGTable algebra _Table _Columns _FromExprs rep)
164 )
85 )
165− => (forall expr a proxy. Eval (_ToExprs expr a)
86+ => (forall a proxy. Eval (_Table a)
166− => proxy expr
167− -> Eval (_Columns expr) (Col Result)
87+ => proxy a -> Eval (_Columns a) (Col Result) -> Eval (_FromExprs a))
168− -> a)
169− -> Eval (GGColumns algebra _Columns exprs) (Col Result)
88+ -> Eval (GGColumns algebra _Columns rep) (Col Result)
170− -> rep x
89+ -> GMap _FromExprs rep x
171ggfromResult f x = case algebraSing @algebra of
90ggfromResult f x = case algebraSing @algebra of
172− SProduct -> gfromResult @_ToExprs @_Columns @exprs f x
91+ SProduct -> gfromResult @_Table @_Columns @_FromExprs @rep f x
173− SSum -> gfromResultADT @_ToExprs @_Columns @exprs f x
92+ SSum -> gfromResultADT @_Table @_Columns @_FromExprs @rep f x
174
93
175
94
176−ggtoResult :: forall algebra _ToExprs _Columns exprs rep x.
95+ggtoResult :: forall algebra _Table _Columns _FromExprs rep x.
177 ( KnownAlgebra algebra
96 ( KnownAlgebra algebra
178− , Eval (GGToExprs algebra _ToExprs _Columns exprs rep)
97+ , Eval (GGTable algebra _Table _Columns _FromExprs rep)
179 )
98 )
180− => (forall expr a proxy. Eval (_ToExprs expr a)
99+ => (forall a proxy. Eval (_Table a)
181− => proxy expr
182− -> a
183− -> Eval (_Columns expr) (Col Result))
100+ => proxy a -> Eval (_FromExprs a) -> Eval (_Columns a) (Col Result))
184− -> rep x
101+ -> GMap _FromExprs rep x
185− -> Eval (GGColumns algebra _Columns exprs) (Col Result)
102+ -> Eval (GGColumns algebra _Columns rep) (Col Result)
186ggtoResult f x = case algebraSing @algebra of
103ggtoResult f x = case algebraSing @algebra of
187− SProduct -> gtoResult @_ToExprs @_Columns @exprs f x
104+ SProduct -> gtoResult @_Table @_Columns @_FromExprs @rep f x
188− SSum -> gtoResultADT @_ToExprs @_Columns @exprs f x
105+ SSum -> gtoResultADT @_Table @_Columns @_FromExprs @rep f x
src/Rel8/Generic/Table/ADT.hs+61−194
@@ -1,10 +1,8 @@
1{-# language AllowAmbiguousTypes #-}
1{-# language AllowAmbiguousTypes #-}
2{-# language DataKinds #-}
2{-# language DataKinds #-}
3−{-# language FlexibleContexts #-}
4{-# language FlexibleInstances #-}
3{-# language FlexibleInstances #-}
5{-# language LambdaCase #-}
4{-# language LambdaCase #-}
6{-# language MultiParamTypeClasses #-}
5{-# language MultiParamTypeClasses #-}
7−{-# language PolyKinds #-}
8{-# language RankNTypes #-}
6{-# language RankNTypes #-}
9{-# language ScopedTypeVariables #-}
7{-# language ScopedTypeVariables #-}
10{-# language StandaloneKindSignatures #-}
8{-# language StandaloneKindSignatures #-}
@@ -14,9 +12,8 @@
14{-# language UndecidableInstances #-}
12{-# language UndecidableInstances #-}
15
13
16module Rel8.Generic.Table.ADT
14module Rel8.Generic.Table.ADT
17− ( GTableADT, GColumnsADT, gfromColumnsADT, gtoColumnsADT, gtableADT
15+ ( GTableADT, GColumnsADT, gfromResultADT, gtoResultADT
18 , GTableADT', GColumnsADT'
16 , GTableADT', GColumnsADT'
19− , GToExprsADT, gfromResultADT, gtoResultADT
20 )
17 )
21where
18where
22
19
@@ -33,18 +30,14 @@ import Prelude hiding ( null )
33
30
34-- rel8
31-- rel8
35import Rel8.FCF ( Eval, Exp )
32import Rel8.FCF ( Eval, Exp )
36−import Rel8.Generic.Table.Record
33+import Rel8.Generic.Map ( GMap )
37− ( GTable, GColumns, gtable
38− , GToExprs, gfromResult, gtoResult
34+import Rel8.Generic.Table.Record ( GTable, GColumns, gfromResult, gtoResult )
39− )
40−import Rel8.Schema.HTable ( HTable, hmap )
35+import Rel8.Schema.HTable ( HTable )
41import Rel8.Schema.HTable.Identity ( HIdentity( HType ), HType )
36import Rel8.Schema.HTable.Identity ( HIdentity( HType ), HType )
42import Rel8.Schema.HTable.Label ( HLabel, hlabel, hunlabel )
37import Rel8.Schema.HTable.Label ( HLabel, hlabel, hunlabel )
43import Rel8.Schema.HTable.Nullify ( HNullify, hnulls, hnullify, hunnullify )
38import Rel8.Schema.HTable.Nullify ( HNullify, hnulls, hnullify, hunnullify )
44import Rel8.Schema.HTable.Product ( HProduct( HProduct ) )
39import Rel8.Schema.HTable.Product ( HProduct( HProduct ) )
45import qualified Rel8.Schema.Kind as K
40import qualified Rel8.Schema.Kind as K
46−import Rel8.Schema.Null ( Nullify )
47−import Rel8.Schema.Spec ( Spec( Spec ), SSpec )
48import Rel8.Schema.Result
41import Rel8.Schema.Result
49 ( Col( R ), Result
42 ( Col( R ), Result
50 , null, nullifier, unnullifier
43 , null, nullifier, unnullifier
@@ -77,241 +70,119 @@ type family GColumnsADT' _Columns htable rep where
77type GTableADT
70type GTableADT
78 :: (Type -> Exp Constraint)
71 :: (Type -> Exp Constraint)
79 -> (Type -> Exp K.HTable)
72 -> (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)
73+ -> (Type -> Exp Type)
133− -> (Type -> Exp K.HTable)
134− -> K.HTable -> K.HContext -> (Type -> Type) -> Constraint
74+ -> (Type -> Type) -> Constraint
135−class GTableADT' _Table _Columns htable context rep where
75+class GTableADT _Table _Columns _FromExprs 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
185 gfromResultADT :: ()
76 gfromResultADT :: ()
186− => (forall expr a proxy.
77+ => (forall a proxy. Eval (_Table a)
187− ( Eval (_ToExprs expr a)
188− , HTable (Eval (_Columns expr))
189− )
190− => proxy expr
191− -> Eval (_Columns expr) (Col Result)
78+ => proxy a -> Eval (_Columns a) (Col Result) -> Eval (_FromExprs a))
192− -> a)
193− -> GColumnsADT _Columns exprs (Col Result)
79+ -> GColumnsADT _Columns rep (Col Result)
194− -> rep x
80+ -> GMap _FromExprs rep x
195
81
196 gtoResultADT :: ()
82 gtoResultADT :: ()
197− => (forall expr a proxy.
83+ => (forall a proxy. Eval (_Table a)
198− ( Eval (_ToExprs expr a)
199− , HTable (Eval (_Columns expr))
200− )
201− => proxy expr
202− -> a
203− -> Eval (_Columns expr) (Col Result))
84+ => proxy a -> Eval (_FromExprs a) -> Eval (_Columns a) (Col Result))
204− -> rep x
85+ -> GMap _FromExprs rep x
205− -> GColumnsADT _Columns exprs (Col Result)
86+ -> GColumnsADT _Columns rep (Col Result)
206
87
207
88
208instance
89instance
209 ( htable ~ HLabel "tag" (HType Tag)
90 ( htable ~ HLabel "tag" (HType Tag)
91+ , Eval (_Table (htable context))
92+ , Eval (_Columns (htable context)) ~ htable
210− , GToExprsADT' _ToExprs _Columns htable exprs rep
93+ , GTableADT' _Table _Columns _FromExprs htable rep
211 )
94 )
212− => GToExprsADT _ToExprs _Columns (M1 D meta exprs) (M1 D meta rep)
95+ => GTableADT _Table _Columns _FromExprs (M1 D meta rep)
213 where
96 where
214 gfromResultADT fromResult columns =
97 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
216 Just rep -> M1 rep
99 Just rep -> M1 rep
217 _ -> error "ADT.fromColumns: mismatch between tag and data"
100 _ -> error "ADT.fromColumns: mismatch between tag and data"
218 where
101 where
219 tag = (\(HType (R a)) -> a) . hunlabel @"tag"
102 tag = (\(HType (R a)) -> a) . hunlabel @"tag"
220
103
221 gtoResultADT toResult (M1 rep) =
104 gtoResultADT toResult (M1 rep) =
222− gtoResultADT' @_ToExprs @_Columns @_ @exprs toResult tag (Just rep)
105+ gtoResultADT' @_Table @_Columns @_FromExprs @htable @rep toResult tag (Just rep)
223 where
106 where
224 tag = hlabel @"tag" . HType . R
107 tag = hlabel @"tag" . HType . R
225
108
226
109
227−type GToExprsADT'
110+type GTableADT'
228− :: (Type -> Type -> Exp Constraint)
111+ :: (Type -> Exp Constraint)
229 -> (Type -> Exp K.HTable)
112 -> (Type -> Exp K.HTable)
113+ -> (Type -> Exp Type)
230− -> K.HTable -> (Type -> Type) -> (Type -> Type) -> Constraint
114+ -> K.HTable -> (Type -> Type) -> Constraint
231−class GToExprsADT' _ToExprs _Columns htable exprs rep where
115+class GTableADT' _Table _Columns _FromExprs htable rep where
232− gfromResultADT' :: ()
116+ gfromResultADT' :: context ~ Col Result
233− => (forall expr a proxy.
117+ => (forall a proxy. Eval (_Table a)
234− ( Eval (_ToExprs expr a)
118+ => proxy a -> Eval (_Columns a) context -> Eval (_FromExprs a))
235− , HTable (Eval (_Columns expr))
236− )
237− => proxy expr
238− -> Eval (_Columns expr) (Col Result)
239− -> a)
240 -> (htable (Col Result) -> Tag)
119 -> (htable (Col Result) -> Tag)
241− -> GColumnsADT' _Columns htable exprs (Col Result)
120+ -> GColumnsADT' _Columns htable rep context
242− -> Maybe (rep x)
121+ -> Maybe (GMap _FromExprs rep x)
243
122
244− gtoResultADT' :: ()
123+ gtoResultADT' :: context ~ Col Result
245− => (forall expr a proxy.
124+ => (forall a proxy. Eval (_Table a)
246− ( Eval (_ToExprs expr a)
125+ => proxy a -> Eval (_FromExprs a) -> Eval (_Columns a) context)
247− , HTable (Eval (_Columns expr))
248− )
249− => proxy expr
250− -> a
251− -> Eval (_Columns expr) (Col Result))
252 -> (Tag -> htable (Col Result))
126 -> (Tag -> htable (Col Result))
253− -> Maybe (rep x)
127+ -> Maybe (GMap _FromExprs rep x)
254− -> GColumnsADT' _Columns htable exprs (Col Result)
128+ -> GColumnsADT' _Columns htable rep context
255
129
256− extract :: GColumnsADT' _Columns htable exprs context -> htable context
130+ extract :: GColumnsADT' _Columns htable rep context -> htable context
257
131
258
132
259instance
133instance
260 ( htable' ~ GColumnsADT' _Columns htable a
134 ( htable' ~ GColumnsADT' _Columns htable a
261− , GToExprsADT' _ToExprs _Columns htable a rep1
135+ , GTableADT' _Table _Columns _FromExprs htable a
262− , GToExprsADT' _ToExprs _Columns htable' b rep2
136+ , GTableADT' _Table _Columns _FromExprs htable' b
263 )
137 )
264− => GToExprsADT' _ToExprs _Columns htable (a :+: b) (rep1 :+: rep2)
138+ => GTableADT' _Table _Columns _FromExprs htable (a :+: b)
265 where
139 where
266 gfromResultADT' fromResult f columns =
140 gfromResultADT' fromResult f columns =
267 case ma of
141 case ma of
268 Just a -> Just (L1 a)
142 Just a -> Just (L1 a)
269 Nothing -> R1 <$>
143 Nothing -> R1 <$>
270− gfromResultADT' @_ToExprs @_Columns @_ @b @rep2
144+ gfromResultADT' @_Table @_Columns @_FromExprs @_ @b
271 fromResult
145 fromResult
272− (f . extract @_ToExprs @_Columns @_ @a @rep1)
146+ (f . extract @_Table @_Columns @_FromExprs @_ @a)
273 columns
147 columns
274 where
148 where
275 ma =
149 ma =
276− gfromResultADT' @_ToExprs @_Columns @_ @a @rep1
150+ gfromResultADT' @_Table @_Columns @_FromExprs @_ @a
277 fromResult
151 fromResult
278 f
152 f
279− (extract @_ToExprs @_Columns @_ @b @rep2 columns)
153+ (extract @_Table @_Columns @_FromExprs @_ @b columns)
280
154
281 gtoResultADT' toResult tag = \case
155 gtoResultADT' toResult tag = \case
282 Just (L1 a) ->
156 Just (L1 a) ->
283− gtoResultADT' @_ToExprs @_Columns @_ @b @rep2
157+ gtoResultADT' @_Table @_Columns @_FromExprs @_ @b
284 toResult
158 toResult
285− (\_ -> gtoResultADT' @_ToExprs @_Columns @_ @a @rep1
159+ (\_ -> gtoResultADT' @_Table @_Columns @_FromExprs @_ @a
286 toResult
160 toResult
287 tag
161 tag
288 (Just a))
162 (Just a))
289 Nothing
163 Nothing
290 Just (R1 b) ->
164 Just (R1 b) ->
291− gtoResultADT' @_ToExprs @_Columns @_ @b @rep2
165+ gtoResultADT' @_Table @_Columns @_FromExprs @_ @b
292 toResult
166 toResult
293 (\tag' ->
167 (\tag' ->
294− gtoResultADT' @_ToExprs @_Columns @_ @a @rep1
168+ gtoResultADT' @_Table @_Columns @_FromExprs @_ @a
295 toResult
169 toResult
296 (\_ -> tag tag')
170 (\_ -> tag tag')
297 Nothing)
171 Nothing)
298 (Just b)
172 (Just b)
299 Nothing ->
173 Nothing ->
300− gtoResultADT' @_ToExprs @_Columns @_ @b @rep2
174+ gtoResultADT' @_Table @_Columns @_FromExprs @_ @b
301 toResult
175 toResult
302− (\_ -> gtoResultADT' @_ToExprs @_Columns @_ @a @rep1 toResult tag Nothing)
176+ (\_ -> gtoResultADT' @_Table @_Columns @_FromExprs @_ @a toResult tag Nothing)
303 Nothing
177 Nothing
304
178
305 extract =
179 extract =
306− extract @_ToExprs @_Columns @_ @a @rep1 .
180+ extract @_Table @_Columns @_FromExprs @_ @a .
307− extract @_ToExprs @_Columns @_ @b @rep2
181+ extract @_Table @_Columns @_FromExprs @_ @b
308
182
309
183
310−instance
311− ( meta ~ 'MetaCons label _fixity _isRecord
184+instance (meta ~ 'MetaCons label _fixity _isRecord, KnownSymbol label) =>
312− , KnownSymbol label
313− )
314− => GToExprsADT' _ToExprs _Columns htable (M1 C meta U1) (M1 C meta U1)
185+ GTableADT' _Table _Columns _FromExprs htable (M1 C meta U1)
315 where
186 where
316 gfromResultADT' _ tag columns
187 gfromResultADT' _ tag columns
317 | tag columns == tag' = Just (M1 U1)
188 | tag columns == tag' = Just (M1 U1)
@@ -327,18 +198,18 @@ instance
327
198
328
199
329instance {-# OVERLAPPABLE #-}
200instance {-# OVERLAPPABLE #-}
330− ( HTable (GColumns _Columns exprs)
201+ ( HTable (GColumns _Columns rep)
331− , GToExprs _ToExprs _Columns exprs rep
202+ , GTable _Table _Columns _FromExprs rep
332 , meta ~ 'MetaCons label _fixity _isRecord
203 , meta ~ 'MetaCons label _fixity _isRecord
333 , KnownSymbol label
204 , KnownSymbol label
334− , GColumnsADT' _Columns htable (M1 C meta exprs) ~
205+ , GColumnsADT' _Columns htable (M1 C ('MetaCons label _fixity _isRecord) rep) ~
335− HProduct htable (HLabel label (HNullify (GColumns _Columns exprs)))
206+ HProduct htable (HLabel label (HNullify (GColumns _Columns rep)))
336 )
207 )
337− => GToExprsADT' _ToExprs _Columns htable (M1 C meta exprs) (M1 C meta rep)
208+ => GTableADT' _Table _Columns _FromExprs htable (M1 C meta rep)
338 where
209 where
339 gfromResultADT' fromResult tag (HProduct a b)
210 gfromResultADT' fromResult tag (HProduct a b)
340 | tag a == tag' =
211 | tag a == tag' =
341− M1 . gfromResult @_ToExprs @_Columns @exprs fromResult <$>
212+ M1 . gfromResult @_Table @_Columns @_FromExprs @rep fromResult <$>
342 hunnullify unnullifier (hunlabel b)
213 hunnullify unnullifier (hunlabel b)
343 | otherwise = Nothing
214 | otherwise = Nothing
344 where
215 where
@@ -349,12 +220,8 @@ instance {-# OVERLAPPABLE #-}
349 Just (M1 rep) -> HProduct (tag tag') $
220 Just (M1 rep) -> HProduct (tag tag') $
350 hlabel $
221 hlabel $
351 hnullify nullifier $
222 hnullify nullifier $
352− gtoResult @_ToExprs @_Columns @exprs toResult rep
223+ gtoResult @_Table @_Columns @_FromExprs @rep toResult rep
353 where
224 where
354 tag' = Tag $ pack $ symbolVal (Proxy @label)
225 tag' = Tag $ pack $ symbolVal (Proxy @label)
355
226
356 extract (HProduct a _) = a
227 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 @@
13{-# language UndecidableInstances #-}
13{-# language UndecidableInstances #-}
14
14
15module Rel8.Generic.Table.Record
15module Rel8.Generic.Table.Record
16− ( GTable, GColumns, GContext, gfromColumns, gtoColumns, gtable
16+ ( GTable, GColumns, GContext
17− , GToExprs, gfromResult, gtoResult
17+ , gfromColumns, gtoColumns, gfromResult, gtoResult, gtable
18 )
18 )
19where
19where
20
20
@@ -30,12 +30,10 @@ import Prelude hiding ( null )
30
30
31-- rel8
31-- rel8
32import Rel8.FCF ( Eval, Exp )
32import Rel8.FCF ( Eval, Exp )
33−import Rel8.Schema.Context ( Col )
33+import Rel8.Generic.Map ( GMap )
34−import Rel8.Schema.HTable ( HTable )
35import Rel8.Schema.HTable.Label ( HLabel, hlabel, hunlabel )
34import Rel8.Schema.HTable.Label ( HLabel, hlabel, hunlabel )
36import Rel8.Schema.HTable.Product ( HProduct(..) )
35import Rel8.Schema.HTable.Product ( HProduct(..) )
37import qualified Rel8.Schema.Kind as K
36import qualified Rel8.Schema.Kind as K
38−import Rel8.Schema.Result ( Result )
39
37
40
38
41type GColumns :: (Type -> Exp K.HTable) -> (Type -> Type) -> K.HTable
39type GColumns :: (Type -> Exp K.HTable) -> (Type -> Type) -> K.HTable
@@ -58,8 +56,9 @@ type family GContext _Context rep where
58type GTable
56type GTable
59 :: (Type -> Exp Constraint)
57 :: (Type -> Exp Constraint)
60 -> (Type -> Exp K.HTable)
58 -> (Type -> Exp K.HTable)
59+ -> (Type -> Exp Type)
61− -> K.HContext -> (Type -> Type) -> Constraint
60+ -> (Type -> Type) -> Constraint
62−class GTable _Table _Columns context rep
61+class GTable _Table _Columns _FromExprs rep
63 where
62 where
64 gfromColumns :: ()
63 gfromColumns :: ()
65 => (forall a. Eval (_Table a) => Eval (_Columns a) context -> a)
64 => (forall a. Eval (_Table a) => Eval (_Columns a) context -> a)
@@ -71,46 +70,73 @@ class GTable _Table _Columns context rep
71 -> rep x
70 -> rep x
72 -> GColumns _Columns rep context
71 -> GColumns _Columns rep context
73
72
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+
74 gtable :: ()
85 gtable :: ()
75 => (forall a proxy. Eval (_Table a) => proxy a -> Eval (_Columns a) context)
86 => (forall a proxy. Eval (_Table a) => proxy a -> Eval (_Columns a) context)
76 -> GColumns _Columns rep context
87 -> GColumns _Columns rep context
77
88
78
89
79−instance GTable _Table _Columns context rep =>
90+instance GTable _Table _Columns _FromExprs rep =>
80− GTable _Table _Columns context (M1 D c rep)
91+ GTable _Table _Columns _FromExprs (M1 D c rep)
81 where
92 where
82 gfromColumns fromColumns =
93 gfromColumns fromColumns =
83− M1 . gfromColumns @_Table @_Columns @context @rep fromColumns
94+ M1 . gfromColumns @_Table @_Columns @_FromExprs @rep fromColumns
84 gtoColumns toColumns (M1 a) =
95 gtoColumns toColumns (M1 a) =
85− gtoColumns @_Table @_Columns @context @rep toColumns a
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
86− gtable = gtable @_Table @_Columns @context @rep
101+ gtable = gtable @_Table @_Columns @_FromExprs @rep
87
102
88
103
89−instance GTable _Table _Columns context rep =>
104+instance GTable _Table _Columns _FromExprs rep =>
90− GTable _Table _Columns context (M1 C c rep)
105+ GTable _Table _Columns _FromExprs (M1 C c rep)
91 where
106 where
92 gfromColumns fromColumns =
107 gfromColumns fromColumns =
93− M1 . gfromColumns @_Table @_Columns @context @rep fromColumns
108+ M1 . gfromColumns @_Table @_Columns @_FromExprs @rep fromColumns
94 gtoColumns toColumns (M1 a) =
109 gtoColumns toColumns (M1 a) =
95− gtoColumns @_Table @_Columns @context @rep toColumns a
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
96− gtable = gtable @_Table @_Columns @context @rep
115+ gtable = gtable @_Table @_Columns @_FromExprs @rep
97
116
98
117
99instance
118instance
100− ( GTable _Table _Columns context rep1
119+ ( GTable _Table _Columns _FromExprs rep1
101− , GTable _Table _Columns context rep2
120+ , GTable _Table _Columns _FromExprs rep2
102 )
121 )
103− => GTable _Table _Columns context (rep1 :*: rep2)
122+ => GTable _Table _Columns _FromExprs (rep1 :*: rep2)
104 where
123 where
105 gfromColumns fromColumns (HProduct a b) =
124 gfromColumns fromColumns (HProduct a b) =
106− gfromColumns @_Table @_Columns @context @rep1 fromColumns a :*:
125+ gfromColumns @_Table @_Columns @_FromExprs @rep1 fromColumns a :*:
107− gfromColumns @_Table @_Columns @context @rep2 fromColumns b
126+ gfromColumns @_Table @_Columns @_FromExprs @rep2 fromColumns b
108 gtoColumns toColumns (a :*: b) = HProduct
127 gtoColumns toColumns (a :*: b) = HProduct
109− (gtoColumns @_Table @_Columns @context @rep1 toColumns a)
128+ (gtoColumns @_Table @_Columns @_FromExprs @rep1 toColumns a)
110− (gtoColumns @_Table @_Columns @context @rep2 toColumns b)
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)
111 gtable table = HProduct
137 gtable table = HProduct
112− (gtable @_Table @_Columns @context @rep1 table)
138+ (gtable @_Table @_Columns @_FromExprs @rep1 table)
113− (gtable @_Table @_Columns @context @rep2 table)
139+ (gtable @_Table @_Columns @_FromExprs @rep2 table)
114
140
115
141
116instance
142instance
@@ -118,83 +144,10 @@ instance
118 , meta ~ 'MetaSel ('Just label) _su _ss _ds
144 , meta ~ 'MetaSel ('Just label) _su _ss _ds
119 , k1 ~ K1 i a
145 , k1 ~ K1 i a
120 )
146 )
121− => GTable _Table _Columns context (M1 S meta k1)
147+ => GTable _Table _Columns _FromExprs (M1 S meta k1)
122 where
148 where
123 gfromColumns fromColumns = M1 . K1 . fromColumns . hunlabel
149 gfromColumns fromColumns = M1 . K1 . fromColumns . hunlabel
124 gtoColumns toColumns (M1 (K1 a)) = hlabel (toColumns a)
150 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)
125 gtable table = hlabel (table (Proxy @a))
153 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 @@
1{-# language DataKinds #-}
1{-# language DataKinds #-}
2{-# language GADTs #-}
2{-# language GADTs #-}
3−{-# language LambdaCase #-}
4{-# language StandaloneKindSignatures #-}
3{-# language StandaloneKindSignatures #-}
5
4
6module Rel8.Kind.Context
5module Rel8.Kind.Context
7 ( Reifiable( contextSing )
6 ( Reifiable( contextSing )
8 , SContext(..)
7 , SContext(..)
9− , sReifiable
10 )
8 )
11where
9where
12
10
@@ -17,11 +15,8 @@ import Prelude ()
17-- rel8
15-- rel8
18import Rel8.Aggregate ( Aggregate )
16import Rel8.Aggregate ( Aggregate )
19import Rel8.Expr ( Expr )
17import Rel8.Expr ( Expr )
20−import Rel8.Schema.Dict ( Dict( Dict ) )
21−import Rel8.Schema.Context ( Interpretation )
22import Rel8.Schema.Kind ( Context )
18import Rel8.Schema.Kind ( Context )
23import Rel8.Schema.Name ( Name )
19import Rel8.Schema.Name ( Name )
24−import Rel8.Schema.Reify ( Reify )
25import Rel8.Schema.Result ( Result )
20import Rel8.Schema.Result ( Result )
26
21
27
22
@@ -31,11 +26,10 @@ data SContext context where
31 SExpr :: SContext Expr
26 SExpr :: SContext Expr
32 SName :: SContext Name
27 SName :: SContext Name
33 SResult :: SContext Result
28 SResult :: SContext Result
34− SReify :: SContext context -> SContext (Reify context)
35
29
36
30
37type Reifiable :: Context -> Constraint
31type Reifiable :: Context -> Constraint
38−class Interpretation context => Reifiable context where
32+class Reifiable context where
39 contextSing :: SContext context
33 contextSing :: SContext context
40
34
41
35
@@ -53,17 +47,3 @@ instance Reifiable Result where
53
47
54instance Reifiable Name where
48instance Reifiable Name where
55 contextSing = SName
49 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 @@
4
4
5module Rel8.Schema.Context
5module Rel8.Schema.Context
6 ( Interpretation( Col )
6 ( Interpretation( Col )
7+ , UnCol
7 )
8 )
8where
9where
9
10
@@ -18,3 +19,8 @@ import Rel8.Schema.Kind ( Context, HContext )
18type Interpretation :: Context -> Constraint
19type Interpretation :: Context -> Constraint
19class Interpretation context where
20class Interpretation context where
20 data Col context :: HContext
21 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
15where
15where
16
16
17-- base
17-- base
18−import Data.Bifunctor ( bimap )
19import Data.Bool ( bool )
18import Data.Bool ( bool )
20import Data.Kind ( Constraint, Type )
19import Data.Kind ( Constraint, Type )
21import Data.Monoid ( getFirst )
20import Data.Monoid ( getFirst )
@@ -37,7 +36,6 @@ import Rel8.Kind.Context ( SContext(..) )
37import qualified Rel8.Schema.Kind as K
36import qualified Rel8.Schema.Kind as K
38import Rel8.Schema.Name ( Col( N ), Name( Name ) )
37import Rel8.Schema.Name ( Col( N ), Name( Name ) )
39import Rel8.Schema.Null ( Nullify, Nullity( Null, NotNull ) )
38import Rel8.Schema.Null ( Nullify, Nullity( Null, NotNull ) )
40−import Rel8.Schema.Reify ( Col( Reify ), Reify )
41import Rel8.Schema.Result ( Col( R ), Result )
39import Rel8.Schema.Result ( Col( R ), Result )
42import Rel8.Schema.Spec ( Spec( Spec ), SSpec(..) )
40import Rel8.Schema.Spec ( Spec( Spec ), SSpec(..) )
43
41
@@ -47,7 +45,6 @@ data Nullifiability context where
47 NAggregate :: Nullifiability Aggregate
45 NAggregate :: Nullifiability Aggregate
48 NExpr :: Nullifiability Expr
46 NExpr :: Nullifiability Expr
49 NName :: Nullifiability Name
47 NName :: Nullifiability Name
50− NReify :: Nullifiability context -> Nullifiability (Reify context)
51
48
52
49
53type Nullifiable :: K.Context -> Constraint
50type Nullifiable :: K.Context -> Constraint
@@ -67,14 +64,9 @@ instance Nullifiable Name where
67 nullifiability = NName
64 nullifiability = NName
68
65
69
66
70−instance Nullifiable context => Nullifiable (Reify context) where
71− nullifiability = NReify nullifiability
72−
73−
74type NonNullifiability :: K.Context -> Type
67type NonNullifiability :: K.Context -> Type
75data NonNullifiability context where
68data NonNullifiability context where
76 NNResult :: NonNullifiability Result
69 NNResult :: NonNullifiability Result
77− NNReify :: NonNullifiability context -> NonNullifiability (Reify context)
78
70
79
71
80nullifiableOrNot :: ()
72nullifiableOrNot :: ()
@@ -85,7 +77,6 @@ nullifiableOrNot = \case
85 SExpr -> Right NExpr
77 SExpr -> Right NExpr
86 SName -> Right NName
78 SName -> Right NName
87 SResult -> Left NNResult
79 SResult -> Left NNResult
88− SReify context -> bimap NNReify NReify $ nullifiableOrNot context
89
80
90
81
91absurd :: Nullifiability context -> NonNullifiability context -> a
82absurd :: Nullifiability context -> NonNullifiability context -> a
@@ -93,8 +84,6 @@ absurd = \case
93 NAggregate -> \case
84 NAggregate -> \case
94 NExpr -> \case
85 NExpr -> \case
95 NName -> \case
86 NName -> \case
96− NReify context -> \case
97− NNReify context' -> absurd context context'
98
87
99
88
100guarder :: ()
89guarder :: ()
@@ -119,8 +108,6 @@ guarder SName _ _ _ name = name
119guarder SResult (R tag) isNonNull _ (R a) = R (bool Nothing a condition)
108guarder SResult (R tag) isNonNull _ (R a) = R (bool Nothing a condition)
120 where
109 where
121 condition = isNonNull tag
110 condition = isNonNull tag
122−guarder (SReify context) (Reify tag) isNonNull isNonNullExpr (Reify a) =
123− Reify $ guarder context tag isNonNull isNonNullExpr a
124
111
125
112
126nullifier :: ()
113nullifier :: ()
@@ -132,7 +119,6 @@ nullifier NAggregate SSpec {nullity} (A (Aggregate a)) =
132 A $ Aggregate $ snullify nullity <$> a
119 A $ Aggregate $ snullify nullity <$> a
133nullifier NExpr SSpec {nullity} (E a) = E $ snullify nullity a
120nullifier NExpr SSpec {nullity} (E a) = E $ snullify nullity a
134nullifier NName _ (N (Name a)) = N $ Name a
121nullifier NName _ (N (Name a)) = N $ Name a
135−nullifier (NReify context) spec (Reify a) = Reify $ nullifier context spec a
136
122
137
123
138unnullifier :: ()
124unnullifier :: ()
@@ -144,7 +130,6 @@ unnullifier NAggregate SSpec {nullity} (A (Aggregate a)) =
144 A $ Aggregate $ sunnullify nullity <$> a
130 A $ Aggregate $ sunnullify nullity <$> a
145unnullifier NExpr SSpec {nullity} (E a) = E $ sunnullify nullity a
131unnullifier NExpr SSpec {nullity} (E a) = E $ sunnullify nullity a
146unnullifier NName _ (N (Name a)) = N $ Name a
132unnullifier NName _ (N (Name a)) = N $ Name a
147−unnullifier (NReify context) spec (Reify a) = Reify (unnullifier context spec a)
148
133
149
134
150sguard :: Expr Bool -> Expr (Maybe a) -> Expr (Maybe a)
135sguard :: 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
20where
20where
21
21
22-- base
22-- base
23−import Data.Functor.Identity ( Identity )
24import Data.Kind ( Constraint, Type )
23import Data.Kind ( Constraint, Type )
25import Data.String ( IsString, fromString )
24import Data.String ( IsString, fromString )
26import Prelude
25import Prelude
@@ -30,12 +29,11 @@ import Rel8.Expr ( Expr )
30import Rel8.Schema.Context ( Interpretation, Col )
29import Rel8.Schema.Context ( Interpretation, Col )
31import Rel8.Schema.HTable.Identity ( HIdentity( HType ), HType )
30import Rel8.Schema.HTable.Identity ( HIdentity( HType ), HType )
32import Rel8.Schema.Null ( Sql )
31import Rel8.Schema.Null ( Sql )
33−import Rel8.Schema.Reify ( notReify )
32+import Rel8.Schema.Result ( Col( R ) )
34−import Rel8.Schema.Result ( Result )
35import Rel8.Schema.Spec ( Spec( Spec ) )
33import Rel8.Schema.Spec ( Spec( Spec ) )
36import Rel8.Table
34import Rel8.Table
37 ( Table, Columns, Context, fromColumns, toColumns
35 ( Table, Columns, Context, fromColumns, toColumns
38− , reify, unreify, coherence, congruence
36+ , FromExprs, fromResult, toResult
39 )
37 )
40import Rel8.Table.Recontextualize ( Recontextualize )
38import Rel8.Table.Recontextualize ( Recontextualize )
41import Rel8.Type ( DBType )
39import Rel8.Type ( DBType )
@@ -60,27 +58,20 @@ instance k ~ Type => IsString (Name (a :: k)) where
60instance Sql DBType a => Table Name (Name a) where
58instance Sql DBType a => Table Name (Name a) where
61 type Columns (Name a) = HType a
59 type Columns (Name a) = HType a
62 type Context (Name a) = Name
60 type Context (Name a) = Name
61+ type FromExprs (Name a) = a
63
62
64 toColumns a = HType (N a)
63 toColumns a = HType (N a)
65 fromColumns (HType (N a)) = a
64 fromColumns (HType (N a)) = a
66− reify = notReify
65+ toResult a = HType (R a)
67− unreify = notReify
66+ fromResult (HType (R a)) = a
68− coherence = notReify
69− congruence = notReify
70
67
71
68
72instance Sql DBType a => Recontextualize Expr Name (Expr a) (Name a)
69instance Sql DBType a => Recontextualize Expr Name (Expr a) (Name a)
73
70
74
71
75−instance Sql DBType a => Recontextualize Result Name (Identity a) (Name a)
76−
77−
78instance Sql DBType a => Recontextualize Name Expr (Name a) (Expr a)
72instance Sql DBType a => Recontextualize Name Expr (Name a) (Expr a)
79
73
80
74
81−instance Sql DBType a => Recontextualize Name Result (Name a) (Identity a)
82−
83−
84instance Sql DBType a => Recontextualize Name Name (Name a) (Name a)
75instance Sql DBType a => Recontextualize Name Name (Name a) (Name a)
85
76
86
77
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 @@
1{-# language DataKinds #-}
1{-# language DataKinds #-}
2−{-# language EmptyCase #-}
3{-# language GADTs #-}
2{-# language GADTs #-}
4−{-# language LambdaCase #-}
5{-# language NamedFieldPuns #-}
3{-# language NamedFieldPuns #-}
6{-# language StandaloneKindSignatures #-}
4{-# language StandaloneKindSignatures #-}
7{-# language TypeFamilies #-}
5{-# language TypeFamilies #-}
8
6
9module Rel8.Schema.Result
7module Rel8.Schema.Result
10 ( Col( R, unR ), Result
8 ( Col( R, unR ), Result
11− , NotResult( NotResult ), absurd
12 , null, nullifier, unnullifier
9 , null, nullifier, unnullifier
13 , vectorizer, unvectorizer
10 , vectorizer, unvectorizer
14 )
11 )
15where
12where
16
13
17-- base
14-- base
18−import Data.Kind ( Type )
19import Prelude hiding ( null )
15import Prelude hiding ( null )
20
16
21-- rel8
17-- rel8
@@ -38,21 +34,6 @@ instance Interpretation Result where
38 R :: {unR :: !a} -> Col Result ('Spec a)
34 R :: {unR :: !a} -> Col Result ('Spec a)
39
35
40
36
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−
56null :: Col Result ('Spec (Maybe a))
37null :: Col Result ('Spec (Maybe a))
57null = R Nothing
38null = R Nothing
58
39
src/Rel8/Table.hs+82−295
@@ -1,83 +1,44 @@
1{-# language AllowAmbiguousTypes #-}
1{-# language AllowAmbiguousTypes #-}
2{-# language DataKinds #-}
2{-# language DataKinds #-}
3{-# language DefaultSignatures #-}
3{-# language DefaultSignatures #-}
4−{-# language DisambiguateRecordFields #-}
5{-# language FlexibleContexts #-}
4{-# language FlexibleContexts #-}
6{-# language FlexibleInstances #-}
5{-# language FlexibleInstances #-}
7{-# language FunctionalDependencies #-}
6{-# language FunctionalDependencies #-}
8−{-# language LambdaCase #-}
9−{-# language NamedFieldPuns #-}
10{-# language ScopedTypeVariables #-}
7{-# language ScopedTypeVariables #-}
11{-# language StandaloneKindSignatures #-}
8{-# language StandaloneKindSignatures #-}
12{-# language TypeApplications #-}
9{-# language TypeApplications #-}
13{-# language TypeFamilies #-}
10{-# language TypeFamilies #-}
14−{-# language TypeOperators #-}
15{-# language UndecidableInstances #-}
11{-# language UndecidableInstances #-}
16
12
17module Rel8.Table
13module Rel8.Table
18 ( Table
14 ( Table
19− ( Columns, Context, toColumns, fromColumns
15+ ( Columns, Context, fromColumns, toColumns
20− , Unreify, reify, unreify, coherence, congruence
16+ , FromExprs, fromResult, toResult
21 )
17 )
22 , Congruent
18 , Congruent
23− , TTable, TColumns, TContext, TUnreify
19+ , TTable, TColumns, TContext, TFromExprs
24 )
20 )
25where
21where
26
22
27-- base
23-- base
28−import Data.Functor ( ($>) )
29−import Data.Functor.Identity ( Identity( Identity ) )
30import Data.Kind ( Constraint, Type )
24import Data.Kind ( Constraint, Type )
31−import Data.List.NonEmpty ( NonEmpty )
32−import Data.Proxy ( Proxy( Proxy ) )
33−import Data.Type.Equality ( (:~:)( Refl ) )
34import GHC.Generics ( Generic, Rep, from, to )
25import GHC.Generics ( Generic, Rep, from, to )
35import Prelude hiding ( null )
26import Prelude hiding ( null )
36
27
37-- rel8
28-- rel8
38import Rel8.FCF ( Eval, Exp )
29import Rel8.FCF ( Eval, Exp )
39−import Rel8.Kind.Algebra
30+import Rel8.Generic.Map ( GMap )
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
31+import Rel8.Generic.Table.Record
46− ( GGTable, GGColumns, GGContext, ggfromColumns, ggtoColumns
32+ ( GTable, GColumns, GContext
47− , GAlgebra
33+ , gfromColumns, gtoColumns, gfromResult, gtoResult
48 )
34 )
49import Rel8.Generic.Record ( Record(..) )
35import Rel8.Generic.Record ( Record(..) )
50−import Rel8.Generic.Reify ( ARep )
36+import Rel8.Schema.Context ( Col, UnCol )
51import Rel8.Schema.HTable ( HTable )
37import Rel8.Schema.HTable ( HTable )
52−import Rel8.Schema.HTable.Either ( HEitherTable(..) )
38+import Rel8.Schema.HTable.Identity ( HIdentity(..) )
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 )
61import qualified Rel8.Schema.Kind as K
39import qualified Rel8.Schema.Kind as K
62−import Rel8.Schema.Null ( Sql )
40+import Rel8.Schema.Result ( Result )
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− )
74import Rel8.Schema.Spec ( KnownSpec )
41import 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 )
81
42
82
43
83-- | @Table@s are one of the foundational elements of Rel8, and describe data
44-- | @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
99 -- | The common context that all columns use as an interpretation.
60 -- | The common context that all columns use as an interpretation.
100 type Context a :: K.Context
61 type Context a :: K.Context
101
62
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
103
66
104 toColumns :: a -> Columns a (Col context)
67 toColumns :: a -> Columns a (Col context)
105 fromColumns :: Columns a (Col context) -> a
68 fromColumns :: Columns a (Col context) -> a
106
69
107− reify :: context :~: Reify ctx -> Unreify a -> a
70+ fromResult :: Columns a (Col Result) -> FromExprs a
108− unreify :: context :~: Reify ctx -> a -> Unreify a
71+ toResult :: FromExprs a -> Columns a (Col Result)
109− coherence :: context :~: Reify ctx -> NotResult ctx -> Context (Unreify a) :~: ctx
110− congruence :: context :~: Reify ctx -> NotResult ctx -> Columns a :~: Columns (Unreify a)
111−
112
72
113− type Columns a = Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))
73+ type Columns a = GColumns TColumns (Rep (Record a))
114− type Context a = Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record a)))
74+ type Context a = GContext TContext (Rep (Record a))
115− type Unreify a = DefaultUnreify a
75+ type FromExprs a = DefaultFromExprs a
116
76
117 default toColumns ::
77 default toColumns ::
118 ( Generic (Record a)
78 ( Generic (Record a)
119− , KnownAlgebra (GAlgebra (Rep (Record a)))
120− , Eval (GGTable (GAlgebra (Rep (Record a))) (TTable context) TColumns (Col context) (Rep (Record a)))
79+ , GTable (TTable context) TColumns TFromExprs (Rep (Record a))
121− , Columns a ~ Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))
80+ , Columns a ~ GColumns TColumns (Rep (Record a))
122− , Context a ~ Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record a)))
123 )
81 )
124 => a -> Columns a (Col context)
82 => a -> Columns a (Col context)
125 toColumns =
83 toColumns =
126− ggtoColumns
84+ gtoColumns
127− @(GAlgebra (Rep (Record a)))
128 @(TTable context)
85 @(TTable context)
129 @TColumns
86 @TColumns
130− id
87+ @TFromExprs
131− id
132 toColumns .
88 toColumns .
133 from .
89 from .
134 Record
90 Record
135
91
136 default fromColumns ::
92 default fromColumns ::
137 ( Generic (Record a)
93 ( Generic (Record a)
138− , KnownAlgebra (GAlgebra (Rep (Record a)))
139− , Eval (GGTable (GAlgebra (Rep (Record a))) (TTable context) TColumns (Col context) (Rep (Record a)))
94+ , GTable (TTable context) TColumns TFromExprs (Rep (Record a))
140− , Columns a ~ Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))
95+ , Columns a ~ GColumns TColumns (Rep (Record a))
141− , Context a ~ Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record a)))
142 )
96 )
143 => Columns a (Col context) -> a
97 => Columns a (Col context) -> a
144 fromColumns =
98 fromColumns =
145 unrecord .
99 unrecord .
146 to .
100 to .
147− ggfromColumns
101+ gfromColumns
148− @(GAlgebra (Rep (Record a)))
149 @(TTable context)
102 @(TTable context)
150 @TColumns
103 @TColumns
151− id
104+ @TFromExprs
152− id
153 fromColumns
105 fromColumns
154
106
155− default reify ::
107+ default toResult ::
156− ( Generic (Record a)
108+ ( Generic (Record (FromExprs a))
157− , Generic (Record (Unreify a))
158− , GMappable (TTable context) (Rep (Record a))
109+ , GTable (TTable context) TColumns TFromExprs (Rep (Record a))
159− , Rep (Record (Unreify a)) ~ GMap TUnreify (Rep (Record a))
110+ , Columns a ~ GColumns TColumns (Rep (Record a))
111+ , Rep (Record (FromExprs a)) ~ GMap TFromExprs (Rep (Record a))
160 )
112 )
161− => context :~: Reify ctx -> Unreify a -> a
113+ => FromExprs a -> Columns a (Col Result)
162− reify Refl =
114+ toResult =
163− unrecord .
115+ gtoResult
164− to .
165− gunmap @(TTable context) (Proxy @TUnreify) (reify Refl) .
116+ @(TTable context)
117+ @TColumns
118+ @TFromExprs
119+ @(Rep (Record a))
120+ (\(_ :: proxy x) -> toResult @(Context x) @x) .
166 from .
121 from .
167 Record
122 Record
168
123
169− default unreify ::
124+ default fromResult ::
170− ( Generic (Record a)
125+ ( Generic (Record (FromExprs a))
171− , Generic (Record (Unreify a))
172− , GMappable (TTable context) (Rep (Record a))
126+ , GTable (TTable context) TColumns TFromExprs (Rep (Record a))
173− , Rep (Record (Unreify a)) ~ GMap TUnreify (Rep (Record a))
127+ , Columns a ~ GColumns TColumns (Rep (Record a))
128+ , Rep (Record (FromExprs a)) ~ GMap TFromExprs (Rep (Record a))
174 )
129 )
175− => context :~: Reify ctx -> a -> Unreify a
130+ => Columns a (Col Result) -> FromExprs a
176− unreify Refl =
131+ fromResult =
177 unrecord .
132 unrecord .
178 to .
133 to .
134+ gfromResult
179− gmap @(TTable context) (Proxy @TUnreify) (unreify Refl) .
135+ @(TTable context)
180− from .
136+ @TColumns
181− Record
137+ @TFromExprs
182−
183− default coherence ::
184− ( KnownAlgebra (GAlgebra (Rep (Record a)))
138+ @(Rep (Record a))
185− , GCoherent (TTable context) (Rep (Record a))
139+ (\(_ :: proxy x) -> fromResult @(Context x) @x)
186− , Context a ~ Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record a)))
140+
187− , Context (Unreify a) ~ Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record (Unreify a))))
141+
188− , Rep (Record (Unreify a)) ~ GMap TUnreify (Rep (Record a))
142+type DefaultFromExprs :: Type -> Type
189− )
143+type family DefaultFromExprs a where
190− => context :~: Reify ctx -> NotResult ctx -> Context (Unreify a) :~: ctx
144+ DefaultFromExprs (t a b c d e f g) =
191− coherence = case algebraSing @(GAlgebra (Rep (Record a))) of
145+ t (FromExprs a) (FromExprs b) (FromExprs c) (FromExprs d) (FromExprs e)
192− SSum -> notReify
146+ (FromExprs f) (FromExprs g)
193− SProduct -> \proof abstract ->
147+ DefaultFromExprs (t a b c d e f) =
194− gcoherence
148+ t (FromExprs a) (FromExprs b) (FromExprs c) (FromExprs d) (FromExprs e)
195− @(TTable context)
149+ (FromExprs f)
196− @(Rep (Record a))
150+ DefaultFromExprs (t a b c d e) =
197− (Proxy @TContext)
151+ t (FromExprs a) (FromExprs b) (FromExprs c) (FromExprs d) (FromExprs e)
198− (Proxy @TUnreify)
152+ DefaultFromExprs (t a b c d) =
199− (\(_ :: _proxy x) -> coherence @context @x proof abstract)
153+ t (FromExprs a) (FromExprs b) (FromExprs c) (FromExprs d)
200−
154+ DefaultFromExprs (t a b c) = t (FromExprs a) (FromExprs b) (FromExprs c)
201− default congruence ::
155+ DefaultFromExprs (t a b) = t (FromExprs a) (FromExprs b)
202− ( KnownAlgebra (GAlgebra (Rep (Record a)))
156+ DefaultFromExprs (t a) = t (FromExprs 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)
219
157
220
158
221data TTable :: K.Context -> Type -> Exp Constraint
159data TTable :: K.Context -> Type -> Exp Constraint
@@ -230,185 +168,34 @@ data TContext :: Type -> Exp K.Context
230type instance Eval (TContext a) = Context a
168type instance Eval (TContext a) = Context a
231
169
232
170
233−data TUnreify :: Type -> Exp Type
171+data TFromExprs :: Type -> Exp Type
234−type instance Eval (TUnreify a) = Unreify a
172+type instance Eval (TFromExprs a) = FromExprs 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))
251
173
252
174
253-- | Any 'HTable' is also a 'Table'.
175-- | Any 'HTable' is also a 'Table'.
176+instance (context ~ UnCol hcontext, hcontext ~ Col context, HTable t) =>
254−instance HTable t => Table context (t (Col context)) where
177+ Table context (t hcontext)
178+ where
255− type Columns (t (Col context)) = t
179+ type Columns (t hcontext) = t
256− type Context (t (Col context)) = context
180+ type Context (t hcontext) = UnCol hcontext
257− type Unreify (t (Col context)) = t (Col (UnwrapReify context))
181+ type FromExprs (t hcontext) = t (Col Result)
258
182
259 toColumns = id
183 toColumns = id
260 fromColumns = id
184 fromColumns = id
261−
185+ toResult = id
262− reify Refl = hreify
186+ fromResult = id
263− unreify Refl = hunreify
264− coherence Refl _ = Refl
265− congruence Refl _ = Refl
266
187
267
188
268-- | Any context is trivially a table.
189-- | Any context is trivially a table.
269instance KnownSpec spec => Table context (Col context spec) where
190instance KnownSpec spec => Table context (Col context spec) where
270 type Columns (Col context spec) = HIdentity spec
191 type Columns (Col context spec) = HIdentity spec
271 type Context (Col context spec) = context
192 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
273
194
274 toColumns = HIdentity
195 toColumns = HIdentity
275 fromColumns = unHIdentity
196 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))
197+ toResult = HIdentity
343− , hjust = hlabel (hnulls (const null))
198+ fromResult = unHIdentity
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
412
199
413
200
414instance (Table context a, Table context b) => Table context (a, b)
201instance (Table context a, Table context b) => Table context (a, b)
src/Rel8/Table/ADT.hs+33−59
@@ -13,7 +13,7 @@
13
13
14module Rel8.Table.ADT
14module Rel8.Table.ADT
15 ( ADT( ADT )
15 ( ADT( ADT )
16− , ADTable, fromADT, toADT
16+ , ADTable
17 , BuildableADT
17 , BuildableADT
18 , BuildADT, buildADT
18 , BuildADT, buildADT
19 , ConstructableADT
19 , ConstructableADT
@@ -27,8 +27,6 @@ where
27
27
28-- base
28-- base
29import Data.Kind ( Constraint, Type )
29import Data.Kind ( Constraint, Type )
30−import Data.Proxy ( Proxy( Proxy ) )
31−import Data.Type.Equality ( (:~:)( Refl ) )
32import GHC.Generics ( Generic, Rep, from, to )
30import GHC.Generics ( Generic, Rep, from, to )
33import GHC.TypeLits ( Symbol )
31import GHC.TypeLits ( Symbol )
34import Prelude
32import Prelude
@@ -46,12 +44,12 @@ import Rel8.Generic.Construction
46 , GGName, ggname
44 , GGName, ggname
47 , GGAggregate, ggaggregate
45 , GGAggregate, ggaggregate
48 )
46 )
49−import Rel8.Generic.Map ( GMappable, GMap, gmap, gunmap )
47+import Rel8.Generic.Map ( GMap )
50−import Rel8.Generic.Record ( GRecordable, GRecord, grecord, gunrecord )
48+import Rel8.Generic.Record ( Record( Record ), unrecord )
51import Rel8.Generic.Rel8able
49import Rel8.Generic.Rel8able
52 ( Rel8able
50 ( Rel8able
53 , GRep, GColumns, gfromColumns, gtoColumns
51 , GRep, GColumns, gfromColumns, gtoColumns
54− , greify, gunreify
52+ , GFromExprs, gfromResult, gtoResult
55 )
53 )
56import qualified Rel8.Generic.Table.ADT as G
54import qualified Rel8.Generic.Table.ADT as G
57import qualified Rel8.Kind.Algebra as K
55import qualified Rel8.Kind.Algebra as K
@@ -59,12 +57,10 @@ import Rel8.Schema.Context ( Col )
59import Rel8.Schema.HTable ( HTable )
57import Rel8.Schema.HTable ( HTable )
60import qualified Rel8.Schema.Kind as K
58import qualified Rel8.Schema.Kind as K
61import Rel8.Schema.Name ( Name )
59import Rel8.Schema.Name ( Name )
62−import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify )
63import Rel8.Schema.Result ( Result )
60import Rel8.Schema.Result ( Result )
64import Rel8.Table
61import Rel8.Table
65− ( Table
62+ ( Table, fromResult, toResult
66− , fromColumns, toColumns, reify, unreify
67− , TTable, TColumns, TUnreify
63+ , TTable, TColumns, TFromExprs
68 )
64 )
69
65
70
66
@@ -74,67 +70,45 @@ newtype ADT t context = ADT (GColumnsADT t (Col context))
74
70
75instance ADTable t => Rel8able (ADT t) where
71instance ADTable t => Rel8able (ADT t) where
76 type GColumns (ADT t) = GColumnsADT t
72 type GColumns (ADT t) = GColumnsADT t
73+ type GFromExprs (ADT t) = t Result
77
74
78− gfromColumns = ADT
75+ gfromColumns _ = ADT
79− gtoColumns (ADT a) = a
76+ gtoColumns _ (ADT a) = a
80
77
81− greify (ADT a) = ADT (hreify a)
78+ gfromResult =
82− gunreify (ADT a) = ADT (hunreify a)
79+ unrecord .
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 =
80+ to .
101− ADT .
81+ G.gfromResultADT
102− hunreify .
103− G.gtoColumnsADT
104− @(TTable (Reify Result))
82+ @(TTable Expr)
105 @TColumns
83 @TColumns
106− (\(Reify a) -> a)
84+ @TFromExprs
107− Reify
85+ @(Eval (ADTRep t Expr))
108− toColumns .
86+ (\(_ :: proxy x) -> fromResult @_ @x)
109− grecord @(Rep (t (Reify Result))) .
110− gunmap @(TTable (Reify Result)) (Proxy @TUnreify) (reify Refl)
111
87
112−
88+ gtoResult =
113−fromADT :: ADTable t => ADT t Result -> t Result
89+ G.gtoResultADT
114−fromADT = to . from
90+ @(TTable Expr)
115−
91+ @TColumns
116−
92+ @TFromExprs
117−toADT :: ADTable t => t Result -> ADT t Result
93+ @(Eval (ADTRep t Expr))
118−toADT = to . from
94+ (\(_ :: proxy x) -> toResult @_ @x) .
95+ from .
96+ Record
119
97
120
98
121type ADTable :: K.Rel8able -> Constraint
99type ADTable :: K.Rel8able -> Constraint
122class
100class
123− ( Generic (t Result)
101+ ( Generic (Record (t Result))
124 , HTable (GColumnsADT t)
102 , HTable (GColumnsADT t)
125− , G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (Rep (t (Reify Result))))
103+ , G.GTableADT (TTable Expr) TColumns TFromExprs (Eval (ADTRep t Expr))
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)
104+ , GMap TFromExprs (Rep (Record (t Expr))) ~ Rep (Record (t Result))
129 )
105 )
130 => ADTable t
106 => ADTable t
131instance
107instance
132− ( Generic (t Result)
108+ ( Generic (Record (t Result))
133 , HTable (GColumnsADT t)
109 , HTable (GColumnsADT t)
134− , G.GTableADT (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (Rep (t (Reify Result))))
110+ , G.GTableADT (TTable Expr) TColumns TFromExprs (Eval (ADTRep t Expr))
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)
111+ , GMap TFromExprs (Rep (Record (t Expr))) ~ Rep (Record (t Result))
138 )
112 )
139 => ADTable t
113 => ADTable t
140
114
@@ -202,4 +176,4 @@ type instance Eval (ADTRep t context) = GRep t context
202
176
203
177
204type GColumnsADT :: K.Rel8able -> K.HTable
178type 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 @@
3{-# language DerivingStrategies #-}
3{-# language DerivingStrategies #-}
4{-# language FlexibleContexts #-}
4{-# language FlexibleContexts #-}
5{-# language FlexibleInstances #-}
5{-# language FlexibleInstances #-}
6+{-# language LambdaCase #-}
6{-# language MultiParamTypeClasses #-}
7{-# language MultiParamTypeClasses #-}
7{-# language NamedFieldPuns #-}
8{-# language NamedFieldPuns #-}
8{-# language ScopedTypeVariables #-}
9{-# language ScopedTypeVariables #-}
@@ -23,11 +24,9 @@ module Rel8.Table.Either
23where
24where
24
25
25-- base
26-- base
26−import Control.Category ( id )
27import Data.Bifunctor ( Bifunctor, bimap )
27import Data.Bifunctor ( Bifunctor, bimap )
28import Data.Kind ( Type )
28import Data.Kind ( Type )
29−import Data.Type.Equality ( apply )
30−import Prelude hiding ( id, undefined )
29+import Prelude hiding ( undefined )
31
30
32-- comonad
31-- comonad
33import Control.Comonad ( extract )
32import Control.Comonad ( extract )
@@ -38,7 +37,6 @@ import Rel8.Expr ( Col( E ), Expr )
38import Rel8.Expr.Aggregate ( groupByExpr )
37import Rel8.Expr.Aggregate ( groupByExpr )
39import Rel8.Expr.Serialize ( litExpr )
38import Rel8.Expr.Serialize ( litExpr )
40import Rel8.Kind.Context ( Reifiable )
39import Rel8.Kind.Context ( Reifiable )
41−import Rel8.Schema.Context.Abstract ( Abstract )
42import Rel8.Schema.Context.Nullify ( Nullifiable )
40import Rel8.Schema.Context.Nullify ( Nullifiable )
43import Rel8.Schema.Dict ( Dict( Dict ) )
41import Rel8.Schema.Dict ( Dict( Dict ) )
44import Rel8.Schema.HTable.Either ( HEitherTable(..) )
42import Rel8.Schema.HTable.Either ( HEitherTable(..) )
@@ -46,17 +44,18 @@ import Rel8.Schema.HTable.Identity ( HIdentity(..) )
46import Rel8.Schema.HTable.Label ( hlabel, hunlabel )
44import Rel8.Schema.HTable.Label ( hlabel, hunlabel )
47import qualified Rel8.Schema.Kind as K
45import qualified Rel8.Schema.Kind as K
48import Rel8.Schema.Name ( Col( N ), Name )
46import Rel8.Schema.Name ( Col( N ), Name )
47+import Rel8.Schema.Result ( Col( R ) )
49import Rel8.Schema.Spec ( Spec( Spec ) )
48import Rel8.Schema.Spec ( Spec( Spec ) )
50import Rel8.Table
49import Rel8.Table
51 ( Table, Columns, Context, fromColumns, toColumns
50 ( Table, Columns, Context, fromColumns, toColumns
52− , reify, unreify, coherence, congruence
51+ , FromExprs, fromResult, toResult
53 )
52 )
54import Rel8.Table.Bool ( bool )
53import Rel8.Table.Bool ( bool )
55import Rel8.Table.Eq ( EqTable, eqTable )
54import Rel8.Table.Eq ( EqTable, eqTable )
56import Rel8.Table.Nullify ( Nullify, aggregateNullify, guard )
55import Rel8.Table.Nullify ( Nullify, aggregateNullify, guard )
57import Rel8.Table.Ord ( OrdTable, ordTable )
56import Rel8.Table.Ord ( OrdTable, ordTable )
58import Rel8.Table.Recontextualize ( Recontextualize )
57import Rel8.Table.Recontextualize ( Recontextualize )
59−import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
58+import Rel8.Table.Serialize ( ToExprs )
60import Rel8.Table.Undefined ( undefined )
59import Rel8.Table.Undefined ( undefined )
61import Rel8.Type.Tag ( EitherTag( IsLeft, IsRight ), isLeft, isRight )
60import Rel8.Type.Tag ( EitherTag( IsLeft, IsRight ), isLeft, isRight )
62
61
@@ -112,12 +111,13 @@ instance (context ~ Expr, Table Expr a, Table Expr b) =>
112
111
113instance
112instance
114 ( Table context a, Table context b
113 ( Table context a, Table context b
115− , Reifiable context, Abstract context, context ~ context'
114+ , Reifiable context, context ~ context'
116 )
115 )
117 => Table context' (EitherTable context a b)
116 => Table context' (EitherTable context a b)
118 where
117 where
119 type Columns (EitherTable context a b) = HEitherTable (Columns a) (Columns b)
118 type Columns (EitherTable context a b) = HEitherTable (Columns a) (Columns b)
120 type Context (EitherTable context a b) = Context a
119 type Context (EitherTable context a b) = Context a
120+ type FromExprs (EitherTable context a b) = Either (FromExprs a) (FromExprs b)
121
121
122 toColumns EitherTable {tag, left, right} = HEitherTable
122 toColumns EitherTable {tag, left, right} = HEitherTable
123 { htag = hlabel $ HType tag
123 { htag = hlabel $ HType tag
@@ -131,28 +131,29 @@ instance
131 , right = fromColumns $ hunlabel hright
131 , right = fromColumns $ hunlabel hright
132 }
132 }
133
133
134− reify proof EitherTable {tag, left, right} = EitherTable
134+ toResult = \case
135− { tag
135+ Left table -> HEitherTable
136− , left = reify proof left
136+ { htag = hlabel (HType (R IsLeft))
137− , right = reify proof right
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))
138− }
144+ }
139−
145+
140− unreify proof EitherTable {tag, left, right} = EitherTable
146+ fromResult HEitherTable {htag, hleft, hright} = case hunlabel htag of
141− { tag
147+ HType (R tag) -> case tag of
142− , left = unreify proof left
148+ IsLeft -> maybe err Left $ fromResult @_ @(Nullify context a) (hunlabel hleft)
143− , right = unreify proof right
149+ IsRight -> maybe err Right $ fromResult @_ @(Nullify context b) (hunlabel hright)
144− }
150+ where
145−
151+ err = error "Either.fromColumns: mismatch between tag and data"
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
151
152
152
153
153instance
154instance
154− ( Reifiable from, Abstract from, from ~ from'
155+ ( Reifiable from, from ~ from'
155− , Reifiable to, Abstract to, to ~ to'
156+ , Reifiable to, to ~ to'
156 , Recontextualize from to a1 b1
157 , Recontextualize from to a1 b1
157 , Recontextualize from to a2 b2
158 , Recontextualize from to a2 b2
158 )
159 )
@@ -179,19 +180,8 @@ instance (OrdTable a, OrdTable b, context ~ Expr) =>
179 }
180 }
180
181
181
182
182−type instance FromExprs (EitherTable _context a b) =
183− Either (FromExprs a) (FromExprs b)
184−
185−
186instance (ToExprs exprs1 a, ToExprs exprs2 b, x ~ EitherTable Expr exprs1 exprs2) =>
183instance (ToExprs exprs1 a, ToExprs exprs2 b, x ~ EitherTable Expr exprs1 exprs2) =>
187 ToExprs x (Either a b)
184 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)
195
185
196
186
197-- | Test if an 'EitherTable' is a 'leftTable'.
187-- | Test if an 'EitherTable' is a 'leftTable'.
src/Rel8/Table/Eq.hs+6−12
@@ -33,11 +33,7 @@ import Rel8.Expr.Bool ( (||.), (&&.) )
33import Rel8.Expr.Eq ( (==.), (/=.) )
33import Rel8.Expr.Eq ( (==.), (/=.) )
34import Rel8.FCF ( Eval, Exp )
34import Rel8.FCF ( Eval, Exp )
35import Rel8.Generic.Record ( Record )
35import Rel8.Generic.Record ( Record )
36−import Rel8.Generic.Table
36+import Rel8.Generic.Table.Record ( GTable, GColumns, gtable )
37− ( GGTable, GGColumns, ggtable
38− , GAlgebra
39− )
40−import Rel8.Kind.Algebra ( KnownAlgebra )
41import Rel8.Schema.Dict ( Dict( Dict ) )
37import Rel8.Schema.Dict ( Dict( Dict ) )
42import Rel8.Schema.HTable
38import Rel8.Schema.HTable
43 ( HTable, HConstrainTable
39 ( HTable, HConstrainTable
@@ -46,7 +42,7 @@ import Rel8.Schema.HTable
46import Rel8.Schema.HTable.Identity ( HIdentity( HType ) )
42import Rel8.Schema.HTable.Identity ( HIdentity( HType ) )
47import Rel8.Schema.Null ( Sql )
43import Rel8.Schema.Null ( Sql )
48import Rel8.Schema.Spec.Constrain ( ConstrainSpec )
44import Rel8.Schema.Spec.Constrain ( ConstrainSpec )
49−import Rel8.Table ( Table, Columns, toColumns, TColumns )
45+import Rel8.Table ( Table, Columns, toColumns, TColumns, TFromExprs )
50import Rel8.Type.Eq ( DBEq )
46import Rel8.Type.Eq ( DBEq )
51
47
52
48
@@ -58,19 +54,17 @@ class Table Expr a => EqTable a where
58 eqTable :: Columns a (Dict (ConstrainSpec (Sql DBEq)))
54 eqTable :: Columns a (Dict (ConstrainSpec (Sql DBEq)))
59
55
60 default eqTable ::
56 default eqTable ::
61− ( KnownAlgebra (GAlgebra (Rep (Record a)))
62− , Eval (GGTable (GAlgebra (Rep (Record a))) TEqTable TColumns (Dict (ConstrainSpec (Sql DBEq))) (Rep (Record a)))
57+ ( GTable TEqTable TColumns TFromExprs (Rep (Record a))
63− , Columns a ~ Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))
58+ , Columns a ~ GColumns TColumns (Rep (Record a))
64 )
59 )
65 => Columns a (Dict (ConstrainSpec (Sql DBEq)))
60 => Columns a (Dict (ConstrainSpec (Sql DBEq)))
66 eqTable =
61 eqTable =
67− ggtable
62+ gtable
68− @(GAlgebra (Rep (Record a)))
69 @TEqTable
63 @TEqTable
70 @TColumns
64 @TColumns
65+ @TFromExprs
71 @(Rep (Record a))
66 @(Rep (Record a))
72 table
67 table
73− (\_ Dict -> Dict)
74 where
68 where
75 table (_ :: proxy x) = eqTable @x
69 table (_ :: proxy x) = eqTable @x
76
70
src/Rel8/Table/HKD.hs+64−106
@@ -13,7 +13,7 @@
13
13
14module Rel8.Table.HKD
14module Rel8.Table.HKD
15 ( HKD( HKD )
15 ( HKD( HKD )
16− , HKDable, fromHKD, toHKD, HKDT(..)
16+ , HKDable
17 , BuildableHKD
17 , BuildableHKD
18 , BuildHKD, buildHKD
18 , BuildHKD, buildHKD
19 , ConstructableHKD
19 , ConstructableHKD
@@ -27,9 +27,6 @@ where
27
27
28-- base
28-- base
29import Data.Kind ( Constraint, Type )
29import Data.Kind ( Constraint, Type )
30−import Data.Proxy ( Proxy( Proxy ) )
31−import Data.Type.Equality ( (:~:)( Refl ) )
32−import Data.Void ( Void )
33import GHC.Generics ( Generic, Rep, from, to )
30import GHC.Generics ( Generic, Rep, from, to )
34import GHC.TypeLits ( Symbol )
31import GHC.TypeLits ( Symbol )
35import Prelude
32import Prelude
@@ -49,35 +46,34 @@ import Rel8.Generic.Construction
49 , GGName, ggname
46 , GGName, ggname
50 , GGAggregate, ggaggregate
47 , GGAggregate, ggaggregate
51 )
48 )
52−import Rel8.Generic.Map ( GMap, GMappable, gmap, gunmap )
49+import Rel8.Generic.Map ( GMap )
50+import Rel8.Generic.Record
53−import Rel8.Generic.Record ( GRecord, GRecordable, grecord, gunrecord )
51+ ( GRecord, GRecordable, grecord, gunrecord
52+ , Record( Record ), unrecord
53+ )
54import Rel8.Generic.Rel8able
54import Rel8.Generic.Rel8able
55 ( Rel8able
55 ( Rel8able
56 , GColumns, gfromColumns, gtoColumns
56 , GColumns, gfromColumns, gtoColumns
57− , greify, gunreify
57+ , GFromExprs, gfromResult, gtoResult
58− , TUnreifyContext
59 )
58 )
60import Rel8.Generic.Table
59import Rel8.Generic.Table
61− ( GGTable, GGColumns, GGContext, ggfromColumns, ggtoColumns
60+ ( GGTable, GGColumns, GAlgebra, ggfromResult, ggtoResult
62− , GAlgebra
63 )
61 )
62+import Rel8.Generic.Table.Record ( GTable, GContext )
63+import qualified Rel8.Generic.Table.Record as G
64import Rel8.Schema.Context ( Col )
64import Rel8.Schema.Context ( Col )
65import qualified Rel8.Schema.Kind as K
65import qualified Rel8.Schema.Kind as K
66import Rel8.Schema.HTable ( HTable )
66import Rel8.Schema.HTable ( HTable )
67import Rel8.Schema.Name ( Name )
67import Rel8.Schema.Name ( Name )
68−import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify, notReify )
69−import Rel8.Schema.Result ( Result )
70import Rel8.Table
68import Rel8.Table
71− ( Table, Columns, Context, fromColumns, toColumns
69+ ( Table, fromColumns, toColumns, fromResult, toResult
72− , Unreify, reify, unreify, coherence, congruence
73− , TTable, TColumns, TUnreify
70+ , TTable, TColumns, TContext, TFromExprs
74 )
71 )
75−import Rel8.Table.Serialize ( ToExprs, fromResult, toResult )
76
72
77
73
78type GColumnsHKD :: Type -> K.HTable
74type GColumnsHKD :: Type -> K.HTable
79type GColumnsHKD a =
75type 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))))
81
77
82
78
83type HKD :: Type -> K.Rel8able
79type HKD :: Type -> K.Rel8able
@@ -86,128 +82,90 @@ newtype HKD a f = HKD (GColumnsHKD a (Col f))
86
82
87instance HKDable a => Rel8able (HKD a) where
83instance HKDable a => Rel8able (HKD a) where
88 type GColumns (HKD a) = GColumnsHKD a
84 type GColumns (HKD a) = GColumnsHKD a
85+ type GFromExprs (HKD a) = a
89
86
90− gfromColumns = HKD
87+ gfromColumns _ = HKD
91− gtoColumns (HKD a) = a
88+ gtoColumns _ (HKD a) = a
92
89
93− greify (HKD a) = HKD (hreify a)
90+ gfromResult =
94− gunreify (HKD a) = HKD (hunreify a)
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
95
111
96
112
97instance
113instance
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))))
114+ ( GTable (TTable f) TColumns TFromExprs (GRecord (GMap (TColumn f) (Rep a)))
101− , Eval (GGColumns (GAlgebra (Rep a)) TColumns (GRecord (GMap (TColumn (Reify f)) (Rep a)))) ~ GColumnsHKD a
115+ , G.GColumns TColumns (GRecord (GMap (TColumn f) (Rep a))) ~ GColumnsHKD a
102− , Eval (GGContext (GAlgebra (Rep a)) TUnreifyContext (GRecord (GMap (TColumn (Reify f)) (Rep a)))) ~ f
116+ , GContext TContext (GRecord (GMap (TColumn f) (Rep a))) ~ f
103− , GRecordable (GMap (TColumn (Reify f)) (Rep a))
117+ , GRecordable (GMap (TColumn 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)
106 )
118 )
107 => Generic (HKD a f)
119 => Generic (HKD a f)
108 where
120 where
109 type Rep (HKD a f) = GMap (TColumn f) (Rep a)
121 type Rep (HKD a f) = GMap (TColumn f) (Rep a)
110
122
111 from =
123 from =
112− gmap @(TTable (Reify f)) (Proxy @TUnreify) (unreify Refl) .
113− gunrecord @(GMap (TColumn (Reify f)) (Rep a)) .
124+ gunrecord @(GMap (TColumn f) (Rep a)) .
114− ggfromColumns
125+ G.gfromColumns
115− @(GAlgebra (Rep a))
116− @(TTable (Reify f))
126+ @(TTable f)
117 @TColumns
127 @TColumns
118− (\(Reify a) -> a)
128+ @TFromExprs
119− Reify
120 fromColumns .
129 fromColumns .
121− hreify .
122 (\(HKD a) -> a)
130 (\(HKD a) -> a)
123
131
124 to =
132 to =
125 HKD .
133 HKD .
126− hunreify .
134+ G.gtoColumns
127− ggtoColumns
128− @(GAlgebra (Rep a))
129− @(TTable (Reify f))
135+ @(TTable f)
130 @TColumns
136 @TColumns
131− (\(Reify a) -> a)
137+ @TFromExprs
132− Reify
133 toColumns .
138 toColumns .
134− grecord @(GMap (TColumn (Reify f)) (Rep a)) .
139+ grecord @(GMap (TColumn 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_
183
140
184
141
142+type HKDable :: Type -> Constraint
185class
143class
186− ( Generic a
144+ ( Generic (Record a)
187 , HTable (GColumns (HKD a))
145 , HTable (GColumns (HKD a))
188 , KnownAlgebra (GAlgebra (Rep a))
146 , KnownAlgebra (GAlgebra (Rep a))
189− , Eval (GGTable (GAlgebra (Rep a)) (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
147+ , Eval (GGTable (GAlgebra (Rep a)) (TTable Expr) TColumns TFromExprs (Eval (HKDRep a Expr)))
190− , Eval (GGContext (GAlgebra (Rep a)) TUnreifyContext (GRecord (GMap (TColumn (Reify Result)) (Rep a)))) ~ Result
148+ , GMap TFromExprs (GRecord (GMap (TColumn Expr) (Rep a))) ~ Rep (Record a)
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)
195 )
149 )
196 => HKDable a
150 => HKDable a
197instance
151instance
198− ( Generic a
152+ ( Generic (Record a)
199 , HTable (GColumns (HKD a))
153 , HTable (GColumns (HKD a))
200 , KnownAlgebra (GAlgebra (Rep a))
154 , KnownAlgebra (GAlgebra (Rep a))
201− , Eval (GGTable (GAlgebra (Rep a)) (TTable (Reify Result)) TColumns (Col (Reify Result)) (GRecord (GMap (TColumn (Reify Result)) (Rep a))))
155+ , Eval (GGTable (GAlgebra (Rep a)) (TTable Expr) TColumns TFromExprs (Eval (HKDRep a Expr)))
202− , Eval (GGContext (GAlgebra (Rep a)) TUnreifyContext (GRecord (GMap (TColumn (Reify Result)) (Rep a)))) ~ Result
156+ , GMap TFromExprs (GRecord (GMap (TColumn Expr) (Rep a))) ~ Rep (Record a)
203− , GRecordable (GMap (TColumn (Reify Result)) (Rep a))
204− , GMappable Top (Rep a)
205− , GMappable (TTable (Reify Result)) (GMap (TColumn (Reify Result)) (Rep a))
206− , GMap TUnreify (GMap (TColumn (Reify Result)) (Rep a)) ~ GMap (TColumn Result) (Rep a)
207 )
157 )
208 => HKDable a
158 => HKDable a
209
159
210
160
161+class Top_
162+instance Top_
163+
164+
165+data Top :: Type -> Exp Constraint
166+type instance Eval (Top _) = Top_
167+
168+
211type BuildableHKD :: Type -> Symbol -> Constraint
169type BuildableHKD :: Type -> Symbol -> Constraint
212class GGBuildable (GAlgebra (Rep a)) name (HKDRep a) => BuildableHKD a name
170class GGBuildable (GAlgebra (Rep a)) name (HKDRep a) => BuildableHKD a name
213instance GGBuildable (GAlgebra (Rep a)) name (HKDRep a) => BuildableHKD a name
171instance 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
16where
16where
17
17
18-- base
18-- base
19−import Control.Category ( id )
20import Data.Functor.Identity ( Identity( Identity ) )
19import Data.Functor.Identity ( Identity( Identity ) )
21import Data.Kind ( Type )
20import Data.Kind ( Type )
22−import Data.Type.Equality ( (:~:)( Refl ), apply )
23−import Prelude hiding ( id )
21+import Prelude
24
22
25-- rel8
23-- rel8
26import Rel8.Expr ( Expr, Col( E, unE ) )
24import Rel8.Expr ( Expr, Col( E, unE ) )
27import Rel8.Expr.Array ( sappend, sempty, slistOf )
25import Rel8.Expr.Array ( sappend, sempty, slistOf )
28−import Rel8.Schema.Context.Abstract ( Abstract, exclusivity, virtual )
29import Rel8.Schema.Dict ( Dict( Dict ) )
26import Rel8.Schema.Dict ( Dict( Dict ) )
30import Rel8.Schema.HTable.List ( HListTable )
27import Rel8.Schema.HTable.List ( HListTable )
31−import Rel8.Schema.HTable.Vectorize ( happend, hempty, hvectorize )
28+import Rel8.Schema.HTable.Vectorize ( happend, hempty, hvectorize, hunvectorize )
32import qualified Rel8.Schema.Kind as K
29import qualified Rel8.Schema.Kind as K
33import Rel8.Schema.Name ( Col( N ), Name( Name ) )
30import Rel8.Schema.Name ( Col( N ), Name( Name ) )
34import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
31import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
32+import Rel8.Schema.Result ( vectorizer, unvectorizer )
35import Rel8.Schema.Spec ( SSpec(..) )
33import Rel8.Schema.Spec ( SSpec(..) )
36−import Rel8.Schema.Reify ( hreify, hunreify )
37import Rel8.Table
34import Rel8.Table
38 ( Table, Context, Columns, fromColumns, toColumns
35 ( Table, Context, Columns, fromColumns, toColumns
39− , reify, unreify, coherence, congruence
36+ , FromExprs, fromResult, toResult
40 )
37 )
41import Rel8.Table.Alternative
38import Rel8.Table.Alternative
42 ( AltTable, (<|>:)
39 ( AltTable, (<|>:)
@@ -45,7 +42,7 @@ import Rel8.Table.Alternative
45import Rel8.Table.Eq ( EqTable, eqTable )
42import Rel8.Table.Eq ( EqTable, eqTable )
46import Rel8.Table.Ord ( OrdTable, ordTable )
43import Rel8.Table.Ord ( OrdTable, ordTable )
47import Rel8.Table.Recontextualize ( Recontextualize )
44import Rel8.Table.Recontextualize ( Recontextualize )
48−import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
45+import Rel8.Table.Serialize ( ToExprs )
49
46
50
47
51-- | A @ListTable@ value contains zero or more instances of @a@. You construct
48-- | A @ListTable@ value contains zero or more instances of @a@. You construct
@@ -55,39 +52,21 @@ newtype ListTable context a =
55 ListTable (HListTable (Columns a) (Col (Context a)))
52 ListTable (HListTable (Columns a) (Col (Context a)))
56
53
57
54
58−instance (Table context a, Abstract context, context ~ context') =>
55+instance (Table context a, context ~ context') =>
59 Table context' (ListTable context a)
56 Table context' (ListTable context a)
60 where
57 where
61 type Columns (ListTable context a) = HListTable (Columns a)
58 type Columns (ListTable context a) = HListTable (Columns a)
62 type Context (ListTable context a) = Context a
59 type Context (ListTable context a) = Context a
60+ type FromExprs (ListTable context a) = [FromExprs a]
63
61
64 fromColumns = ListTable
62 fromColumns = ListTable
65 toColumns (ListTable a) = a
63 toColumns (ListTable a) = a
64+ fromResult = fmap (fromResult @_ @a) . hunvectorize unvectorizer
65+ toResult = hvectorize vectorizer . fmap (toResult @_ @a)
66
66
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
73
67
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
68+instance (Recontextualize from to a b, from ~ from', to ~ to') =>
87− , Abstract from, from ~ from'
88− , Abstract to, to ~ to'
89− )
90− => Recontextualize from to (ListTable from' a) (ListTable to' b)
69+ Recontextualize from to (ListTable from' a) (ListTable to' b)
91
70
92
71
93instance (EqTable a, context ~ Expr) => EqTable (ListTable context a) where
72instance (EqTable a, context ~ Expr) => EqTable (ListTable context a) where
@@ -108,14 +87,8 @@ instance (OrdTable a, context ~ Expr) => OrdTable (ListTable context a) where
108 (Identity (ordTable @a))
87 (Identity (ordTable @a))
109
88
110
89
111−type instance FromExprs (ListTable _context a) = [FromExprs a]
112−
113−
114instance (ToExprs exprs a, context ~ Expr) =>
90instance (ToExprs exprs a, context ~ Expr) =>
115 ToExprs (ListTable context exprs) [a]
91 ToExprs (ListTable context exprs) [a]
116− where
117− fromResult = fmap (fromResult @exprs) . fromColumns
118− toResult = toColumns . fmap (toResult @exprs)
119
92
120
93
121instance context ~ Expr => AltTable (ListTable context) where
94instance context ~ Expr => AltTable (ListTable context) where
src/Rel8/Table/Maybe.hs+22−25
@@ -22,11 +22,10 @@ module Rel8.Table.Maybe
22where
22where
23
23
24-- base
24-- base
25−import Control.Category ( id )
25+import Data.Functor ( ($>) )
26import Data.Kind ( Type )
26import Data.Kind ( Type )
27−import Data.Maybe ( isJust )
27+import Data.Maybe ( fromMaybe, isJust )
28−import Data.Type.Equality ( apply )
29−import Prelude hiding ( id, null, undefined )
28+import Prelude hiding ( null, undefined )
30
29
31-- comonad
30-- comonad
32import Control.Comonad ( extract )
31import Control.Comonad ( extract )
@@ -38,7 +37,6 @@ import Rel8.Expr.Aggregate ( groupByExpr )
38import Rel8.Expr.Bool ( boolExpr )
37import Rel8.Expr.Bool ( boolExpr )
39import Rel8.Expr.Null ( isNull, isNonNull, null, nullify )
38import Rel8.Expr.Null ( isNull, isNonNull, null, nullify )
40import Rel8.Kind.Context ( Reifiable )
39import Rel8.Kind.Context ( Reifiable )
41−import Rel8.Schema.Context.Abstract ( Abstract )
42import Rel8.Schema.Dict ( Dict( Dict ) )
40import Rel8.Schema.Dict ( Dict( Dict ) )
43import qualified Rel8.Schema.Kind as K
41import qualified Rel8.Schema.Kind as K
44import Rel8.Schema.HTable.Identity ( HIdentity(..) )
42import Rel8.Schema.HTable.Identity ( HIdentity(..) )
@@ -47,10 +45,11 @@ import Rel8.Schema.HTable.Maybe ( HMaybeTable(..) )
47import Rel8.Schema.Name ( Col( N ), Name )
45import Rel8.Schema.Name ( Col( N ), Name )
48import Rel8.Schema.Null ( Nullity( Null, NotNull ), Sql, nullable )
46import Rel8.Schema.Null ( Nullity( Null, NotNull ), Sql, nullable )
49import qualified Rel8.Schema.Null as N
47import qualified Rel8.Schema.Null as N
48+import Rel8.Schema.Result ( Col( R ) )
50import Rel8.Schema.Spec ( Spec( Spec ) )
49import Rel8.Schema.Spec ( Spec( Spec ) )
51import Rel8.Table
50import Rel8.Table
52 ( Table, Columns, Context, fromColumns, toColumns
51 ( Table, Columns, Context, fromColumns, toColumns
53− , coherence, congruence, reify, unreify
52+ , FromExprs, fromResult, toResult
54 )
53 )
55import Rel8.Table.Alternative
54import Rel8.Table.Alternative
56 ( AltTable, (<|>:)
55 ( AltTable, (<|>:)
@@ -61,10 +60,10 @@ import Rel8.Table.Eq ( EqTable, eqTable )
61import Rel8.Table.Ord ( OrdTable, ordTable )
60import Rel8.Table.Ord ( OrdTable, ordTable )
62import Rel8.Table.Nullify ( Nullify, aggregateNullify, guard )
61import Rel8.Table.Nullify ( Nullify, aggregateNullify, guard )
63import Rel8.Table.Recontextualize ( Recontextualize )
62import Rel8.Table.Recontextualize ( Recontextualize )
64−import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
63+import Rel8.Table.Serialize ( ToExprs )
65import Rel8.Table.Undefined ( undefined )
64import Rel8.Table.Undefined ( undefined )
66import Rel8.Type ( DBType )
65import Rel8.Type ( DBType )
67−import Rel8.Type.Tag ( MaybeTag )
66+import Rel8.Type.Tag ( MaybeTag( IsJust ) )
68
67
69-- semigroupoids
68-- semigroupoids
70import Data.Functor.Apply ( Apply, (<.>) )
69import Data.Functor.Apply ( Apply, (<.>) )
@@ -129,14 +128,12 @@ instance (context ~ Expr, Table Expr a, Semigroup a) =>
129 mempty = nothingTable
128 mempty = nothingTable
130
129
131
130
132−instance
133− ( Table context a
134− , Reifiable context, Abstract context, context ~ context'
131+instance (Table context a, Reifiable context, context ~ context') =>
135− )
136− => Table context' (MaybeTable context a)
132+ Table context' (MaybeTable context a)
137 where
133 where
138 type Columns (MaybeTable context a) = HMaybeTable (Columns a)
134 type Columns (MaybeTable context a) = HMaybeTable (Columns a)
139 type Context (MaybeTable context a) = Context a
135 type Context (MaybeTable context a) = Context a
136+ type FromExprs (MaybeTable context a) = Maybe (FromExprs a)
140
137
141 toColumns MaybeTable {tag, just} = HMaybeTable
138 toColumns MaybeTable {tag, just} = HMaybeTable
142 { htag = hlabel $ HIdentity tag
139 { htag = hlabel $ HIdentity tag
@@ -148,16 +145,22 @@ instance
148 , just = fromColumns $ hunlabel hjust
145 , just = fromColumns $ hunlabel hjust
149 }
146 }
150
147
151− reify proof (MaybeTable tag a) = MaybeTable tag (reify proof a)
148+ toResult ma = HMaybeTable
152− unreify proof (MaybeTable tag a) = MaybeTable tag (unreify proof a)
149+ { htag = hlabel (HIdentity (R (IsJust <$ ma)))
153− coherence = coherence @context @a
150+ , hjust = hlabel (toResult @_ @(Nullify context a) ma)
154− congruence proof abstract = id `apply` congruence @context @a proof abstract
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"
155
158
156
159
157instance
160instance
158 ( Recontextualize from to a b
161 ( Recontextualize from to a b
159− , Reifiable from, Abstract from, from ~ from'
162+ , Reifiable from, from ~ from'
160− , Reifiable to, Abstract to, to ~ to'
163+ , Reifiable to, to ~ to'
161 )
164 )
162 => Recontextualize from to (MaybeTable from' a) (MaybeTable to' b)
165 => Recontextualize from to (MaybeTable from' a) (MaybeTable to' b)
163
166
@@ -176,14 +179,8 @@ instance (OrdTable a, context ~ Expr) => OrdTable (MaybeTable context a) where
176 }
179 }
177
180
178
181
179−type instance FromExprs (MaybeTable _context a) = Maybe (FromExprs a)
180−
181−
182instance (ToExprs exprs a, context ~ Expr) =>
182instance (ToExprs exprs a, context ~ Expr) =>
183 ToExprs (MaybeTable context exprs) (Maybe a)
183 ToExprs (MaybeTable context exprs) (Maybe a)
184− where
185− fromResult = fmap (fromResult @exprs) . fromColumns
186− toResult = toColumns . fmap (toResult @exprs)
187
184
188
185
189-- | Check if a @MaybeTable@ is absent of any row. Like 'Data.Maybe.isNothing'.
186-- | 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
16where
16where
17
17
18-- base
18-- base
19−import Control.Category ( id )
20import Data.Functor.Identity ( Identity( Identity ) )
19import Data.Functor.Identity ( Identity( Identity ) )
21import Data.Kind ( Type )
20import Data.Kind ( Type )
22import Data.List.NonEmpty ( NonEmpty )
21import Data.List.NonEmpty ( NonEmpty )
23−import Data.Type.Equality ( (:~:)( Refl ), apply )
24import Prelude hiding ( id )
22import Prelude hiding ( id )
25
23
26-- rel8
24-- rel8
27import Rel8.Expr ( Expr, Col( E, unE ) )
25import Rel8.Expr ( Expr, Col( E, unE ) )
28import Rel8.Expr.Array ( sappend1, snonEmptyOf )
26import Rel8.Expr.Array ( sappend1, snonEmptyOf )
29−import Rel8.Schema.Context.Abstract ( Abstract, exclusivity, virtual )
30import Rel8.Schema.Dict ( Dict( Dict ) )
27import Rel8.Schema.Dict ( Dict( Dict ) )
31import Rel8.Schema.HTable.NonEmpty ( HNonEmptyTable )
28import Rel8.Schema.HTable.NonEmpty ( HNonEmptyTable )
32−import Rel8.Schema.HTable.Vectorize ( happend, hvectorize )
29+import Rel8.Schema.HTable.Vectorize ( happend, hvectorize, hunvectorize )
33import qualified Rel8.Schema.Kind as K
30import qualified Rel8.Schema.Kind as K
34import Rel8.Schema.Name ( Col( N ), Name( Name ) )
31import Rel8.Schema.Name ( Col( N ), Name( Name ) )
35import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
32import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
36−import Rel8.Schema.Reify ( hreify, hunreify )
33+import Rel8.Schema.Result ( vectorizer, unvectorizer )
37import Rel8.Schema.Spec ( SSpec(..) )
34import Rel8.Schema.Spec ( SSpec(..) )
38import Rel8.Table
35import Rel8.Table
39 ( Table, Context, Columns, fromColumns, toColumns
36 ( Table, Context, Columns, fromColumns, toColumns
40− , reify, unreify, coherence, congruence
37+ , FromExprs, fromResult, toResult
41 )
38 )
42import Rel8.Table.Alternative ( AltTable, (<|>:) )
39import Rel8.Table.Alternative ( AltTable, (<|>:) )
43import Rel8.Table.Eq ( EqTable, eqTable )
40import Rel8.Table.Eq ( EqTable, eqTable )
44import Rel8.Table.Ord ( OrdTable, ordTable )
41import Rel8.Table.Ord ( OrdTable, ordTable )
45import Rel8.Table.Recontextualize ( Recontextualize )
42import Rel8.Table.Recontextualize ( Recontextualize )
46−import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
43+import Rel8.Table.Serialize ( ToExprs )
47
44
48
45
49-- | A @NonEmptyTable@ value contains one or more instances of @a@. You
46-- | A @NonEmptyTable@ value contains one or more instances of @a@. You
@@ -53,39 +50,21 @@ newtype NonEmptyTable context a =
53 NonEmptyTable (HNonEmptyTable (Columns a) (Col (Context a)))
50 NonEmptyTable (HNonEmptyTable (Columns a) (Col (Context a)))
54
51
55
52
56−instance (Table context a, Abstract context, context ~ context') =>
53+instance (Table context a, context ~ context') =>
57 Table context' (NonEmptyTable context a)
54 Table context' (NonEmptyTable context a)
58 where
55 where
59 type Columns (NonEmptyTable context a) = HNonEmptyTable (Columns a)
56 type Columns (NonEmptyTable context a) = HNonEmptyTable (Columns a)
60 type Context (NonEmptyTable context a) = Context a
57 type Context (NonEmptyTable context a) = Context a
58+ type FromExprs (NonEmptyTable context a) = NonEmpty (FromExprs a)
61
59
62 fromColumns = NonEmptyTable
60 fromColumns = NonEmptyTable
63 toColumns (NonEmptyTable a) = a
61 toColumns (NonEmptyTable a) = a
62+ fromResult = fmap (fromResult @_ @a) . hunvectorize unvectorizer
63+ toResult = hvectorize vectorizer . fmap (toResult @_ @a)
64
64
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
71
65
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
66+instance (Recontextualize from to a b, from ~ from', to ~ to') =>
85− , Abstract from, from ~ from'
86− , Abstract to, to ~ to'
87− )
88− => Recontextualize from to (NonEmptyTable from' a) (NonEmptyTable to' b)
67+ Recontextualize from to (NonEmptyTable from' a) (NonEmptyTable to' b)
89
68
90
69
91instance (EqTable a, context ~ Expr) =>
70instance (EqTable a, context ~ Expr) =>
@@ -110,14 +89,8 @@ instance (OrdTable a, context ~ Expr) =>
110 (Identity (ordTable @a))
89 (Identity (ordTable @a))
111
90
112
91
113−type instance FromExprs (NonEmptyTable _context a) = NonEmpty (FromExprs a)
114−
115−
116instance (ToExprs exprs a, context ~ Expr) =>
92instance (ToExprs exprs a, context ~ Expr) =>
117 ToExprs (NonEmptyTable context exprs) (NonEmpty a)
93 ToExprs (NonEmptyTable context exprs) (NonEmpty a)
118− where
119− fromResult = fmap (fromResult @exprs) . fromColumns
120− toResult = toColumns . fmap (toResult @exprs)
121
94
122
95
123instance context ~ Expr => AltTable (NonEmptyTable context) where
96instance context ~ Expr => AltTable (NonEmptyTable context) where
src/Rel8/Table/Nullify.hs+15−37
@@ -17,11 +17,9 @@ where
17
17
18-- base
18-- base
19import Control.Applicative ( liftA2 )
19import Control.Applicative ( liftA2 )
20−import Control.Category ( id )
21import Data.Functor.Identity ( runIdentity )
20import Data.Functor.Identity ( runIdentity )
22import Data.Kind ( Type )
21import Data.Kind ( Type )
23−import Data.Type.Equality ( (:~:)( Refl ), apply )
24−import Prelude hiding ( id )
22+import Prelude
25
23
26-- comonad
24-- comonad
27import Control.Comonad ( Comonad, duplicate, extract, ComonadApply, (<@>) )
25import Control.Comonad ( Comonad, duplicate, extract, ComonadApply, (<@>) )
@@ -31,10 +29,9 @@ import Rel8.Aggregate ( Aggregate )
31import Rel8.Expr ( Expr )
29import Rel8.Expr ( Expr )
32import Rel8.Kind.Context ( Reifiable, contextSing )
30import Rel8.Kind.Context ( Reifiable, contextSing )
33import Rel8.Schema.Context ( Col )
31import Rel8.Schema.Context ( Col )
34−import Rel8.Schema.Context.Abstract ( Abstract, exclusivity, virtual )
35import Rel8.Schema.Context.Nullify
32import Rel8.Schema.Context.Nullify
36 ( Nullifiability( NAggregate, NExpr )
33 ( Nullifiability( NAggregate, NExpr )
37− , NonNullifiability( NNReify )
34+ , NonNullifiability
38 , Nullifiable, nullifiability
35 , Nullifiable, nullifiability
39 , nullifiableOrNot, absurd
36 , nullifiableOrNot, absurd
40 , guarder
37 , guarder
@@ -43,13 +40,13 @@ import Rel8.Schema.Context.Nullify
43 )
40 )
44import Rel8.Schema.Dict ( Dict( Dict ) )
41import Rel8.Schema.Dict ( Dict( Dict ) )
45import Rel8.Schema.HTable ( HTable )
42import 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 )
47import qualified Rel8.Schema.Kind as K
44import qualified Rel8.Schema.Kind as K
48−import Rel8.Schema.Reify ( hreify, hunreify )
45+import qualified Rel8.Schema.Result as R
49import Rel8.Schema.Spec ( Spec( Spec ) )
46import Rel8.Schema.Spec ( Spec( Spec ) )
50import Rel8.Table
47import Rel8.Table
51 ( Table, Columns, Context, toColumns, fromColumns
48 ( Table, Columns, Context, toColumns, fromColumns
52− , reify, unreify, coherence, congruence
49+ , FromExprs, fromResult, toResult
53 )
50 )
54import Rel8.Table.Eq ( EqTable, eqTable )
51import Rel8.Table.Eq ( EqTable, eqTable )
55import Rel8.Table.Ord ( OrdTable, ordTable )
52import Rel8.Table.Ord ( OrdTable, ordTable )
@@ -124,14 +121,12 @@ instance Nullifiable context => ComonadApply (Nullify context) where
124 (<@>) = (<.>)
121 (<@>) = (<.>)
125
122
126
123
127−instance
128− ( Table context a
129− , Reifiable context, Abstract context, context ~ context'
124+instance (Table context a, Reifiable context, context ~ context') =>
130− )
131− => Table context' (Nullify context a)
125+ Table context' (Nullify context a)
132 where
126 where
133 type Columns (Nullify context a) = HNullify (Columns a)
127 type Columns (Nullify context a) = HNullify (Columns a)
134 type Context (Nullify context a) = Context a
128 type Context (Nullify context a) = Context a
129+ type FromExprs (Nullify context a) = Maybe (FromExprs a)
135
130
136 fromColumns = case nullifiableOrNot contextSing of
131 fromColumns = case nullifiableOrNot contextSing of
137 Left notNullifiable -> Fields notNullifiable
132 Left notNullifiable -> Fields notNullifiable
@@ -145,34 +140,17 @@ instance
145 Table nullifiable a -> hnullify (nullifier nullifiable) (toColumns a)
140 Table nullifiable a -> hnullify (nullifier nullifiable) (toColumns a)
146 Fields _ a -> a
141 Fields _ a -> a
147
142
148− reify proof@Refl = \case
143+ fromResult = fmap (fromResult @_ @a) . hunnullify R.unnullifier
149− Table nullifiable a -> Table nullifiable (reify proof a)
144+
150− Fields notNullifiable a -> case notNullifiable of
145+ toResult =
151− NNReify (_ :: NonNullifiability ctx) ->
146+ maybe (hnulls (const R.null)) (hnullify R.nullifier) .
152− case coherence @context @a proof abstract of
147+ fmap (toResult @_ @a)
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
170
148
171
149
172instance
150instance
173 ( Recontextualize from to a b
151 ( Recontextualize from to a b
174− , Reifiable from, Abstract from, from ~ from'
152+ , Reifiable from, from ~ from'
175− , Reifiable to, Abstract to, to ~ to'
153+ , Reifiable to, to ~ to'
176 )
154 )
177 => Recontextualize from' to' (Nullify from a) (Nullify to b)
155 => Recontextualize from' to' (Nullify from a) (Nullify to b)
178
156
src/Rel8/Table/Ord.hs+6−12
@@ -31,11 +31,7 @@ import Rel8.Expr.Eq ( (==.) )
31import Rel8.Expr.Ord ( (<.), (>.) )
31import Rel8.Expr.Ord ( (<.), (>.) )
32import Rel8.FCF ( Eval, Exp )
32import Rel8.FCF ( Eval, Exp )
33import Rel8.Generic.Record ( Record )
33import Rel8.Generic.Record ( Record )
34−import Rel8.Generic.Table
34+import Rel8.Generic.Table.Record ( GTable, GColumns, gtable )
35− ( GGTable, GGColumns, ggtable
36− , GAlgebra
37− )
38−import Rel8.Kind.Algebra ( KnownAlgebra )
39import Rel8.Schema.Dict ( Dict( Dict ) )
35import Rel8.Schema.Dict ( Dict( Dict ) )
40import Rel8.Schema.HTable
36import Rel8.Schema.HTable
41 ( HTable, HConstrainTable
37 ( HTable, HConstrainTable
@@ -44,7 +40,7 @@ import Rel8.Schema.HTable
44import Rel8.Schema.HTable.Identity ( HIdentity( HType ) )
40import Rel8.Schema.HTable.Identity ( HIdentity( HType ) )
45import Rel8.Schema.Null (Sql)
41import Rel8.Schema.Null (Sql)
46import Rel8.Schema.Spec.Constrain ( ConstrainSpec )
42import Rel8.Schema.Spec.Constrain ( ConstrainSpec )
47−import Rel8.Table ( Columns, toColumns, TColumns )
43+import Rel8.Table ( Columns, toColumns, TColumns, TFromExprs )
48import Rel8.Table.Bool ( bool )
44import Rel8.Table.Bool ( bool )
49import Rel8.Table.Eq ( EqTable )
45import Rel8.Table.Eq ( EqTable )
50import Rel8.Type.Eq ( DBEq )
46import Rel8.Type.Eq ( DBEq )
@@ -59,19 +55,17 @@ class EqTable a => OrdTable a where
59 ordTable :: Columns a (Dict (ConstrainSpec (Sql DBOrd)))
55 ordTable :: Columns a (Dict (ConstrainSpec (Sql DBOrd)))
60
56
61 default ordTable ::
57 default ordTable ::
62− ( KnownAlgebra (GAlgebra (Rep (Record a)))
63− , Eval (GGTable (GAlgebra (Rep (Record a))) TOrdTable TColumns (Dict (ConstrainSpec (Sql DBOrd))) (Rep (Record a)))
58+ ( GTable TOrdTable TColumns TFromExprs (Rep (Record a))
64− , Columns a ~ Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))
59+ , Columns a ~ GColumns TColumns (Rep (Record a))
65 )
60 )
66 => Columns a (Dict (ConstrainSpec (Sql DBOrd)))
61 => Columns a (Dict (ConstrainSpec (Sql DBOrd)))
67 ordTable =
62 ordTable =
68− ggtable
63+ gtable
69− @(GAlgebra (Rep (Record a)))
70 @TOrdTable
64 @TOrdTable
71 @TColumns
65 @TColumns
66+ @TFromExprs
72 @(Rep (Record a))
67 @(Rep (Record a))
73 table
68 table
74− (\_ Dict -> Dict)
75 where
69 where
76 table (_ :: proxy x) = ordTable @x
70 table (_ :: proxy x) = ordTable @x
77
71
src/Rel8/Table/Recontextualize.hs+1−40
@@ -12,23 +12,15 @@ module Rel8.Table.Recontextualize
12where
12where
13
13
14-- base
14-- base
15−import Data.Functor.Identity ( Identity )
16import Data.Kind ( Constraint, Type )
15import Data.Kind ( Constraint, Type )
17−import Data.List.NonEmpty ( NonEmpty)
16+import Prelude ()
18−import Prelude
19
17
20-- rel8
18-- rel8
21import Rel8.Schema.Context ( Col )
19import Rel8.Schema.Context ( Col )
22import Rel8.Schema.HTable ( HTable )
20import Rel8.Schema.HTable ( HTable )
23import qualified Rel8.Schema.Kind as K
21import qualified Rel8.Schema.Kind as K
24−import Rel8.Schema.Null ( Sql )
25−import Rel8.Schema.Result ( Result )
26import Rel8.Schema.Spec ( KnownSpec )
22import Rel8.Schema.Spec ( KnownSpec )
27import Rel8.Table ( Table, Congruent )
23import Rel8.Table ( Table, Congruent )
28−import Rel8.Type ( DBType )
29−
30−-- these
31−import Data.These ( These)
32
24
33
25
34-- | @Recontextualize from to a b@ is evidence that the types @a@ and @b@ are
26-- | @Recontextualize from to a b@ is evidence that the types @a@ and @b@ are
@@ -49,43 +41,12 @@ class
49 , b from -> a
41 , b from -> a
50
42
51
43
52−instance Sql DBType a => Recontextualize Result Result (Identity a) (Identity a)
53−
54−
55instance KnownSpec spec => Recontextualize from to (Col from spec) (Col to spec)
44instance KnownSpec spec => Recontextualize from to (Col from spec) (Col to spec)
56
45
57
46
58instance HTable t => Recontextualize from to (t (Col from)) (t (Col to))
47instance HTable t => Recontextualize from to (t (Col from)) (t (Col to))
59
48
60
49
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−
89instance
50instance
90 ( Recontextualize from to a1 b1
51 ( Recontextualize from to a1 b1
91 , Recontextualize from to a2 b2
52 , Recontextualize from to a2 b2
src/Rel8/Table/Rel8able.hs+21−71
@@ -1,6 +1,6 @@
1{-# language DataKinds #-}
1{-# language DataKinds #-}
2{-# language FlexibleInstances #-}
2{-# language FlexibleInstances #-}
3−{-# language FunctionalDependencies #-}
3+{-# language MultiParamTypeClasses #-}
4{-# language ScopedTypeVariables #-}
4{-# language ScopedTypeVariables #-}
5{-# language StandaloneKindSignatures #-}
5{-# language StandaloneKindSignatures #-}
6{-# language TypeApplications #-}
6{-# language TypeApplications #-}
@@ -15,71 +15,50 @@ module Rel8.Table.Rel8able
15where
15where
16
16
17-- base
17-- base
18−import Data.Kind ( Constraint, Type )
19−import Data.Type.Equality ( (:~:)( Refl ) )
20−import Prelude
18+import Prelude ()
21
19
22-- rel8
20-- rel8
23import Rel8.Expr ( Expr )
21import Rel8.Expr ( Expr )
24import qualified Rel8.Kind.Algebra as K
22import qualified Rel8.Kind.Algebra as K
25−import Rel8.Kind.Context
26− ( SContext( SReify )
27− , Reifiable, contextSing
28− , sReifiable
29− )
30import Rel8.Generic.Rel8able
23import Rel8.Generic.Rel8able
31 ( Rel8able, Algebra
24 ( Rel8able, Algebra
32 , GColumns, gfromColumns, gtoColumns
25 , GColumns, gfromColumns, gtoColumns
33− , greify, gunreify
26+ , GFromExprs, gfromResult, gtoResult
34 )
27 )
35−import Rel8.Schema.Context ( Col )
28+import Rel8.Schema.Context.Virtual ( Virtual, virtual )
36−import Rel8.Schema.Dict ( Dict( Dict ) )
37import qualified Rel8.Schema.Kind as K
29import qualified Rel8.Schema.Kind as K
38import Rel8.Schema.HTable ( HConstrainTable, hdicts )
30import Rel8.Schema.HTable ( HConstrainTable, hdicts )
39import Rel8.Schema.Null ( Sql )
31import Rel8.Schema.Null ( Sql )
40−import Rel8.Schema.Reify ( hreify, hunreify, UnwrapReify )
41import Rel8.Schema.Result ( Result )
32import Rel8.Schema.Result ( Result )
42import Rel8.Table
33import Rel8.Table
43 ( Table, Columns, Context, Congruent, fromColumns, toColumns
34 ( Table, Columns, Context, Congruent, fromColumns, toColumns
44− , Unreify, reify, unreify, coherence, congruence
35+ , FromExprs, fromResult, toResult
45 )
36 )
46import Rel8.Schema.Spec.Constrain ( ConstrainSpec )
37import Rel8.Schema.Spec.Constrain ( ConstrainSpec )
47−import Rel8.Table.ADT ( ADT( ADT ), ADTable, fromADT, toADT )
38+import Rel8.Table.ADT ( ADT )
48import Rel8.Table.Eq ( EqTable, eqTable )
39import Rel8.Table.Eq ( EqTable, eqTable )
49−import Rel8.Table.HKD ( HKD )
50import Rel8.Table.Ord ( OrdTable, ordTable )
40import Rel8.Table.Ord ( OrdTable, ordTable )
51import Rel8.Table.Recontextualize ( Recontextualize )
41import Rel8.Table.Recontextualize ( Recontextualize )
52−import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
42+import Rel8.Table.Serialize ( ToExprs )
53import Rel8.Type.Eq ( DBEq )
43import Rel8.Type.Eq ( DBEq )
54import Rel8.Type.Ord ( DBOrd )
44import Rel8.Type.Ord ( DBOrd )
55
45
56
46
57−instance (Rel8able t, Reifiable context) =>
47+instance (Rel8able t, Virtual context) => Table context (t context) where
58− Table context (t context)
59− where
60 type Columns (t context) = GColumns t
48 type Columns (t context) = GColumns t
61 type Context (t context) = context
49 type Context (t context) = context
62− type Unreify (t context) = t (UnwrapReify context)
50+ type FromExprs (t context) = GFromExprs t
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
74
51
75− coherence Refl _ = Refl
52+ fromColumns = gfromColumns virtual
76− congruence Refl _ = Refl
53+ toColumns = gtoColumns virtual
54+ fromResult = gfromResult @t
55+ toResult = gtoResult @t
77
56
78
57
79instance
58instance
80 ( Rel8able t
59 ( Rel8able t
81− , Reifiable from
60+ , Virtual from
82− , Reifiable to
61+ , Virtual to
83 , Congruent (t from) (t to)
62 , Congruent (t from) (t to)
84 )
63 )
85 => Recontextualize from to (t from) (t to)
64 => Recontextualize from to (t from) (t to)
@@ -106,44 +85,15 @@ instance
106 ordTable = hdicts @(Columns (t context)) @(ConstrainSpec (Sql DBOrd))
85 ordTable = hdicts @(Columns (t context)) @(ConstrainSpec (Sql DBOrd))
107
86
108
87
109−type instance FromExprs (t Expr) = FromExprs' t
110−
111−
112instance
88instance
89+ ( Rel8able t', t' ~ Choose (Algebra t) t
113− ( x ~ t' Expr
90+ , x ~ t' Expr
114 , result ~ Result
91 , result ~ Result
115− , ToExprs' (Algebra t) t' t
116 )
92 )
117 => ToExprs x (t result)
93 => ToExprs x (t result)
118− where
119− fromResult = fromResult' @(Algebra t) @t'
120− toResult = toResult' @(Algebra t) @t'
121−
122
94
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
128
95
129−
130−type ToExprs' :: K.Algebra -> K.Rel8able -> K.Rel8able -> Constraint
96+type Choose :: K.Algebra -> K.Rel8able -> K.Rel8able
131−class (algebra ~ Algebra t, Rel8able t') =>
97+type family Choose algebra t where
132− ToExprs' algebra t' t | algebra t -> t'
98+ Choose 'K.Sum t = ADT 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
99+ Choose '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
src/Rel8/Table/Serialize.hs+12−105
@@ -1,7 +1,4 @@
1{-# language AllowAmbiguousTypes #-}
1{-# language AllowAmbiguousTypes #-}
2−{-# language DataKinds #-}
3−{-# language DefaultSignatures #-}
4−{-# language DisambiguateRecordFields #-}
5{-# language FlexibleContexts #-}
2{-# language FlexibleContexts #-}
6{-# language FlexibleInstances #-}
3{-# language FlexibleInstances #-}
7{-# language FunctionalDependencies #-}
4{-# language FunctionalDependencies #-}
@@ -10,20 +7,17 @@
10{-# language StandaloneKindSignatures #-}
7{-# language StandaloneKindSignatures #-}
11{-# language TypeApplications #-}
8{-# language TypeApplications #-}
12{-# language TypeFamilies #-}
9{-# language TypeFamilies #-}
13−{-# language TypeOperators #-}
14{-# language UndecidableInstances #-}
10{-# language UndecidableInstances #-}
15
11
16module Rel8.Table.Serialize
12module Rel8.Table.Serialize
17 ( Serializable, lit, parse
13 ( Serializable, lit, parse
18− , ToExprs(..), FromExprs
14+ , ToExprs
19− , TToExprs
20 )
15 )
21where
16where
22
17
23-- base
18-- base
24import Data.Kind ( Constraint, Type )
19import Data.Kind ( Constraint, Type )
25import Data.List.NonEmpty ( NonEmpty )
20import Data.List.NonEmpty ( NonEmpty )
26−import GHC.Generics ( Generic, Rep, from, to )
27import Prelude
21import Prelude
28
22
29-- hasql
23-- hasql
@@ -32,19 +26,11 @@ import qualified Hasql.Decoders as Hasql
32-- rel8
26-- rel8
33import Rel8.Expr ( Expr, Col( E ) )
27import Rel8.Expr ( Expr, Col( E ) )
34import Rel8.Expr.Serialize ( slitExpr, sparseValue )
28import 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 )
42import Rel8.Schema.HTable ( HTable, htabulate, htabulateA, hfield, hspecs )
29import Rel8.Schema.HTable ( HTable, htabulate, htabulateA, hfield, hspecs )
43−import Rel8.Schema.HTable.Identity ( HIdentity( HType ) )
44import Rel8.Schema.Null ( NotNull, Sql )
30import Rel8.Schema.Null ( NotNull, Sql )
45import Rel8.Schema.Result ( Col( R ), Result )
31import Rel8.Schema.Result ( Col( R ), Result )
46import Rel8.Schema.Spec ( SSpec(..), KnownSpec )
32import Rel8.Schema.Spec ( SSpec(..), KnownSpec )
47−import Rel8.Table ( Table, Columns, fromColumns, toColumns, TColumns )
33+import Rel8.Table ( Table, fromColumns, FromExprs, fromResult, toResult )
48import Rel8.Type ( DBType )
34import Rel8.Type ( DBType )
49
35
50-- semigroupoids
36-- semigroupoids
@@ -53,71 +39,21 @@ import Data.Functor.Apply ( WrappedApplicative(..) )
53
39
54-- | @ToExprs exprs a@ is evidence that the types @exprs@ and @a@ describe
40-- | @ToExprs exprs a@ is evidence that the types @exprs@ and @a@ describe
55-- essentially the same type, but @exprs@ is in the 'Expr' context, and @a@ is
41-- essentially the same type, but @exprs@ is in the 'Expr' context, and @a@ is
56−-- in the 'Result' context.
42+-- a normal Haskell type.
57type ToExprs :: Type -> Type -> Constraint
43type ToExprs :: Type -> Type -> Constraint
58−class Table Expr exprs => ToExprs exprs a where
44+class Table Expr exprs => ToExprs exprs a
59− fromResult :: Columns exprs (Col Result) -> a
45+
60− toResult :: a -> Columns exprs (Col Result)
46+
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
47+instance {-# OVERLAPPABLE #-} (Sql DBType a, x ~ Expr a) => ToExprs x a
102− fromResult (HType (R a)) = a
48+
103− toResult = HType . R
49+
104−
105−
106−instance (Sql DBType a, x ~ [a]) => ToExprs (Expr x) [a] where
50+instance (Sql DBType a, x ~ [a]) => ToExprs (Expr x) [a]
107− fromResult (HType (R a)) = a
108− toResult = HType . R
109
51
110
52
111instance (Sql DBType a, NotNull a, x ~ Maybe a) => ToExprs (Expr x) (Maybe a)
53instance (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
115
54
116
55
117instance (Sql DBType a, NotNull a, x ~ NonEmpty a) => ToExprs (Expr x) (NonEmpty a)
56instance (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
121
57
122
58
123instance (ToExprs exprs1 a, ToExprs exprs2 b, x ~ (exprs1, exprs2)) =>
59instance (ToExprs exprs1 a, ToExprs exprs2 b, x ~ (exprs1, exprs2)) =>
@@ -181,39 +117,10 @@ instance
181
117
182instance (HTable t, result ~ Col Result, x ~ t (Col Expr)) =>
118instance (HTable t, result ~ Col Result, x ~ t (Col Expr)) =>
183 ToExprs x (t result)
119 ToExprs x (t result)
184− where
185− fromResult = id
186− toResult = id
187
120
188
121
189instance (KnownSpec spec, x ~ Col Expr spec) =>
122instance (KnownSpec spec, x ~ Col Expr spec) =>
190 ToExprs x (Col Result spec)
123 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)
217
124
218
125
219-- | @Serializable@ witnesses the one-to-one correspondence between the type
126-- | @Serializable@ witnesses the one-to-one correspondence between the type
@@ -228,11 +135,11 @@ instance {-# OVERLAPPING #-} Sql DBType a => Serializable (Expr a) a
228-- | Use @lit@ to turn literal Haskell values into expressions. @lit@ is
135-- | Use @lit@ to turn literal Haskell values into expressions. @lit@ is
229-- capable of lifting single @Expr@s to full tables.
136-- capable of lifting single @Expr@s to full tables.
230lit :: forall exprs a. Serializable exprs a => a -> exprs
137lit :: forall exprs a. Serializable exprs a => a -> exprs
231−lit = fromColumns . litHTable . toResult @exprs
138+lit = fromColumns . litHTable . toResult @_ @exprs
232
139
233
140
234parse :: forall exprs a. Serializable exprs a => Hasql.Row a
141parse :: forall exprs a. Serializable exprs a => Hasql.Row a
235−parse = fromResult @exprs <$> parseHTable
142+parse = fromResult @_ @exprs <$> parseHTable
236
143
237
144
238litHTable :: HTable t => t (Col Result) -> t (Col Expr)
145litHTable :: HTable t => t (Col Result) -> t (Col Expr)
src/Rel8/Table/These.hs+45−36
@@ -26,12 +26,10 @@ module Rel8.Table.These
26where
26where
27
27
28-- base
28-- base
29−import Control.Category ( id )
30import Data.Bifunctor ( Bifunctor, bimap )
29import Data.Bifunctor ( Bifunctor, bimap )
31import Data.Kind ( Type )
30import Data.Kind ( Type )
32import Data.Maybe ( isJust )
31import Data.Maybe ( isJust )
33−import Data.Type.Equality ( apply )
34−import Prelude hiding ( id, undefined )
32+import Prelude hiding ( undefined )
35
33
36-- rel8
34-- rel8
37import Rel8.Aggregate ( Aggregate )
35import Rel8.Aggregate ( Aggregate )
@@ -39,17 +37,17 @@ import Rel8.Expr ( Expr )
39import Rel8.Expr.Bool ( (&&.), not_ )
37import Rel8.Expr.Bool ( (&&.), not_ )
40import Rel8.Expr.Null ( isNonNull )
38import Rel8.Expr.Null ( isNonNull )
41import Rel8.Kind.Context ( Reifiable )
39import Rel8.Kind.Context ( Reifiable )
42−import Rel8.Schema.Context.Abstract ( Abstract )
43import Rel8.Schema.Context.Nullify ( Nullifiable )
40import Rel8.Schema.Context.Nullify ( Nullifiable )
44import Rel8.Schema.Dict ( Dict( Dict ) )
41import Rel8.Schema.Dict ( Dict( Dict ) )
45−import Rel8.Schema.HTable.Label ( hlabel, hunlabel )
42+import Rel8.Schema.HTable.Label ( hlabel, hrelabel, hunlabel )
46import Rel8.Schema.HTable.Identity ( HIdentity(..) )
43import Rel8.Schema.HTable.Identity ( HIdentity(..) )
44+import Rel8.Schema.HTable.Maybe ( HMaybeTable(..) )
47import Rel8.Schema.HTable.These ( HTheseTable(..) )
45import Rel8.Schema.HTable.These ( HTheseTable(..) )
48import qualified Rel8.Schema.Kind as K
46import qualified Rel8.Schema.Kind as K
49import Rel8.Schema.Name ( Name )
47import Rel8.Schema.Name ( Name )
50import Rel8.Table
48import Rel8.Table
51 ( Table, Columns, Context, fromColumns, toColumns
49 ( Table, Columns, Context, fromColumns, toColumns
52− , coherence, congruence, reify, unreify
50+ , FromExprs, fromResult, toResult
53 )
51 )
54import Rel8.Table.Eq ( EqTable, eqTable )
52import Rel8.Table.Eq ( EqTable, eqTable )
55import Rel8.Table.Maybe
53import Rel8.Table.Maybe
@@ -62,7 +60,7 @@ import Rel8.Table.Maybe
62import Rel8.Table.Nullify ( Nullify, guard )
60import Rel8.Table.Nullify ( Nullify, guard )
63import Rel8.Table.Ord ( OrdTable, ordTable )
61import Rel8.Table.Ord ( OrdTable, ordTable )
64import Rel8.Table.Recontextualize ( Recontextualize )
62import Rel8.Table.Recontextualize ( Recontextualize )
65−import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
63+import Rel8.Table.Serialize ( ToExprs )
66import Rel8.Table.Undefined ( undefined )
64import Rel8.Table.Undefined ( undefined )
67import Rel8.Type.Tag ( MaybeTag )
65import Rel8.Type.Tag ( MaybeTag )
68
66
@@ -71,7 +69,8 @@ import Data.Functor.Apply ( Apply, (<.>) )
71import Data.Functor.Bind ( Bind, (>>-) )
69import Data.Functor.Bind ( Bind, (>>-) )
72
70
73-- these
71-- these
74−import Data.These ( These )
72+import Data.These ( These( This, That, These ) )
73+import Data.These.Combinators ( justHere, justThere )
75
74
76
75
77-- | @TheseTable a b@ is a Rel8 table that contains either the table @a@, the
76-- | @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)
139
138
140instance
139instance
141 ( Table context a, Table context b
140 ( Table context a, Table context b
142− , Reifiable context, Abstract context, context ~ context'
141+ , Reifiable context, context ~ context'
143 )
142 )
144 => Table context' (TheseTable context a b)
143 => Table context' (TheseTable context a b)
145 where
144 where
146 type Columns (TheseTable context a b) = HTheseTable (Columns a) (Columns b)
145 type Columns (TheseTable context a b) = HTheseTable (Columns a) (Columns b)
147 type Context (TheseTable context a b) = Context a
146 type Context (TheseTable context a b) = Context a
147+ type FromExprs (TheseTable context a b) =
148+ These (FromExprs a) (FromExprs b)
148
149
149 toColumns TheseTable {here, there} = HTheseTable
150 toColumns TheseTable {here, there} = HTheseTable
150 { hhereTag = hlabel $ HIdentity $ tag here
151 { hhereTag = hlabel $ HIdentity $ tag here
@@ -166,27 +167,46 @@ instance
166 }
167 }
167 }
168 }
168
169
169− reify proof TheseTable {here, there} = TheseTable
170+ toResult tables = HTheseTable
170− { here = reify proof here
171+ { hhereTag = hrelabel hhereTag
171− , there = reify proof there
172+ , hhere = hrelabel hhere
173+ , hthereTag = hrelabel hthereTag
174+ , hthere = hrelabel hthere
172 }
175 }
173− unreify proof TheseTable {here, there} = TheseTable
176+ where
174− { here = unreify proof here
177+ HMaybeTable
175− , there = unreify proof there
178+ { htag = hhereTag
176− }
179+ , hjust = hhere
177−
180+ } = toResult @_ @(MaybeTable context a) (justHere tables)
178− coherence = coherence @context @a
181+ HMaybeTable
179− congruence proof abstract =
182+ { htag = hthereTag
180− id `apply`
183+ , hjust = hthere
181− congruence @context @a proof abstract `apply`
184+ } = toResult @_ @(MaybeTable context b) (justThere tables)
182− congruence @context @b proof abstract
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+ }
183
203
184
204
185instance
205instance
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
189 , Recontextualize from to a2 b2
207 , Recontextualize from to a2 b2
208+ , Reifiable from, from ~ from'
209+ , Reifiable to, to ~ to'
190 )
210 )
191 => Recontextualize from to (TheseTable from' a1 a2) (TheseTable to' b1 b2)
211 => Recontextualize from to (TheseTable from' a1 a2) (TheseTable to' b1 b2)
192
212
@@ -213,19 +233,8 @@ instance (OrdTable a, OrdTable b, context ~ Expr) =>
213 }
233 }
214
234
215
235
216−type instance FromExprs (TheseTable _context a b) =
217− These (FromExprs a) (FromExprs b)
218−
219−
220instance (ToExprs exprs1 a, ToExprs exprs2 b, x ~ TheseTable Expr exprs1 exprs2) =>
236instance (ToExprs exprs1 a, ToExprs exprs2 b, x ~ TheseTable Expr exprs1 exprs2) =>
221 ToExprs x (These a b)
237 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)
229
238
230
239
231-- | Test if a 'TheseTable' was constructed with 'thisTable'.
240-- | 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
32-- rel8
32-- rel8
33import Rel8.Expr ( Col( E ), Expr )
33import Rel8.Expr ( Col( E ), Expr )
34import Rel8.Expr.Opaleye ( castExpr, fromPrimExpr, toPrimExpr )
34import 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 )
36import Rel8.Schema.Name ( Col( N ), Name( Name ) )
36import Rel8.Schema.Name ( Col( N ), Name( Name ) )
37import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
37import Rel8.Schema.Null ( Nullity( Null, NotNull ) )
38import Rel8.Schema.Result ( Col( R ), Result )
38import Rel8.Schema.Result ( Col( R ), Result )
39import Rel8.Schema.Spec ( SSpec( SSpec, nullity, info ) )
39import Rel8.Schema.Spec ( SSpec( SSpec, nullity, info ) )
40−import Rel8.Table ( Table, fromColumns, toColumns )
40+import Rel8.Table ( fromColumns, toColumns, fromResult, toResult )
41import Rel8.Table.Eq ( EqTable )
41import Rel8.Table.Eq ( EqTable )
42−import Rel8.Table.HKD ( HKD, HKDable, fromHKD, toHKD )
42+import Rel8.Table.HKD ( HKD, HKDable )
43import Rel8.Table.Ord ( OrdTable )
43import Rel8.Table.Ord ( OrdTable )
44import Rel8.Table.Rel8able ()
44import Rel8.Table.Rel8able ()
45import Rel8.Table.Serialize ( lit )
45import Rel8.Table.Serialize ( lit )
@@ -67,8 +67,8 @@ newtype Composite a = Composite
67
67
68instance DBComposite a => DBType (Composite a) where
68instance DBComposite a => DBType (Composite a) where
69 typeInformation = TypeInformation
69 typeInformation = TypeInformation
70− { decode = Hasql.composite (Composite . fromHKD <$> decoder)
70+ { decode = Hasql.composite (Composite . fromResult @_ @(HKD a Expr) <$> decoder)
71− , encode = encoder . lit . toColumns . toHKD . unComposite
71+ , encode = encoder . lit . toResult @_ @(HKD a Expr) . unComposite
72 , typeName = compositeTypeName @a
72 , typeName = compositeTypeName @a
73 }
73 }
74
74
@@ -103,7 +103,7 @@ class (DBType a, HKDable a) => DBComposite a where
103-- single column expression, by combining them into a PostgreSQL composite
103-- single column expression, by combining them into a PostgreSQL composite
104-- type.
104-- type.
105compose :: DBComposite a => HKD a Expr -> Expr a
105compose :: DBComposite a => HKD a Expr -> Expr a
106−compose = castExpr . fromPrimExpr . encoder
106+compose = castExpr . fromPrimExpr . encoder . toColumns
107
107
108
108
109-- | Expand a composite type into a 'HKD'.
109-- | Expand a composite type into a 'HKD'.
@@ -118,8 +118,8 @@ decompose (toPrimExpr -> a) = fromColumns $ htabulate \field ->
118 names = toColumns (compositeFields @a)
118 names = toColumns (compositeFields @a)
119
119
120
120
121−decoder :: Table Result a => Hasql.Composite a
121+decoder :: HTable t => Hasql.Composite (t (Col Result))
122−decoder = fmap fromColumns $ unwrapApplicative $ htabulateA \field ->
122+decoder = unwrapApplicative $ htabulateA \field ->
123 case hfield hspecs field of
123 case hfield hspecs field of
124 SSpec {nullity, info} -> WrapApplicative $ R <$>
124 SSpec {nullity, info} -> WrapApplicative $ R <$>
125 case nullity of
125 case nullity of
@@ -127,8 +127,8 @@ decoder = fmap fromColumns $ unwrapApplicative $ htabulateA \field ->
127 NotNull -> Hasql.field $ Hasql.nonNullable $ decode info
127 NotNull -> Hasql.field $ Hasql.nonNullable $ decode info
128
128
129
129
130−encoder :: Table Expr a => a -> Opaleye.PrimExpr
130+encoder :: HTable t => t (Col Expr) -> Opaleye.PrimExpr
131−encoder (toColumns -> a) = Opaleye.FunExpr "ROW" exprs
131+encoder a = Opaleye.FunExpr "ROW" exprs
132 where
132 where
133 exprs = getConst $ htabulateA \field -> case hfield a field of
133 exprs = getConst $ htabulateA \field -> case hfield a field of
134 E (toPrimExpr -> expr) -> Const [expr]
134 E (toPrimExpr -> expr) -> Const [expr]
src/Rel8/Type/Tag.hs+1−1
@@ -21,7 +21,7 @@ import Prelude
21import qualified Opaleye.Internal.HaskellDB.PrimQuery as Opaleye
21import qualified Opaleye.Internal.HaskellDB.PrimQuery as Opaleye
22
22
23-- rel8
23-- rel8
24−import {-# SOURCE #-} Rel8.Expr ( Expr )
24+import Rel8.Expr ( Expr )
25import Rel8.Expr.Eq ( (==.) )
25import Rel8.Expr.Eq ( (==.) )
26import Rel8.Expr.Opaleye ( zipPrimExprsWith )
26import Rel8.Expr.Opaleye ( zipPrimExprsWith )
27import Rel8.Expr.Serialize ( litExpr )
27import Rel8.Expr.Serialize ( litExpr )
tests/Rel8/Generic/Rel8able/Test.hs+3−15
@@ -1,13 +1,11 @@
1{-# language DataKinds #-}
1{-# language DataKinds #-}
2{-# language DeriveAnyClass #-}
2{-# language DeriveAnyClass #-}
3{-# language DeriveGeneric #-}
3{-# language DeriveGeneric #-}
4−{-# language DerivingVia #-}
4+{-# language DerivingStrategies #-}
5{-# language DuplicateRecordFields #-}
5{-# language DuplicateRecordFields #-}
6{-# language FlexibleInstances #-}
6{-# language FlexibleInstances #-}
7{-# language MultiParamTypeClasses #-}
7{-# language MultiParamTypeClasses #-}
8−{-# language StandaloneDeriving #-}
9{-# language TypeFamilies #-}
8{-# language TypeFamilies #-}
10−{-# language UndecidableInstances #-}
11
9
12{-# options_ghc -O0 #-}
10{-# options_ghc -O0 #-}
13
11
@@ -98,24 +96,14 @@ data S3Object = S3Object
98 deriving stock Generic
96 deriving stock Generic
99
97
100
98
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
107
100
108
101
109data HKDSum = HKDSumA Text | HKDSumB Bool Char | HKDSumC
102data HKDSum = HKDSumA Text | HKDSumB Bool Char | HKDSumC
110 deriving stock Generic
103 deriving stock Generic
111
104
112
105
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
119
107
120
108
121data HKDTest f = HKDTest
109data HKDTest f = HKDTest