git.iko.soy/rel8
on master help sign in
Get rid of Rel8.Table.Unreify and all remaining uses of QuantifiedConstraints (#103)
991998aShane
rel8.cabal+2−1
compare with master
unifiedsplit
@@ -81,6 +81,7 @@ library
81 Rel8.Kind.Algebra
81 Rel8.Kind.Algebra
82 Rel8.Kind.Context
82 Rel8.Kind.Context
83
83
84+ Rel8.Generic.Coherence
84 Rel8.Generic.Construction
85 Rel8.Generic.Construction
85 Rel8.Generic.Construction.ADT
86 Rel8.Generic.Construction.ADT
86 Rel8.Generic.Construction.Record
87 Rel8.Generic.Construction.Record
@@ -114,6 +115,7 @@ library
114 Rel8.Query.Values
115 Rel8.Query.Values
115
116
116 Rel8.Schema.Context
117 Rel8.Schema.Context
118+ Rel8.Schema.Context.Abstract
117 Rel8.Schema.Context.Nullify
119 Rel8.Schema.Context.Nullify
118 Rel8.Schema.Dict
120 Rel8.Schema.Dict
119 Rel8.Schema.HTable
121 Rel8.Schema.HTable
@@ -164,7 +166,6 @@ library
164 Rel8.Table.Serialize
166 Rel8.Table.Serialize
165 Rel8.Table.These
167 Rel8.Table.These
166 Rel8.Table.Undefined
168 Rel8.Table.Undefined
167− Rel8.Table.Unreify
168
169
169 Rel8.Type
170 Rel8.Type
170 Rel8.Type.Array
171 Rel8.Type.Array
src/Rel8/Aggregate.hs+3−1
@@ -41,7 +41,7 @@ import Rel8.Schema.Result ( Result )
41import Rel8.Schema.Spec ( Spec( Spec ) )
41import Rel8.Schema.Spec ( Spec( Spec ) )
42import Rel8.Table
42import Rel8.Table
43 ( Table, Columns, Context, fromColumns, toColumns
43 ( Table, Columns, Context, fromColumns, toColumns
44− , reify, unreify
44+ , reify, unreify, coherence, congruence
45 )
45 )
46import Rel8.Table.Recontextualize ( Recontextualize )
46import Rel8.Table.Recontextualize ( Recontextualize )
47import Rel8.Type ( DBType )
47import Rel8.Type ( DBType )
@@ -73,6 +73,8 @@ instance Sql DBType a => Table Aggregate (Aggregate a) where
73
73
74 reify = notReify
74 reify = notReify
75 unreify = notReify
75 unreify = notReify
76+ coherence = notReify
77+ congruence = notReify
76
78
77
79
78instance Sql DBType a =>
80instance Sql DBType a =>
src/Rel8/Column.hs+20−6
@@ -2,7 +2,9 @@
2{-# language FlexibleContexts #-}
2{-# language FlexibleContexts #-}
3{-# language LambdaCase #-}
3{-# language LambdaCase #-}
4{-# language MultiParamTypeClasses #-}
4{-# language MultiParamTypeClasses #-}
5+{-# language ScopedTypeVariables #-}
5{-# language StandaloneKindSignatures #-}
6{-# language StandaloneKindSignatures #-}
7+{-# language TypeApplications #-}
6{-# language TypeFamilies #-}
8{-# language TypeFamilies #-}
7
9
8module Rel8.Column
10module Rel8.Column
@@ -13,6 +15,7 @@ where
13
15
14-- base
16-- base
15import Data.Kind ( Type )
17import Data.Kind ( Type )
18+import Data.Type.Equality ( (:~:)( Refl ) )
16import Prelude
19import Prelude
17
20
18-- rel8
21-- rel8
@@ -25,11 +28,11 @@ import qualified Rel8.Schema.Kind as K
25import Rel8.Schema.Name ( Name(..), Col( N ) )
28import Rel8.Schema.Name ( Name(..), Col( N ) )
26import Rel8.Schema.Null ( Sql )
29import Rel8.Schema.Null ( Sql )
27import Rel8.Schema.Reify ( Reify, Col(..) )
30import Rel8.Schema.Reify ( Reify, Col(..) )
28−import Rel8.Schema.Result ( Col( R ), Result )
31+import Rel8.Schema.Result ( Col( R ), Result, absurd )
29import Rel8.Schema.Spec ( Spec( Spec ) )
32import Rel8.Schema.Spec ( Spec( Spec ) )
30import Rel8.Table
33import Rel8.Table
31 ( Table, Columns, Context, fromColumns, toColumns
34 ( Table, Columns, Context, fromColumns, toColumns
32− , Unreify, reify, unreify
35+ , Unreify, reify, unreify, coherence, congruence
33 )
36 )
34import Rel8.Table.Recontextualize ( Recontextualize )
37import Rel8.Table.Recontextualize ( Recontextualize )
35import Rel8.Type ( DBType )
38import Rel8.Type ( DBType )
@@ -63,11 +66,22 @@ instance (Reifiable context, Sql DBType a) =>
63 reify _ = AColumn
66 reify _ = AColumn
64 unreify _ (AColumn a) = a
67 unreify _ (AColumn a) = a
65
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
66
75
67−instance
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+
68− ( Reifiable context, Reifiable context'
84+instance (Reifiable context, Reifiable context', Sql DBType a) =>
69− , Sql DBType a
70− ) =>
71 Recontextualize
85 Recontextualize
72 (Reify context)
86 (Reify context)
73 (Reify context')
87 (Reify context')
src/Rel8/Column/ADT.hs+20−2
@@ -1,7 +1,9 @@
1{-# language DataKinds #-}
1{-# language DataKinds #-}
2{-# language LambdaCase #-}
2{-# language LambdaCase #-}
3{-# language MultiParamTypeClasses #-}
3{-# language MultiParamTypeClasses #-}
4+{-# language ScopedTypeVariables #-}
4{-# language StandaloneKindSignatures #-}
5{-# language StandaloneKindSignatures #-}
6+{-# language TypeApplications #-}
5{-# language TypeFamilies #-}
7{-# language TypeFamilies #-}
6{-# language UndecidableInstances #-}
8{-# language UndecidableInstances #-}
7
9
@@ -12,6 +14,7 @@ where
12
14
13-- base
15-- base
14import Data.Kind ( Type )
16import Data.Kind ( Type )
17+import Data.Type.Equality ( (:~:)( Refl ) )
15import Prelude
18import Prelude
16
19
17-- rel8
20-- rel8
@@ -20,12 +23,13 @@ import Rel8.Kind.Context ( SContext(..), Reifiable, contextSing )
20import Rel8.Schema.Context ( Col )
23import Rel8.Schema.Context ( Col )
21import qualified Rel8.Schema.Kind as K
24import qualified Rel8.Schema.Kind as K
22import Rel8.Schema.Reify ( Reify, hreify, hunreify )
25import Rel8.Schema.Reify ( Reify, hreify, hunreify )
23−import Rel8.Schema.Result ( Result )
26+import Rel8.Schema.Result ( Result, absurd )
24import Rel8.Table
27import Rel8.Table
25 ( Table, Columns, Context, fromColumns, toColumns
28 ( Table, Columns, Context, fromColumns, toColumns
26− , Unreify, reify, unreify
29+ , Unreify, reify, unreify, coherence, congruence
27 )
30 )
28import Rel8.Table.ADT ( ADT( ADT ), ADTable, fromADT, toADT )
31import Rel8.Table.ADT ( ADT( ADT ), ADTable, fromADT, toADT )
32+import Rel8.Table.Rel8able ()
29import Rel8.Table.Recontextualize ( Recontextualize )
33import Rel8.Table.Recontextualize ( Recontextualize )
30
34
31
35
@@ -52,6 +56,20 @@ instance (ADTable t, Reifiable context) =>
52 reify _ = AHADT
56 reify _ = AHADT
53 unreify _ (AHADT a) = a
57 unreify _ (AHADT a) = a
54
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+
55
73
56instance
74instance
57 ( Reifiable context, Reifiable context'
75 ( Reifiable context, Reifiable context'
src/Rel8/Column/Either.hs+33−3
@@ -2,7 +2,9 @@
2{-# language FlexibleContexts #-}
2{-# language FlexibleContexts #-}
3{-# language LambdaCase #-}
3{-# language LambdaCase #-}
4{-# language MultiParamTypeClasses #-}
4{-# language MultiParamTypeClasses #-}
5+{-# language ScopedTypeVariables #-}
5{-# language StandaloneKindSignatures #-}
6{-# language StandaloneKindSignatures #-}
7+{-# language TypeApplications #-}
6{-# language TypeFamilyDependencies #-}
8{-# language TypeFamilyDependencies #-}
7{-# language UndecidableInstances #-}
9{-# language UndecidableInstances #-}
8
10
@@ -13,9 +15,11 @@ where
13
15
14-- base
16-- base
15import Control.Applicative ( liftA2 )
17import Control.Applicative ( liftA2 )
18+import Control.Category ( id )
16import Data.Bifunctor ( Bifunctor, bimap )
19import Data.Bifunctor ( Bifunctor, bimap )
17import Data.Kind ( Type )
20import Data.Kind ( Type )
21+import Data.Type.Equality ( (:~:)( Refl ), apply )
18−import Prelude
22+import Prelude hiding ( id )
19
23
20-- rel8
24-- rel8
21import Rel8.Aggregate ( Aggregate )
25import Rel8.Aggregate ( Aggregate )
@@ -26,10 +30,10 @@ import Rel8.Schema.HTable.Either ( HEitherTable )
26import qualified Rel8.Schema.Kind as K
30import qualified Rel8.Schema.Kind as K
27import Rel8.Schema.Name ( Name(..) )
31import Rel8.Schema.Name ( Name(..) )
28import Rel8.Schema.Reify ( Reify, hreify, hunreify )
32import Rel8.Schema.Reify ( Reify, hreify, hunreify )
29−import Rel8.Schema.Result ( Result )
33+import Rel8.Schema.Result ( Result, absurd )
30import Rel8.Table
34import Rel8.Table
31 ( Table, Columns, Context, fromColumns, toColumns
35 ( Table, Columns, Context, fromColumns, toColumns
32− , Unreify, reify, unreify
36+ , Unreify, reify, unreify, coherence, congruence
33 )
37 )
34import Rel8.Table.Either ( EitherTable )
38import Rel8.Table.Either ( EitherTable )
35import Rel8.Table.Recontextualize ( Recontextualize )
39import Rel8.Table.Recontextualize ( Recontextualize )
@@ -71,6 +75,32 @@ instance (Reifiable context, Table (Reify context) a, Table (Reify context) b)
71 reify proof = liftA2 bimap reify reify proof . AHEither
75 reify proof = liftA2 bimap reify reify proof . AHEither
72 unreify proof = (\(AHEither a) -> a) . liftA2 bimap unreify unreify proof
76 unreify proof = (\(AHEither a) -> a) . liftA2 bimap unreify unreify proof
73
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+
74
104
75instance
105instance
76 ( Reifiable context, Reifiable context'
106 ( Reifiable context, Reifiable context'
src/Rel8/Column/Lift.hs+19−2
@@ -1,7 +1,9 @@
1{-# language DataKinds #-}
1{-# language DataKinds #-}
2{-# language LambdaCase #-}
2{-# language LambdaCase #-}
3{-# language MultiParamTypeClasses #-}
3{-# language MultiParamTypeClasses #-}
4+{-# language ScopedTypeVariables #-}
4{-# language StandaloneKindSignatures #-}
5{-# language StandaloneKindSignatures #-}
6+{-# language TypeApplications #-}
5{-# language TypeFamilies #-}
7{-# language TypeFamilies #-}
6
8
7module Rel8.Column.Lift
9module Rel8.Column.Lift
@@ -11,6 +13,7 @@ where
11
13
12-- base
14-- base
13import Data.Kind ( Type )
15import Data.Kind ( Type )
16+import Data.Type.Equality ( (:~:)( Refl ) )
14import Prelude
17import Prelude
15
18
16-- rel8
19-- rel8
@@ -19,10 +22,10 @@ import Rel8.Kind.Context ( Reifiable(..), SContext(..) )
19import Rel8.Schema.Context ( Col )
22import Rel8.Schema.Context ( Col )
20import qualified Rel8.Schema.Kind as K
23import qualified Rel8.Schema.Kind as K
21import Rel8.Schema.Reify ( Reify, hreify, hunreify )
24import Rel8.Schema.Reify ( Reify, hreify, hunreify )
22−import Rel8.Schema.Result ( Result )
25+import Rel8.Schema.Result ( Result, absurd )
23import Rel8.Table
26import Rel8.Table
24 ( Table, Columns, Context, fromColumns, toColumns
27 ( Table, Columns, Context, fromColumns, toColumns
25− , Unreify, reify, unreify
28+ , Unreify, reify, unreify, coherence, congruence
26 )
29 )
27import Rel8.Table.Rel8able ()
30import Rel8.Table.Rel8able ()
28import Rel8.Table.HKD ( HKD( HKD ), HKDable, fromHKD, toHKD )
31import Rel8.Table.HKD ( HKD( HKD ), HKDable, fromHKD, toHKD )
@@ -54,6 +57,20 @@ instance (Reifiable context, HKDable a) =>
54 reify _ = ALift
57 reify _ = ALift
55 unreify _ (ALift a) = a
58 unreify _ (ALift a) = a
56
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+
57
74
58instance (Reifiable context, Reifiable context', HKDable a) =>
75instance (Reifiable context, Reifiable context', HKDable a) =>
59 Recontextualize
76 Recontextualize
src/Rel8/Column/List.hs+52−25
@@ -2,7 +2,10 @@
2{-# language FlexibleContexts #-}
2{-# language FlexibleContexts #-}
3{-# language LambdaCase #-}
3{-# language LambdaCase #-}
4{-# language MultiParamTypeClasses #-}
4{-# language MultiParamTypeClasses #-}
5+{-# language RankNTypes #-}
6+{-# language ScopedTypeVariables #-}
5{-# language StandaloneKindSignatures #-}
7{-# language StandaloneKindSignatures #-}
8+{-# language TypeApplications #-}
6{-# language TypeFamilyDependencies #-}
9{-# language TypeFamilyDependencies #-}
7{-# language UndecidableInstances #-}
10{-# language UndecidableInstances #-}
8
11
@@ -12,27 +15,28 @@ module Rel8.Column.List
12where
15where
13
16
14-- base
17-- base
18+import Control.Category ( id )
15import Data.Kind ( Type )
19import Data.Kind ( Type )
16−import Data.Type.Equality ( (:~:)( Refl ) )
20+import Data.Type.Equality ( (:~:)( Refl ), apply )
17−import Prelude
21+import Prelude hiding ( id )
18
22
19-- rel8
23-- rel8
20import Rel8.Aggregate ( Aggregate )
24import Rel8.Aggregate ( Aggregate )
21import Rel8.Expr ( Expr )
25import Rel8.Expr ( Expr )
22import Rel8.Kind.Context ( SContext(..), Reifiable( contextSing ) )
26import Rel8.Kind.Context ( SContext(..), Reifiable( contextSing ) )
23import Rel8.Schema.Context ( Col )
27import Rel8.Schema.Context ( Col )
28+import Rel8.Schema.Context.Abstract ( exclusivity, virtualOrResult )
24import Rel8.Schema.HTable.List ( HListTable )
29import Rel8.Schema.HTable.List ( HListTable )
25import qualified Rel8.Schema.Kind as K
30import qualified Rel8.Schema.Kind as K
26import Rel8.Schema.Name ( Name )
31import Rel8.Schema.Name ( Name )
27import Rel8.Schema.Reify ( Reify, hreify, hunreify )
32import Rel8.Schema.Reify ( Reify, hreify, hunreify )
28−import Rel8.Schema.Result ( Result )
33+import Rel8.Schema.Result ( Result, absurd )
29import Rel8.Table
34import Rel8.Table
30 ( Table, Columns, Congruent, Context, fromColumns, toColumns
35 ( Table, Columns, Congruent, Context, fromColumns, toColumns
31− , Unreify, reify, unreify
36+ , Unreify, reify, unreify, coherence, congruence
32 )
37 )
33import Rel8.Table.List ( ListTable( ListTable ) )
38import Rel8.Table.List ( ListTable( ListTable ) )
34import Rel8.Table.Recontextualize ( Recontextualize )
39import Rel8.Table.Recontextualize ( Recontextualize )
35−import Rel8.Table.Unreify ( Unreifiability(..), Unreifiable, unreifiability )
36
40
37
41
38-- | Nest a list within a 'Rel8able'. @HList f a@ will produce a 'ListTable'
42-- | Nest a list within a 'Rel8able'. @HList f a@ will produce a 'ListTable'
@@ -50,7 +54,7 @@ type AHList :: K.Context -> Type -> Type
50newtype AHList context a = AHList (HList context a)
54newtype AHList context a = AHList (HList context a)
51
55
52
56
53−instance (Reifiable context, Unreifiable a, Table (Reify context) a) =>
57+instance (Reifiable context, Table (Reify context) a) =>
54 Table (Reify context) (AHList context a)
58 Table (Reify context) (AHList context a)
55 where
59 where
56 type Context (AHList context a) = Reify context
60 type Context (AHList context a) = Reify context
@@ -60,13 +64,26 @@ instance (Reifiable context, Unreifiable a, Table (Reify context) a) =>
60 fromColumns = sfromColumnsList contextSing
64 fromColumns = sfromColumnsList contextSing
61 toColumns = stoColumnsList contextSing
65 toColumns = stoColumnsList contextSing
62
66
63− reify _ = sreifyList (unreifiability contextSing)
67+ reify _ = sreifyList contextSing
64− unreify _ = sunreifyList (unreifiability 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
65
83
66
84
67instance
85instance
68 ( Reifiable context, Reifiable context'
86 ( Reifiable context, Reifiable context'
69− , Unreifiable a, Unreifiable a'
70 , Recontextualize (Reify context) (Reify context') a a'
87 , Recontextualize (Reify context) (Reify context') a a'
71 )
88 )
72 => Recontextualize
89 => Recontextualize
@@ -123,23 +140,33 @@ stoColumnsList = \case
123 (\(AHList a) -> a)
140 (\(AHList a) -> a)
124
141
125
142
126−sreifyList :: Table (Reify context) a
143+sreifyList :: forall context a. Table (Reify context) a
127− => Unreifiability context a
144+ => SContext context
128 -> HList context (Unreify a)
145 -> HList context (Unreify a)
129 -> AHList context a
146 -> AHList context a
130−sreifyList = \case
147+sreifyList context = case virtualOrResult context of
131− UResult -> AHList . fmap (reify Refl)
148+ Left Refl -> AHList . fmap (reify Refl)
132− Unreifiability context ->
149+ Right virtual ->
150+ case coherence @(Reify context) @a Refl abstract of
151+ Refl -> case congruence @(Reify context) @a Refl abstract of
152+ Refl ->
133− smapList context (reify Refl) hreify .
153+ smapList context (reify Refl) hreify .
134− AHList
154+ AHList
135−
155+ where
136−
156+ abstract = exclusivity virtual
157+
158+
137−sunreifyList :: Table (Reify context) a
159+sunreifyList :: forall context a. Table (Reify context) a
138− => Unreifiability context a
160+ => SContext context
139 -> AHList context a
161 -> AHList context a
140 -> HList context (Unreify a)
162 -> HList context (Unreify a)
141−sunreifyList = \case
163+sunreifyList context = case virtualOrResult context of
142− UResult -> fmap (unreify Refl) . (\(AHList a) -> a)
164+ Left Refl -> fmap (unreify Refl) . (\(AHList a) -> a)
143− Unreifiability context ->
165+ Right virtual ->
166+ case coherence @(Reify context) @a Refl abstract of
167+ Refl -> case congruence @(Reify context) @a Refl abstract of
168+ Refl ->
144− (\(AHList a) -> a) .
169+ (\(AHList a) -> a) .
145− smapList context (unreify Refl) hunreify
170+ smapList context (unreify Refl) hunreify
171+ where
172+ abstract = exclusivity virtual
src/Rel8/Column/Maybe.hs+21−3
@@ -3,7 +3,9 @@
3{-# language GADTs #-}
3{-# language GADTs #-}
4{-# language LambdaCase #-}
4{-# language LambdaCase #-}
5{-# language MultiParamTypeClasses #-}
5{-# language MultiParamTypeClasses #-}
6+{-# language ScopedTypeVariables #-}
6{-# language StandaloneKindSignatures #-}
7{-# language StandaloneKindSignatures #-}
8+{-# language TypeApplications #-}
7{-# language TypeFamilyDependencies #-}
9{-# language TypeFamilyDependencies #-}
8{-# language UndecidableInstances #-}
10{-# language UndecidableInstances #-}
9
11
@@ -13,8 +15,10 @@ module Rel8.Column.Maybe
13where
15where
14
16
15-- base
17-- base
18+import Control.Category ( id )
16import Data.Kind ( Type )
19import Data.Kind ( Type )
20+import Data.Type.Equality ( (:~:)( Refl ), apply )
17−import Prelude
21+import Prelude hiding ( id )
18
22
19-- rel8
23-- rel8
20import Rel8.Aggregate ( Aggregate )
24import Rel8.Aggregate ( Aggregate )
@@ -25,10 +29,10 @@ import Rel8.Schema.HTable.Maybe ( HMaybeTable )
25import qualified Rel8.Schema.Kind as K
29import qualified Rel8.Schema.Kind as K
26import Rel8.Schema.Name ( Name )
30import Rel8.Schema.Name ( Name )
27import Rel8.Schema.Reify ( Reify, hreify, hunreify )
31import Rel8.Schema.Reify ( Reify, hreify, hunreify )
28−import Rel8.Schema.Result ( Result )
32+import Rel8.Schema.Result ( Result, absurd )
29import Rel8.Table
33import Rel8.Table
30 ( Table, Columns, Context, fromColumns, toColumns
34 ( Table, Columns, Context, fromColumns, toColumns
31− , Unreify, reify, unreify
35+ , Unreify, reify, unreify, coherence, congruence
32 )
36 )
33import Rel8.Table.Maybe ( MaybeTable )
37import Rel8.Table.Maybe ( MaybeTable )
34import Rel8.Table.Recontextualize ( Recontextualize )
38import Rel8.Table.Recontextualize ( Recontextualize )
@@ -66,6 +70,20 @@ instance (Reifiable context, Table (Reify context) a) =>
66 reify proof = fmap fmap reify proof . AHMaybe
70 reify proof = fmap fmap reify proof . AHMaybe
67 unreify proof = (\(AHMaybe a) -> a) . fmap fmap unreify proof
71 unreify proof = (\(AHMaybe a) -> a) . fmap fmap unreify proof
68
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+
69
87
70instance
88instance
71 ( Reifiable context, Reifiable context'
89 ( Reifiable context, Reifiable context'
src/Rel8/Column/NonEmpty.hs+51−25
@@ -2,7 +2,9 @@
2{-# language FlexibleContexts #-}
2{-# language FlexibleContexts #-}
3{-# language LambdaCase #-}
3{-# language LambdaCase #-}
4{-# language MultiParamTypeClasses #-}
4{-# language MultiParamTypeClasses #-}
5+{-# language ScopedTypeVariables #-}
5{-# language StandaloneKindSignatures #-}
6{-# language StandaloneKindSignatures #-}
7+{-# language TypeApplications #-}
6{-# language TypeFamilyDependencies #-}
8{-# language TypeFamilyDependencies #-}
7{-# language UndecidableInstances #-}
9{-# language UndecidableInstances #-}
8
10
@@ -12,28 +14,29 @@ module Rel8.Column.NonEmpty
12where
14where
13
15
14-- base
16-- base
17+import Control.Category ( id )
15import Data.Kind ( Type )
18import Data.Kind ( Type )
16import Data.List.NonEmpty ( NonEmpty )
19import Data.List.NonEmpty ( NonEmpty )
17−import Data.Type.Equality ( (:~:)( Refl ) )
20+import Data.Type.Equality ( (:~:)( Refl ), apply )
18−import Prelude
21+import Prelude hiding ( id )
19
22
20-- rel8
23-- rel8
21import Rel8.Aggregate ( Aggregate )
24import Rel8.Aggregate ( Aggregate )
22import Rel8.Expr ( Expr )
25import Rel8.Expr ( Expr )
23import Rel8.Kind.Context ( SContext(..), Reifiable( contextSing ) )
26import Rel8.Kind.Context ( SContext(..), Reifiable( contextSing ) )
24import Rel8.Schema.Context ( Col )
27import Rel8.Schema.Context ( Col )
28+import Rel8.Schema.Context.Abstract ( exclusivity, virtualOrResult )
25import Rel8.Schema.HTable.NonEmpty ( HNonEmptyTable )
29import Rel8.Schema.HTable.NonEmpty ( HNonEmptyTable )
26import qualified Rel8.Schema.Kind as K
30import qualified Rel8.Schema.Kind as K
27import Rel8.Schema.Name ( Name )
31import Rel8.Schema.Name ( Name )
28import Rel8.Schema.Reify ( Reify, hreify, hunreify )
32import Rel8.Schema.Reify ( Reify, hreify, hunreify )
29−import Rel8.Schema.Result ( Result )
33+import Rel8.Schema.Result ( Result, absurd )
30import Rel8.Table
34import Rel8.Table
31 ( Table, Columns, Congruent, Context, fromColumns, toColumns
35 ( Table, Columns, Congruent, Context, fromColumns, toColumns
32− , Unreify, reify, unreify
36+ , Unreify, reify, unreify, coherence, congruence
33 )
37 )
34import Rel8.Table.NonEmpty ( NonEmptyTable( NonEmptyTable ) )
38import Rel8.Table.NonEmpty ( NonEmptyTable( NonEmptyTable ) )
35import Rel8.Table.Recontextualize ( Recontextualize )
39import Rel8.Table.Recontextualize ( Recontextualize )
36−import Rel8.Table.Unreify ( Unreifiability(..), Unreifiable, unreifiability )
37
40
38
41
39-- | Nest a 'NonEmpty' list within a 'Rel8able'. @HNonEmpty f a@ will produce a
42-- | Nest a 'NonEmpty' list within a 'Rel8able'. @HNonEmpty f a@ will produce a
@@ -52,7 +55,7 @@ type AHNonEmpty :: K.Context -> Type -> Type
52newtype AHNonEmpty context a = AHNonEmpty (HNonEmpty context a)
55newtype AHNonEmpty context a = AHNonEmpty (HNonEmpty context a)
53
56
54
57
55−instance (Reifiable context, Unreifiable a, Table (Reify context) a) =>
58+instance (Reifiable context, Table (Reify context) a) =>
56 Table (Reify context) (AHNonEmpty context a)
59 Table (Reify context) (AHNonEmpty context a)
57 where
60 where
58 type Context (AHNonEmpty context a) = Reify context
61 type Context (AHNonEmpty context a) = Reify context
@@ -62,13 +65,26 @@ instance (Reifiable context, Unreifiable a, Table (Reify context) a) =>
62 fromColumns = sfromColumnsNonEmpty contextSing
65 fromColumns = sfromColumnsNonEmpty contextSing
63 toColumns = stoColumnsNonEmpty contextSing
66 toColumns = stoColumnsNonEmpty contextSing
64
67
65− reify _ = sreifyNonEmpty (unreifiability contextSing)
68+ reify _ = sreifyNonEmpty contextSing
66− unreify _ = sunreifyNonEmpty (unreifiability 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
67
84
68
85
69instance
86instance
70 ( Reifiable context, Reifiable context'
87 ( Reifiable context, Reifiable context'
71− , Unreifiable a, Unreifiable a'
72 , Recontextualize (Reify context) (Reify context') a a'
88 , Recontextualize (Reify context) (Reify context') a a'
73 )
89 )
74 => Recontextualize
90 => Recontextualize
@@ -126,23 +142,33 @@ stoColumnsNonEmpty = \case
126 (\(AHNonEmpty a) -> a)
142 (\(AHNonEmpty a) -> a)
127
143
128
144
129−sreifyNonEmpty :: Table (Reify context) a
145+sreifyNonEmpty :: forall context a. Table (Reify context) a
130− => Unreifiability context a
146+ => SContext context
131 -> HNonEmpty context (Unreify a)
147 -> HNonEmpty context (Unreify a)
132 -> AHNonEmpty context a
148 -> AHNonEmpty context a
133−sreifyNonEmpty = \case
149+sreifyNonEmpty context = case virtualOrResult context of
134− UResult -> AHNonEmpty . fmap (reify Refl)
150+ Left Refl -> AHNonEmpty . fmap (reify Refl)
135− Unreifiability context ->
151+ Right virtual ->
152+ case coherence @(Reify context) @a Refl abstract of
153+ Refl -> case congruence @(Reify context) @a Refl abstract of
154+ Refl ->
136− smapNonEmpty context (reify Refl) hreify .
155+ smapNonEmpty context (reify Refl) hreify .
137− AHNonEmpty
156+ AHNonEmpty
138−
157+ where
139−
158+ abstract = exclusivity virtual
159+
160+
140−sunreifyNonEmpty :: Table (Reify context) a
161+sunreifyNonEmpty :: forall context a. Table (Reify context) a
141− => Unreifiability context a
162+ => SContext context
142 -> AHNonEmpty context a
163 -> AHNonEmpty context a
143 -> HNonEmpty context (Unreify a)
164 -> HNonEmpty context (Unreify a)
144−sunreifyNonEmpty = \case
165+sunreifyNonEmpty context = case virtualOrResult context of
145− UResult -> fmap (unreify Refl) . (\(AHNonEmpty a) -> a)
166+ Left Refl -> fmap (unreify Refl) . (\(AHNonEmpty a) -> a)
146− Unreifiability context ->
167+ Right virtual ->
168+ case coherence @(Reify context) @a Refl abstract of
169+ Refl -> case congruence @(Reify context) @a Refl abstract of
170+ Refl ->
147− (\(AHNonEmpty a) -> a) .
171+ (\(AHNonEmpty a) -> a) .
148− smapNonEmpty context (unreify Refl) hunreify
172+ smapNonEmpty context (unreify Refl) hunreify
173+ where
174+ abstract = exclusivity virtual
src/Rel8/Column/These.hs+33−3
@@ -3,7 +3,9 @@
3{-# language GADTs #-}
3{-# language GADTs #-}
4{-# language LambdaCase #-}
4{-# language LambdaCase #-}
5{-# language MultiParamTypeClasses #-}
5{-# language MultiParamTypeClasses #-}
6+{-# language ScopedTypeVariables #-}
6{-# language StandaloneKindSignatures #-}
7{-# language StandaloneKindSignatures #-}
8+{-# language TypeApplications #-}
7{-# language TypeFamilyDependencies #-}
9{-# language TypeFamilyDependencies #-}
8{-# language UndecidableInstances #-}
10{-# language UndecidableInstances #-}
9
11
@@ -14,9 +16,11 @@ where
14
16
15-- base
17-- base
16import Control.Applicative ( liftA2 )
18import Control.Applicative ( liftA2 )
19+import Control.Category ( id )
17import Data.Bifunctor ( Bifunctor, bimap )
20import Data.Bifunctor ( Bifunctor, bimap )
18import Data.Kind ( Type )
21import Data.Kind ( Type )
22+import Data.Type.Equality ( (:~:)( Refl ), apply )
19−import Prelude
23+import Prelude hiding ( id )
20
24
21-- rel8
25-- rel8
22import Rel8.Aggregate ( Aggregate )
26import Rel8.Aggregate ( Aggregate )
@@ -27,10 +31,10 @@ import Rel8.Schema.HTable.These ( HTheseTable )
27import qualified Rel8.Schema.Kind as K
31import qualified Rel8.Schema.Kind as K
28import Rel8.Schema.Name ( Name )
32import Rel8.Schema.Name ( Name )
29import Rel8.Schema.Reify ( Reify, hreify, hunreify )
33import Rel8.Schema.Reify ( Reify, hreify, hunreify )
30−import Rel8.Schema.Result ( Result )
34+import Rel8.Schema.Result ( Result, absurd )
31import Rel8.Table
35import Rel8.Table
32 ( Table, Columns, Context, fromColumns, toColumns
36 ( Table, Columns, Context, fromColumns, toColumns
33− , Unreify, reify, unreify
37+ , Unreify, reify, unreify, coherence, congruence
34 )
38 )
35import Rel8.Table.Recontextualize ( Recontextualize )
39import Rel8.Table.Recontextualize ( Recontextualize )
36import Rel8.Table.These ( TheseTable )
40import Rel8.Table.These ( TheseTable )
@@ -75,6 +79,32 @@ instance (Reifiable context, Table (Reify context) a, Table (Reify context) b)
75 reify proof = liftA2 bimap reify reify proof . AHThese
79 reify proof = liftA2 bimap reify reify proof . AHThese
76 unreify proof = (\(AHThese a) -> a) . liftA2 bimap unreify unreify proof
80 unreify proof = (\(AHThese a) -> a) . liftA2 bimap unreify unreify proof
77
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+
78
108
79instance
109instance
80 ( Reifiable context, Reifiable context'
110 ( Reifiable context, Reifiable context'
src/Rel8/Expr.hs+4−1
@@ -45,7 +45,8 @@ import Rel8.Schema.Reify ( notReify )
45import Rel8.Schema.Result ( Result )
45import Rel8.Schema.Result ( Result )
46import Rel8.Schema.Spec ( Spec( Spec ) )
46import Rel8.Schema.Spec ( Spec( Spec ) )
47import Rel8.Table
47import Rel8.Table
48− ( Table, Columns, Context, fromColumns, toColumns, reify, unreify
48+ ( Table, Columns, Context, fromColumns, toColumns
49+ , reify, unreify, coherence, congruence
49 )
50 )
50import Rel8.Table.Recontextualize ( Recontextualize )
51import Rel8.Table.Recontextualize ( Recontextualize )
51import Rel8.Type ( DBType )
52import Rel8.Type ( DBType )
@@ -138,6 +139,8 @@ instance Sql DBType a => Table Expr (Expr a) where
138 fromColumns (HType (E a)) = a
139 fromColumns (HType (E a)) = a
139 reify = notReify
140 reify = notReify
140 unreify = notReify
141 unreify = notReify
142+ coherence = notReify
143+ congruence = notReify
141
144
142
145
143instance Sql DBType a => Recontextualize Expr Expr (Expr a) (Expr a)
146instance Sql DBType a => Recontextualize Expr Expr (Expr a) (Expr a)
src/Rel8/Generic/Coherence.hsnew file+79
@@ -0,0 +1,79 @@
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/Schema/Context/Abstract.hsnew file+80
@@ -0,0 +1,80 @@
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/HTable/Nullify.hs−1
@@ -8,7 +8,6 @@
8{-# language LambdaCase #-}
8{-# language LambdaCase #-}
9{-# language MultiParamTypeClasses #-}
9{-# language MultiParamTypeClasses #-}
10{-# language NamedFieldPuns #-}
10{-# language NamedFieldPuns #-}
11−{-# language QuantifiedConstraints #-}
12{-# language RankNTypes #-}
11{-# language RankNTypes #-}
13{-# language RecordWildCards #-}
12{-# language RecordWildCards #-}
14{-# language ScopedTypeVariables #-}
13{-# language ScopedTypeVariables #-}
src/Rel8/Schema/HTable/Vectorize.hs−1
@@ -10,7 +10,6 @@
10{-# language LambdaCase #-}
10{-# language LambdaCase #-}
11{-# language MultiParamTypeClasses #-}
11{-# language MultiParamTypeClasses #-}
12{-# language NamedFieldPuns #-}
12{-# language NamedFieldPuns #-}
13−{-# language QuantifiedConstraints #-}
14{-# language RankNTypes #-}
13{-# language RankNTypes #-}
15{-# language RecordWildCards #-}
14{-# language RecordWildCards #-}
16{-# language ScopedTypeVariables #-}
15{-# language ScopedTypeVariables #-}
src/Rel8/Schema/Name.hs+4−1
@@ -34,7 +34,8 @@ import Rel8.Schema.Reify ( notReify )
34import Rel8.Schema.Result ( Result )
34import Rel8.Schema.Result ( Result )
35import Rel8.Schema.Spec ( Spec( Spec ) )
35import Rel8.Schema.Spec ( Spec( Spec ) )
36import Rel8.Table
36import Rel8.Table
37− ( Table, Columns, Context, fromColumns, toColumns, reify, unreify
37+ ( Table, Columns, Context, fromColumns, toColumns
38+ , reify, unreify, coherence, congruence
38 )
39 )
39import Rel8.Table.Recontextualize ( Recontextualize )
40import Rel8.Table.Recontextualize ( Recontextualize )
40import Rel8.Type ( DBType )
41import Rel8.Type ( DBType )
@@ -64,6 +65,8 @@ instance Sql DBType a => Table Name (Name a) where
64 fromColumns (HType (N a)) = a
65 fromColumns (HType (N a)) = a
65 reify = notReify
66 reify = notReify
66 unreify = notReify
67 unreify = notReify
68+ coherence = notReify
69+ congruence = notReify
67
70
68
71
69instance Sql DBType a => Recontextualize Expr Name (Expr a) (Name a)
72instance Sql DBType a => Recontextualize Expr Name (Expr a) (Name a)
src/Rel8/Schema/Result.hs+19
@@ -1,17 +1,21 @@
1{-# language DataKinds #-}
1{-# language DataKinds #-}
2+{-# language EmptyCase #-}
2{-# language GADTs #-}
3{-# language GADTs #-}
4+{-# language LambdaCase #-}
3{-# language NamedFieldPuns #-}
5{-# language NamedFieldPuns #-}
4{-# language StandaloneKindSignatures #-}
6{-# language StandaloneKindSignatures #-}
5{-# language TypeFamilies #-}
7{-# language TypeFamilies #-}
6
8
7module Rel8.Schema.Result
9module Rel8.Schema.Result
8 ( Col( R, unR ), Result
10 ( Col( R, unR ), Result
11+ , NotResult( NotResult ), absurd
9 , null, nullifier, unnullifier
12 , null, nullifier, unnullifier
10 , vectorizer, unvectorizer
13 , vectorizer, unvectorizer
11 )
14 )
12where
15where
13
16
14-- base
17-- base
18+import Data.Kind ( Type )
15import Prelude hiding ( null )
19import Prelude hiding ( null )
16
20
17-- rel8
21-- rel8
@@ -34,6 +38,21 @@ instance Interpretation Result where
34 R :: {unR :: !a} -> Col Result ('Spec a)
38 R :: {unR :: !a} -> Col Result ('Spec a)
35
39
36
40
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+
37null :: Col Result ('Spec (Maybe a))
56null :: Col Result ('Spec (Maybe a))
38null = R Nothing
57null = R Nothing
39
58
src/Rel8/Table.hs+87−14
@@ -15,7 +15,10 @@
15{-# language UndecidableInstances #-}
15{-# language UndecidableInstances #-}
16
16
17module Rel8.Table
17module Rel8.Table
18+ ( Table
18− ( Table (Columns, Context, Unreify, toColumns, fromColumns, reify, unreify)
19+ ( Columns, Context, toColumns, fromColumns
20+ , Unreify, reify, unreify, coherence, congruence
21+ )
19 , Congruent
22 , Congruent
20 , TTable, TColumns, TContext, TUnreify
23 , TTable, TColumns, TContext, TUnreify
21 )
24 )
@@ -33,7 +36,11 @@ import Prelude hiding ( null )
33
36
34-- rel8
37-- rel8
35import Rel8.FCF ( Eval, Exp )
38import Rel8.FCF ( Eval, Exp )
36−import Rel8.Kind.Algebra ( KnownAlgebra )
39+import Rel8.Kind.Algebra
40+ ( SAlgebra( SSum, SProduct )
41+ , KnownAlgebra, algebraSing
42+ )
43+import Rel8.Generic.Coherence ( GCoherent, gcoherence, gcongruence )
37import Rel8.Generic.Map ( GMap, GMappable, gmap, gunmap )
44import Rel8.Generic.Map ( GMap, GMappable, gmap, gunmap )
38import Rel8.Generic.Table
45import Rel8.Generic.Table
39 ( GGTable, GGColumns, GGContext, ggfromColumns, ggtoColumns
46 ( GGTable, GGColumns, GGContext, ggfromColumns, ggtoColumns
@@ -60,6 +67,7 @@ import Rel8.Schema.Reify
60 )
67 )
61import Rel8.Schema.Result
68import Rel8.Schema.Result
62 ( Col( R ), Result
69 ( Col( R ), Result
70+ , NotResult
63 , null, nullifier, unnullifier
71 , null, nullifier, unnullifier
64 , vectorizer, unvectorizer
72 , vectorizer, unvectorizer
65 )
73 )
@@ -98,6 +106,9 @@ class (HTable (Columns a), context ~ Context a) => Table context a | a -> contex
98
106
99 reify :: context :~: Reify ctx -> Unreify a -> a
107 reify :: context :~: Reify ctx -> Unreify a -> a
100 unreify :: context :~: Reify ctx -> a -> Unreify a
108 unreify :: context :~: Reify ctx -> a -> Unreify a
109+ coherence :: context :~: Reify ctx -> NotResult ctx -> Context (Unreify a) :~: ctx
110+ congruence :: context :~: Reify ctx -> NotResult ctx -> Columns a :~: Columns (Unreify a)
111+
101
112
102 type Columns a = Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))
113 type Columns a = Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))
103 type Context a = Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record a)))
114 type Context a = Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record a)))
@@ -169,6 +180,43 @@ class (HTable (Columns a), context ~ Context a) => Table context a | a -> contex
169 from .
180 from .
170 Record
181 Record
171
182
183+ default coherence ::
184+ ( KnownAlgebra (GAlgebra (Rep (Record a)))
185+ , GCoherent (TTable context) (Rep (Record a))
186+ , Context a ~ Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record a)))
187+ , Context (Unreify a) ~ Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record (Unreify a))))
188+ , Rep (Record (Unreify a)) ~ GMap TUnreify (Rep (Record a))
189+ )
190+ => context :~: Reify ctx -> NotResult ctx -> Context (Unreify a) :~: ctx
191+ coherence = case algebraSing @(GAlgebra (Rep (Record a))) of
192+ SSum -> notReify
193+ SProduct -> \proof abstract ->
194+ gcoherence
195+ @(TTable context)
196+ @(Rep (Record a))
197+ (Proxy @TContext)
198+ (Proxy @TUnreify)
199+ (\(_ :: _proxy x) -> coherence @context @x proof abstract)
200+
201+ default congruence ::
202+ ( KnownAlgebra (GAlgebra (Rep (Record a)))
203+ , GCoherent (TTable context) (Rep (Record a))
204+ , Context a ~ Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record a)))
205+ , Columns a ~ Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))
206+ , Columns (Unreify a) ~ Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record (Unreify a))))
207+ , Rep (Record (Unreify a)) ~ GMap TUnreify (Rep (Record a))
208+ )
209+ => context :~: Reify ctx -> NotResult ctx -> Columns a :~: Columns (Unreify a)
210+ congruence = case algebraSing @(GAlgebra (Rep (Record a))) of
211+ SSum -> notReify
212+ SProduct -> \proof abstract ->
213+ gcongruence
214+ @(TTable context)
215+ @(Rep (Record a))
216+ (Proxy @TColumns)
217+ (Proxy @TUnreify)
218+ (\(_ :: _proxy x) -> congruence @context @x proof abstract)
219+
172
220
173data TTable :: K.Context -> Type -> Exp Constraint
221data TTable :: K.Context -> Type -> Exp Constraint
174type instance Eval (TTable context a) = Table context a
222type instance Eval (TTable context a) = Table context a
@@ -213,6 +261,8 @@ instance HTable t => Table context (t (Col context)) where
213
261
214 reify Refl = hreify
262 reify Refl = hreify
215 unreify Refl = hunreify
263 unreify Refl = hunreify
264+ coherence Refl _ = Refl
265+ congruence Refl _ = Refl
216
266
217
267
218-- | Any context is trivially a table.
268-- | Any context is trivially a table.
@@ -226,6 +276,8 @@ instance KnownSpec spec => Table context (Col context spec) where
226
276
227 reify Refl = Reify
277 reify Refl = Reify
228 unreify Refl (Reify a) = a
278 unreify Refl (Reify a) = a
279+ coherence Refl _ = Refl
280+ congruence Refl _ = Refl
229
281
230
282
231instance Sql DBType a => Table Result (Identity a) where
283instance Sql DBType a => Table Result (Identity a) where
@@ -237,11 +289,15 @@ instance Sql DBType a => Table Result (Identity a) where
237
289
238 reify = notReify
290 reify = notReify
239 unreify = notReify
291 unreify = notReify
292+ coherence = notReify
293+ congruence = notReify
240
294
241
295
242−instance (Table Result a, Table Result b) => Table Result (Either a b) where
296+instance (context ~ Result, Table context a, Table context b) =>
297+ Table context (Either a b)
298+ where
243 type Columns (Either a b) = HEitherTable (Columns a) (Columns b)
299 type Columns (Either a b) = HEitherTable (Columns a) (Columns b)
244− type Context (Either a b) = Result
300+ type Context (Either a b) = Context a
245
301
246 toColumns = \case
302 toColumns = \case
247 Left table -> HEitherTable
303 Left table -> HEitherTable
@@ -262,18 +318,24 @@ instance (Table Result a, Table Result b) => Table Result (Either a b) where
262 where
318 where
263 err = error "Either.fromColumns: mismatch between tag and data"
319 err = error "Either.fromColumns: mismatch between tag and data"
264
320
321+ coherence = notReify
322+ congruence = notReify
265
323
324+
266−instance Table Result a => Table Result [a] where
325+instance (context ~ Result, Table context a) => Table context [a] where
267 type Columns [a] = HListTable (Columns a)
326 type Columns [a] = HListTable (Columns a)
268− type Context [a] = Result
327+ type Context [a] = Context a
269
328
270 toColumns = hvectorize vectorizer . fmap toColumns
329 toColumns = hvectorize vectorizer . fmap toColumns
271 fromColumns = fmap fromColumns . hunvectorize unvectorizer
330 fromColumns = fmap fromColumns . hunvectorize unvectorizer
272
331
332+ coherence = notReify
333+ congruence = notReify
334+
273
335
274−instance Table Result a => Table Result (Maybe a) where
336+instance (context ~ Result, Table context a) => Table context (Maybe a) where
275 type Columns (Maybe a) = HMaybeTable (Columns a)
337 type Columns (Maybe a) = HMaybeTable (Columns a)
276− type Context (Maybe a) = Result
338+ type Context (Maybe a) = Context a
277
339
278 toColumns = \case
340 toColumns = \case
279 Nothing -> HMaybeTable
341 Nothing -> HMaybeTable
@@ -291,18 +353,27 @@ instance Table Result a => Table Result (Maybe a) where
291 Nothing -> error "Maybe.fromColumns: mismatch between tag and data"
353 Nothing -> error "Maybe.fromColumns: mismatch between tag and data"
292 Just just -> fromColumns just
354 Just just -> fromColumns just
293
355
356+ coherence = notReify
357+ congruence = notReify
294
358
359+
295−instance Table Result a => Table Result (NonEmpty a) where
360+instance (context ~ Result, Table context a) => Table context (NonEmpty a)
361+ where
296 type Columns (NonEmpty a) = HNonEmptyTable (Columns a)
362 type Columns (NonEmpty a) = HNonEmptyTable (Columns a)
297− type Context (NonEmpty a) = Result
363+ type Context (NonEmpty a) = Context a
298
364
299 toColumns = hvectorize vectorizer . fmap toColumns
365 toColumns = hvectorize vectorizer . fmap toColumns
300 fromColumns = fmap fromColumns . hunvectorize unvectorizer
366 fromColumns = fmap fromColumns . hunvectorize unvectorizer
301
367
368+ coherence = notReify
369+ congruence = notReify
370+
302
371
303−instance (Table Result a, Table Result b) => Table Result (These a b) where
372+instance (context ~ Result, Table context a, Table context b) =>
373+ Table context (These a b)
374+ where
304 type Columns (These a b) = HTheseTable (Columns a) (Columns b)
375 type Columns (These a b) = HTheseTable (Columns a) (Columns b)
305− type Context (These a b) = Result
376+ type Context (These a b) = Context a
306
377
307 toColumns tables = HTheseTable
378 toColumns tables = HTheseTable
308 { hhereTag = hrelabel hhereTag
379 { hhereTag = hrelabel hhereTag
@@ -336,9 +407,11 @@ instance (Table Result a, Table Result b) => Table Result (These a b) where
336 , hjust = hrelabel hthere
407 , hjust = hrelabel hthere
337 }
408 }
338
409
410+ coherence = notReify
411+ congruence = notReify
412+
339
413
340−instance (Table context a, Table context b)
414+instance (Table context a, Table context b) => Table context (a, b)
341− => Table context (a, b)
342
415
343
416
344instance
417instance
src/Rel8/Table/Either.hs+10−2
@@ -24,10 +24,12 @@ where
24
24
25-- base
25-- base
26import Control.Applicative ( liftA2 )
26import Control.Applicative ( liftA2 )
27+import Control.Category ( id )
27import Data.Bifunctor ( Bifunctor, bimap )
28import Data.Bifunctor ( Bifunctor, bimap )
28import Data.Functor.Identity ( runIdentity )
29import Data.Functor.Identity ( runIdentity )
29import Data.Kind ( Type )
30import Data.Kind ( Type )
31+import Data.Type.Equality ( apply )
30−import Prelude hiding ( undefined )
32+import Prelude hiding ( id, undefined )
31
33
32-- rel8
34-- rel8
33import Rel8.Aggregate ( Col( A ), Aggregate )
35import Rel8.Aggregate ( Col( A ), Aggregate )
@@ -45,7 +47,7 @@ import Rel8.Schema.Name ( Col( N ), Name )
45import Rel8.Schema.Spec ( Spec( Spec ) )
47import Rel8.Schema.Spec ( Spec( Spec ) )
46import Rel8.Table
48import Rel8.Table
47 ( Table, Columns, Context, fromColumns, toColumns
49 ( Table, Columns, Context, fromColumns, toColumns
48− , reify, unreify
50+ , reify, unreify, coherence, congruence
49 )
51 )
50import Rel8.Table.Bool ( bool )
52import Rel8.Table.Bool ( bool )
51import Rel8.Table.Eq ( EqTable, eqTable )
53import Rel8.Table.Eq ( EqTable, eqTable )
@@ -139,6 +141,12 @@ instance
139 reify = liftA2 bimap reify reify
141 reify = liftA2 bimap reify reify
140 unreify = liftA2 bimap unreify unreify
142 unreify = liftA2 bimap unreify unreify
141
143
144+ coherence = coherence @context @a
145+ congruence proof abstract =
146+ id `apply`
147+ congruence @context @a proof abstract `apply`
148+ congruence @context @b proof abstract
149+
142
150
143instance
151instance
144 ( Nullifiable from, from ~ from'
152 ( Nullifiable from, from ~ from'
src/Rel8/Table/HKD.hs+4−2
@@ -68,8 +68,8 @@ import Rel8.Schema.Name ( Name )
68import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify, notReify )
68import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify, notReify )
69import Rel8.Schema.Result ( Result )
69import Rel8.Schema.Result ( Result )
70import Rel8.Table
70import Rel8.Table
71− ( Table, Columns, Context, Unreify
71+ ( Table, Columns, Context, fromColumns, toColumns
72− , fromColumns, toColumns, reify, unreify
72+ , Unreify, reify, unreify, coherence, congruence
73 , TTable, TColumns, TUnreify
73 , TTable, TColumns, TUnreify
74 )
74 )
75import Rel8.Table.Serialize ( ToExprs, fromResult, toResult )
75import Rel8.Table.Serialize ( ToExprs, fromResult, toResult )
@@ -150,6 +150,8 @@ instance HKDable a => Table Result (HKDT a) where
150 toColumns = (\(HKD a) -> a) . toHKD . (\(HKDT a) -> a)
150 toColumns = (\(HKD a) -> a) . toHKD . (\(HKDT a) -> a)
151 reify = notReify
151 reify = notReify
152 unreify = notReify
152 unreify = notReify
153+ coherence = notReify
154+ congruence = notReify
153
155
154
156
155instance
157instance
src/Rel8/Table/List.hs+25−10
@@ -16,14 +16,16 @@ module Rel8.Table.List
16where
16where
17
17
18-- base
18-- base
19+import Control.Category ( id )
19import Data.Functor.Identity ( Identity( Identity ) )
20import Data.Functor.Identity ( Identity( Identity ) )
20import Data.Kind ( Type )
21import Data.Kind ( Type )
21−import Data.Type.Equality ( (:~:)( Refl ) )
22+import Data.Type.Equality ( (:~:)( Refl ), apply )
22−import Prelude
23+import Prelude hiding ( id )
23
24
24-- rel8
25-- rel8
25import Rel8.Expr ( Expr, Col( E, unE ) )
26import Rel8.Expr ( Expr, Col( E, unE ) )
26import Rel8.Expr.Array ( sappend, sempty, slistOf )
27import Rel8.Expr.Array ( sappend, sempty, slistOf )
28+import Rel8.Schema.Context.Abstract ( Abstract, exclusivity, virtual )
27import Rel8.Schema.Dict ( Dict( Dict ) )
29import Rel8.Schema.Dict ( Dict( Dict ) )
28import Rel8.Schema.HTable.List ( HListTable )
30import Rel8.Schema.HTable.List ( HListTable )
29import Rel8.Schema.HTable.Vectorize ( happend, hempty, hvectorize )
31import Rel8.Schema.HTable.Vectorize ( happend, hempty, hvectorize )
@@ -34,7 +36,7 @@ import Rel8.Schema.Spec ( SSpec(..) )
34import Rel8.Schema.Reify ( hreify, hunreify )
36import Rel8.Schema.Reify ( hreify, hunreify )
35import Rel8.Table
37import Rel8.Table
36 ( Table, Context, Columns, fromColumns, toColumns
38 ( Table, Context, Columns, fromColumns, toColumns
37− , reify, unreify
39+ , reify, unreify, coherence, congruence
38 )
40 )
39import Rel8.Table.Alternative
41import Rel8.Table.Alternative
40 ( AltTable, (<|>:)
42 ( AltTable, (<|>:)
@@ -44,7 +46,6 @@ import Rel8.Table.Eq ( EqTable, eqTable )
44import Rel8.Table.Ord ( OrdTable, ordTable )
46import Rel8.Table.Ord ( OrdTable, ordTable )
45import Rel8.Table.Recontextualize ( Recontextualize )
47import Rel8.Table.Recontextualize ( Recontextualize )
46import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
48import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
47−import Rel8.Table.Unreify ( Unreifies )
48
49
49
50
50-- | A @ListTable@ value contains zero or more instances of @a@. You construct
51-- | A @ListTable@ value contains zero or more instances of @a@. You construct
@@ -54,7 +55,7 @@ newtype ListTable context a =
54 ListTable (HListTable (Columns a) (Col (Context a)))
55 ListTable (HListTable (Columns a) (Col (Context a)))
55
56
56
57
57−instance (Table context a, Unreifies context a, context ~ context') =>
58+instance (Table context a, Abstract context, context ~ context') =>
58 Table context' (ListTable context a)
59 Table context' (ListTable context a)
59 where
60 where
60 type Columns (ListTable context a) = HListTable (Columns a)
61 type Columns (ListTable context a) = HListTable (Columns a)
@@ -63,14 +64,28 @@ instance (Table context a, Unreifies context a, context ~ context') =>
63 fromColumns = ListTable
64 fromColumns = ListTable
64 toColumns (ListTable a) = a
65 toColumns (ListTable a) = a
65
66
66− reify Refl (ListTable a) = ListTable (hreify a)
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− unreify Refl (ListTable a) = ListTable (hunreify a)
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
68
83
69
84
70instance
85instance
71− ( Unreifies from a, from ~ from'
72− , Unreifies to b, to ~ to'
73− , Recontextualize from to a b
86+ ( Recontextualize from to a b
87+ , Abstract from, from ~ from'
88+ , Abstract to, to ~ to'
74 )
89 )
75 => Recontextualize from to (ListTable from' a) (ListTable to' b)
90 => Recontextualize from to (ListTable from' a) (ListTable to' b)
76
91
src/Rel8/Table/Maybe.hs+7−2
@@ -22,9 +22,11 @@ module Rel8.Table.Maybe
22where
22where
23
23
24-- base
24-- base
25+import Control.Category ( id )
25import Data.Functor.Identity ( runIdentity )
26import Data.Functor.Identity ( runIdentity )
26import Data.Kind ( Type )
27import Data.Kind ( Type )
28+import Data.Type.Equality ( apply )
27−import Prelude hiding ( null, undefined )
29+import Prelude hiding ( id, null, undefined )
28
30
29-- rel8
31-- rel8
30import Rel8.Aggregate ( Col( A ), Aggregate )
32import Rel8.Aggregate ( Col( A ), Aggregate )
@@ -44,7 +46,7 @@ import Rel8.Schema.Null ( Nullify, Nullity( Null, NotNull ), Sql, nullable )
44import Rel8.Schema.Spec ( Spec( Spec ) )
46import Rel8.Schema.Spec ( Spec( Spec ) )
45import Rel8.Table
47import Rel8.Table
46 ( Table, Columns, Context, fromColumns, toColumns
48 ( Table, Columns, Context, fromColumns, toColumns
47− , reify, unreify
49+ , coherence, congruence, reify, unreify
48 )
50 )
49import Rel8.Table.Alternative
51import Rel8.Table.Alternative
50 ( AltTable, (<|>:)
52 ( AltTable, (<|>:)
@@ -142,6 +144,9 @@ instance (Table context a, Nullifiable context, context ~ context') =>
142 reify = fmap fmap reify
144 reify = fmap fmap reify
143 unreify = fmap fmap unreify
145 unreify = fmap fmap unreify
144
146
147+ coherence = coherence @context @a
148+ congruence proof abstract = id `apply` congruence @context @a proof abstract
149+
145
150
146instance
151instance
147 ( Nullifiable from, from ~ from'
152 ( Nullifiable from, from ~ from'
src/Rel8/Table/NonEmpty.hs+25−10
@@ -16,15 +16,17 @@ module Rel8.Table.NonEmpty
16where
16where
17
17
18-- base
18-- base
19+import Control.Category ( id )
19import Data.Functor.Identity ( Identity( Identity ) )
20import Data.Functor.Identity ( Identity( Identity ) )
20import Data.Kind ( Type )
21import Data.Kind ( Type )
21import Data.List.NonEmpty ( NonEmpty )
22import Data.List.NonEmpty ( NonEmpty )
22−import Data.Type.Equality ( (:~:)( Refl ) )
23+import Data.Type.Equality ( (:~:)( Refl ), apply )
23−import Prelude
24+import Prelude hiding ( id )
24
25
25-- rel8
26-- rel8
26import Rel8.Expr ( Expr, Col( E, unE ) )
27import Rel8.Expr ( Expr, Col( E, unE ) )
27import Rel8.Expr.Array ( sappend1, snonEmptyOf )
28import Rel8.Expr.Array ( sappend1, snonEmptyOf )
29+import Rel8.Schema.Context.Abstract ( Abstract, exclusivity, virtual )
28import Rel8.Schema.Dict ( Dict( Dict ) )
30import Rel8.Schema.Dict ( Dict( Dict ) )
29import Rel8.Schema.HTable.NonEmpty ( HNonEmptyTable )
31import Rel8.Schema.HTable.NonEmpty ( HNonEmptyTable )
30import Rel8.Schema.HTable.Vectorize ( happend, hvectorize )
32import Rel8.Schema.HTable.Vectorize ( happend, hvectorize )
@@ -35,14 +37,13 @@ import Rel8.Schema.Reify ( hreify, hunreify )
35import Rel8.Schema.Spec ( SSpec(..) )
37import Rel8.Schema.Spec ( SSpec(..) )
36import Rel8.Table
38import Rel8.Table
37 ( Table, Context, Columns, fromColumns, toColumns
39 ( Table, Context, Columns, fromColumns, toColumns
38− , reify, unreify
40+ , reify, unreify, coherence, congruence
39 )
41 )
40import Rel8.Table.Alternative ( AltTable, (<|>:) )
42import Rel8.Table.Alternative ( AltTable, (<|>:) )
41import Rel8.Table.Eq ( EqTable, eqTable )
43import Rel8.Table.Eq ( EqTable, eqTable )
42import Rel8.Table.Ord ( OrdTable, ordTable )
44import Rel8.Table.Ord ( OrdTable, ordTable )
43import Rel8.Table.Recontextualize ( Recontextualize )
45import Rel8.Table.Recontextualize ( Recontextualize )
44import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
46import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
45−import Rel8.Table.Unreify ( Unreifies )
46
47
47
48
48-- | A @NonEmptyTable@ value contains one or more instances of @a@. You
49-- | A @NonEmptyTable@ value contains one or more instances of @a@. You
@@ -52,7 +53,7 @@ newtype NonEmptyTable context a =
52 NonEmptyTable (HNonEmptyTable (Columns a) (Col (Context a)))
53 NonEmptyTable (HNonEmptyTable (Columns a) (Col (Context a)))
53
54
54
55
55−instance (Table context a, Unreifies context a, context ~ context') =>
56+instance (Table context a, Abstract context, context ~ context') =>
56 Table context' (NonEmptyTable context a)
57 Table context' (NonEmptyTable context a)
57 where
58 where
58 type Columns (NonEmptyTable context a) = HNonEmptyTable (Columns a)
59 type Columns (NonEmptyTable context a) = HNonEmptyTable (Columns a)
@@ -61,14 +62,28 @@ instance (Table context a, Unreifies context a, context ~ context') =>
61 fromColumns = NonEmptyTable
62 fromColumns = NonEmptyTable
62 toColumns (NonEmptyTable a) = a
63 toColumns (NonEmptyTable a) = a
63
64
64− reify Refl (NonEmptyTable a) = NonEmptyTable (hreify a)
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− unreify Refl (NonEmptyTable a) = NonEmptyTable (hunreify a)
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
66
81
67
82
68instance
83instance
69− ( Unreifies from a, from ~ from'
70− , Unreifies to b, to ~ to'
71− , Recontextualize from to a b
84+ ( Recontextualize from to a b
85+ , Abstract from, from ~ from'
86+ , Abstract to, to ~ to'
72 )
87 )
73 => Recontextualize from to (NonEmptyTable from' a) (NonEmptyTable to' b)
88 => Recontextualize from to (NonEmptyTable from' a) (NonEmptyTable to' b)
74
89
src/Rel8/Table/Recontextualize.hs+33−1
@@ -14,7 +14,8 @@ where
14-- base
14-- base
15import Data.Functor.Identity ( Identity )
15import Data.Functor.Identity ( Identity )
16import Data.Kind ( Constraint, Type )
16import Data.Kind ( Constraint, Type )
17−import Prelude ()
17+import Data.List.NonEmpty ( NonEmpty)
18+import Prelude
18
19
19-- rel8
20-- rel8
20import Rel8.Schema.Context ( Col )
21import Rel8.Schema.Context ( Col )
@@ -26,6 +27,9 @@ import Rel8.Schema.Spec ( KnownSpec )
26import Rel8.Table ( Table, Congruent )
27import Rel8.Table ( Table, Congruent )
27import Rel8.Type ( DBType )
28import Rel8.Type ( DBType )
28
29
30+-- these
31+import Data.These ( These)
32+
29
33
30-- | @Recontextualize from to a b@ is evidence that the types @a@ and @b@ are
34-- | @Recontextualize from to a b@ is evidence that the types @a@ and @b@ are
31-- related, and that @b@ is the same type as @a@, but after changing the
35-- related, and that @b@ is the same type as @a@, but after changing the
@@ -54,6 +58,34 @@ instance KnownSpec spec => Recontextualize from to (Col from spec) (Col to spec)
54instance HTable t => Recontextualize from to (t (Col from)) (t (Col to))
58instance HTable t => Recontextualize from to (t (Col from)) (t (Col to))
55
59
56
60
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+
57instance
89instance
58 ( Recontextualize from to a1 b1
90 ( Recontextualize from to a1 b1
59 , Recontextualize from to a2 b2
91 , Recontextualize from to a2 b2
src/Rel8/Table/Rel8able.hs+4−1
@@ -41,7 +41,7 @@ import Rel8.Schema.Reify ( hreify, hunreify, UnwrapReify )
41import Rel8.Schema.Result ( Result )
41import Rel8.Schema.Result ( Result )
42import Rel8.Table
42import Rel8.Table
43 ( Table, Columns, Context, Congruent, fromColumns, toColumns
43 ( Table, Columns, Context, Congruent, fromColumns, toColumns
44− , Unreify, reify, unreify
44+ , Unreify, reify, unreify, coherence, congruence
45 )
45 )
46import Rel8.Schema.Spec.Constrain ( ConstrainSpec )
46import Rel8.Schema.Spec.Constrain ( ConstrainSpec )
47import Rel8.Table.ADT ( ADT( ADT ), ADTable, fromADT, toADT )
47import Rel8.Table.ADT ( ADT( ADT ), ADTable, fromADT, toADT )
@@ -72,6 +72,9 @@ instance (Rel8able t, Reifiable context) =>
72 SReify context -> case sReifiable context of
72 SReify context -> case sReifiable context of
73 Dict -> gunreify
73 Dict -> gunreify
74
74
75+ coherence Refl _ = Refl
76+ congruence Refl _ = Refl
77+
75
78
76instance
79instance
77 ( Rel8able t
80 ( Rel8able t
src/Rel8/Table/These.hs+10−2
@@ -27,10 +27,12 @@ where
27
27
28-- base
28-- base
29import Control.Applicative ( liftA2 )
29import Control.Applicative ( liftA2 )
30+import Control.Category ( id )
30import Data.Bifunctor ( Bifunctor, bimap )
31import Data.Bifunctor ( Bifunctor, bimap )
31import Data.Functor.Identity ( runIdentity )
32import Data.Functor.Identity ( runIdentity )
32import Data.Kind ( Type )
33import Data.Kind ( Type )
34+import Data.Type.Equality ( apply )
33−import Prelude hiding ( undefined )
35+import Prelude hiding ( id, undefined )
34
36
35-- rel8
37-- rel8
36import Rel8.Aggregate ( Aggregate )
38import Rel8.Aggregate ( Aggregate )
@@ -47,7 +49,7 @@ import qualified Rel8.Schema.Kind as K
47import Rel8.Schema.Name ( Name )
49import Rel8.Schema.Name ( Name )
48import Rel8.Table
50import Rel8.Table
49 ( Table, Columns, Context, fromColumns, toColumns
51 ( Table, Columns, Context, fromColumns, toColumns
50− , reify, unreify
52+ , coherence, congruence, reify, unreify
51 )
53 )
52import Rel8.Table.Eq ( EqTable, eqTable )
54import Rel8.Table.Eq ( EqTable, eqTable )
53import Rel8.Table.Maybe
55import Rel8.Table.Maybe
@@ -178,6 +180,12 @@ instance
178 reify = liftA2 bimap reify reify
180 reify = liftA2 bimap reify reify
179 unreify = liftA2 bimap unreify unreify
181 unreify = liftA2 bimap unreify unreify
180
182
183+ coherence = coherence @context @a
184+ congruence proof abstract =
185+ id `apply`
186+ congruence @context @a proof abstract `apply`
187+ congruence @context @b proof abstract
188+
181
189
182instance
190instance
183 ( Nullifiable from, from ~ from'
191 ( Nullifiable from, from ~ from'
src/Rel8/Table/Unreify.hsdeleted−102
@@ -1,102 +0,0 @@
1−{-# language DataKinds #-}
2−{-# language FlexibleContexts #-}
3−{-# language FlexibleInstances #-}
4−{-# language GADTs #-}
5−{-# language LambdaCase #-}
6−{-# language MultiParamTypeClasses #-}
7−{-# language QuantifiedConstraints #-}
8−{-# language RankNTypes #-}
9−{-# language StandaloneKindSignatures #-}
10−{-# language TypeFamilies #-}
11−{-# language UndecidableInstances #-}
12−
13−-- | This module implements some machinery for implementing methods of the
14−-- 'Table' class for a particular special (but important) class of polymorphic
15−-- @Table@ types.
16−--
17−-- This special case is characterised by a @newtype@ wrapper around a bare
18−-- 'HTable' which is constructed by applying a type family to the polymorphic
19−-- type variable.
20−--
21−-- Examples of this class of @Table@ include @ListTable@ and @NonEmptyTable@.
22−--
23−-- The tricky part about implementing @Table@ for these types is 'reify' and
24−-- 'unreify'. There is no guarantee in general that @'Unreify' a@ is itself
25−-- a @Table@, let alone a @Table@ with the same 'Columns' as @a@
26−-- (e.g., @Unreify (AColumn Result Bool) = Bool@, and @Bool@ is not a
27−-- @Table@)
28−
29−module Rel8.Table.Unreify
30− ( Unreifiable, Unreifiability(..), unreifiability
31− , Unreifies
32− )
33−where
34−
35−-- base
36−import Data.Kind ( Constraint, Type )
37−import Prelude ()
38−
39−-- rel8
40−import Rel8.Aggregate ( Aggregate )
41−import Rel8.Expr ( Expr )
42−import Rel8.Kind.Context ( SContext(..), Reifiable, sReifiable )
43−import Rel8.Schema.Dict ( Dict( Dict ) )
44−import qualified Rel8.Schema.Kind as K
45−import Rel8.Schema.Name ( Name )
46−import Rel8.Schema.Reify ( Reify )
47−import Rel8.Schema.Result ( Result )
48−import Rel8.Table ( Table, Context, Congruent, Unreify )
49−
50−
51−type Unreifies :: K.Context -> Type -> Constraint
52−type family Unreifies context a where
53− Unreifies (Reify context) a = Unreifier context a
54− Unreifies _ _ = ()
55−
56−
57−type Unreifiable :: Type -> Constraint
58−class
59− ( Context a ~ Reify Aggregate => Unreifier Aggregate a
60− , Context a ~ Reify Expr => Unreifier Expr a
61− , Context a ~ Reify Name => Unreifier Name a
62− , (forall ctx. (Context a ~ Reify (Reify ctx), Reifiable ctx) => Unreifier (Reify ctx) a)
63− )
64− => Unreifiable a
65−instance
66− ( Context a ~ Reify Aggregate => Unreifier Aggregate a
67− , Context a ~ Reify Expr => Unreifier Expr a
68− , Context a ~ Reify Name => Unreifier Name a
69− , (forall ctx. (Context a ~ Reify (Reify ctx), Reifiable ctx) => Unreifier (Reify ctx) a)
70− )
71− => Unreifiable a
72−
73−
74−type Unreifier :: K.Context -> Type -> Constraint
75−class
76− ( Table context (Unreify a)
77− , Congruent a (Unreify a)
78− )
79− => Unreifier context a
80−instance
81− ( Table context (Unreify a)
82− , Congruent a (Unreify a)
83− )
84− => Unreifier context a
85−
86−
87−type Unreifiability :: K.Context -> Type -> Type
88−data Unreifiability context a where
89− UResult :: Unreifiability Result a
90− Unreifiability :: Unreifier context a
91− => SContext context -> Unreifiability context a
92−
93−
94−unreifiability :: (Context a ~ Reify context, Unreifiable a)
95− => SContext context -> Unreifiability context a
96−unreifiability = \case
97− SAggregate -> Unreifiability SAggregate
98− SExpr -> Unreifiability SExpr
99− SName -> Unreifiability SName
100− SResult -> UResult
101− SReify context -> case sReifiable context of
102− Dict -> Unreifiability (SReify context)