git.iko.soy/rel8
on master help sign in
Get rid of Rel8.Table.Unreify and all remaining uses of QuantifiedConstraints (#103)

But we need more proofs

commit991998ab5dc8f260d48fd112c888b8c5f5039132 authorShane <shane.obrien@circuithub.com> dateMon 5 Jul 2021, 02:32 (5 years ago) parent707a36a
27 files changed+645−221
compare with master
unifiedsplit
rel8.cabal+2−1 src/Rel8/Aggregate.hs+3−1 src/Rel8/Column.hs+20−6 src/Rel8/Column/ADT.hs+20−2 src/Rel8/Column/Either.hs+33−3 src/Rel8/Column/Lift.hs+19−2 src/Rel8/Column/List.hs+52−25 src/Rel8/Column/Maybe.hs+21−3 src/Rel8/Column/NonEmpty.hs+51−25 src/Rel8/Column/These.hs+33−3 src/Rel8/Expr.hs+4−1 src/Rel8/Generic/Coherence.hs+79 src/Rel8/Schema/Context/Abstract.hs+80 src/Rel8/Schema/HTable/Nullify.hs−1 src/Rel8/Schema/HTable/Vectorize.hs−1 src/Rel8/Schema/Name.hs+4−1 src/Rel8/Schema/Result.hs+19 src/Rel8/Table.hs+87−14 src/Rel8/Table/Either.hs+10−2 src/Rel8/Table/HKD.hs+4−2 src/Rel8/Table/List.hs+25−10 src/Rel8/Table/Maybe.hs+7−2 src/Rel8/Table/NonEmpty.hs+25−10 src/Rel8/Table/Recontextualize.hs+33−1 src/Rel8/Table/Rel8able.hs+4−1 src/Rel8/Table/These.hs+10−2 src/Rel8/Table/Unreify.hs−102
rel8.cabal+2−1
@@ -81,6 +81,7 @@ library
8181 Rel8.Kind.Algebra
8282 Rel8.Kind.Context
8383
84+ Rel8.Generic.Coherence
8485 Rel8.Generic.Construction
8586 Rel8.Generic.Construction.ADT
8687 Rel8.Generic.Construction.Record
@@ -114,6 +115,7 @@ library
114115 Rel8.Query.Values
115116
116117 Rel8.Schema.Context
118+ Rel8.Schema.Context.Abstract
117119 Rel8.Schema.Context.Nullify
118120 Rel8.Schema.Dict
119121 Rel8.Schema.HTable
@@ -164,7 +166,6 @@ library
164166 Rel8.Table.Serialize
165167 Rel8.Table.These
166168 Rel8.Table.Undefined
167− Rel8.Table.Unreify
168169
169170 Rel8.Type
170171 Rel8.Type.Array
src/Rel8/Aggregate.hs+3−1
@@ -41,7 +41,7 @@ import Rel8.Schema.Result ( Result )
4141import Rel8.Schema.Spec ( Spec( Spec ) )
4242import Rel8.Table
4343 ( Table, Columns, Context, fromColumns, toColumns
44− , reify, unreify
44+ , reify, unreify, coherence, congruence
4545 )
4646import Rel8.Table.Recontextualize ( Recontextualize )
4747import Rel8.Type ( DBType )
@@ -73,6 +73,8 @@ instance Sql DBType a => Table Aggregate (Aggregate a) where
7373
7474 reify = notReify
7575 unreify = notReify
76+ coherence = notReify
77+ congruence = notReify
7678
7779
7880instance Sql DBType a =>
src/Rel8/Column.hs+20−6
@@ -2,7 +2,9 @@
22{-# language FlexibleContexts #-}
33{-# language LambdaCase #-}
44{-# language MultiParamTypeClasses #-}
5+{-# language ScopedTypeVariables #-}
56{-# language StandaloneKindSignatures #-}
7+{-# language TypeApplications #-}
68{-# language TypeFamilies #-}
79
810module Rel8.Column
@@ -13,6 +15,7 @@ where
1315
1416-- base
1517import Data.Kind ( Type )
18+import Data.Type.Equality ( (:~:)( Refl ) )
1619import Prelude
1720
1821-- rel8
@@ -25,11 +28,11 @@ import qualified Rel8.Schema.Kind as K
2528import Rel8.Schema.Name ( Name(..), Col( N ) )
2629import Rel8.Schema.Null ( Sql )
2730import Rel8.Schema.Reify ( Reify, Col(..) )
28−import Rel8.Schema.Result ( Col( R ), Result )
31+import Rel8.Schema.Result ( Col( R ), Result, absurd )
2932import Rel8.Schema.Spec ( Spec( Spec ) )
3033import Rel8.Table
3134 ( Table, Columns, Context, fromColumns, toColumns
32− , Unreify, reify, unreify
35+ , Unreify, reify, unreify, coherence, congruence
3336 )
3437import Rel8.Table.Recontextualize ( Recontextualize )
3538import Rel8.Type ( DBType )
@@ -63,11 +66,22 @@ instance (Reifiable context, Sql DBType a) =>
6366 reify _ = AColumn
6467 unreify _ (AColumn a) = a
6568
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
6675
67−instance
68− ( Reifiable context, Reifiable context'
69− , Sql DBType a
70− ) =>
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) =>
7185 Recontextualize
7286 (Reify context)
7387 (Reify context')
src/Rel8/Column/ADT.hs+20−2
@@ -1,7 +1,9 @@
11{-# language DataKinds #-}
22{-# language LambdaCase #-}
33{-# language MultiParamTypeClasses #-}
4+{-# language ScopedTypeVariables #-}
45{-# language StandaloneKindSignatures #-}
6+{-# language TypeApplications #-}
57{-# language TypeFamilies #-}
68{-# language UndecidableInstances #-}
79
@@ -12,6 +14,7 @@ where
1214
1315-- base
1416import Data.Kind ( Type )
17+import Data.Type.Equality ( (:~:)( Refl ) )
1518import Prelude
1619
1720-- rel8
@@ -20,12 +23,13 @@ import Rel8.Kind.Context ( SContext(..), Reifiable, contextSing )
2023import Rel8.Schema.Context ( Col )
2124import qualified Rel8.Schema.Kind as K
2225import Rel8.Schema.Reify ( Reify, hreify, hunreify )
23−import Rel8.Schema.Result ( Result )
26+import Rel8.Schema.Result ( Result, absurd )
2427import Rel8.Table
2528 ( Table, Columns, Context, fromColumns, toColumns
26− , Unreify, reify, unreify
29+ , Unreify, reify, unreify, coherence, congruence
2730 )
2831import Rel8.Table.ADT ( ADT( ADT ), ADTable, fromADT, toADT )
32+import Rel8.Table.Rel8able ()
2933import Rel8.Table.Recontextualize ( Recontextualize )
3034
3135
@@ -52,6 +56,20 @@ instance (ADTable t, Reifiable context) =>
5256 reify _ = AHADT
5357 unreify _ (AHADT a) = a
5458
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+
5573
5674instance
5775 ( Reifiable context, Reifiable context'
src/Rel8/Column/Either.hs+33−3
@@ -2,7 +2,9 @@
22{-# language FlexibleContexts #-}
33{-# language LambdaCase #-}
44{-# language MultiParamTypeClasses #-}
5+{-# language ScopedTypeVariables #-}
56{-# language StandaloneKindSignatures #-}
7+{-# language TypeApplications #-}
68{-# language TypeFamilyDependencies #-}
79{-# language UndecidableInstances #-}
810
@@ -13,9 +15,11 @@ where
1315
1416-- base
1517import Control.Applicative ( liftA2 )
18+import Control.Category ( id )
1619import Data.Bifunctor ( Bifunctor, bimap )
1720import Data.Kind ( Type )
18−import Prelude
21+import Data.Type.Equality ( (:~:)( Refl ), apply )
22+import Prelude hiding ( id )
1923
2024-- rel8
2125import Rel8.Aggregate ( Aggregate )
@@ -26,10 +30,10 @@ import Rel8.Schema.HTable.Either ( HEitherTable )
2630import qualified Rel8.Schema.Kind as K
2731import Rel8.Schema.Name ( Name(..) )
2832import Rel8.Schema.Reify ( Reify, hreify, hunreify )
29−import Rel8.Schema.Result ( Result )
33+import Rel8.Schema.Result ( Result, absurd )
3034import Rel8.Table
3135 ( Table, Columns, Context, fromColumns, toColumns
32− , Unreify, reify, unreify
36+ , Unreify, reify, unreify, coherence, congruence
3337 )
3438import Rel8.Table.Either ( EitherTable )
3539import Rel8.Table.Recontextualize ( Recontextualize )
@@ -71,6 +75,32 @@ instance (Reifiable context, Table (Reify context) a, Table (Reify context) b)
7175 reify proof = liftA2 bimap reify reify proof . AHEither
7276 unreify proof = (\(AHEither a) -> a) . liftA2 bimap unreify unreify proof
7377
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+
74104
75105instance
76106 ( Reifiable context, Reifiable context'
src/Rel8/Column/Lift.hs+19−2
@@ -1,7 +1,9 @@
11{-# language DataKinds #-}
22{-# language LambdaCase #-}
33{-# language MultiParamTypeClasses #-}
4+{-# language ScopedTypeVariables #-}
45{-# language StandaloneKindSignatures #-}
6+{-# language TypeApplications #-}
57{-# language TypeFamilies #-}
68
79module Rel8.Column.Lift
@@ -11,6 +13,7 @@ where
1113
1214-- base
1315import Data.Kind ( Type )
16+import Data.Type.Equality ( (:~:)( Refl ) )
1417import Prelude
1518
1619-- rel8
@@ -19,10 +22,10 @@ import Rel8.Kind.Context ( Reifiable(..), SContext(..) )
1922import Rel8.Schema.Context ( Col )
2023import qualified Rel8.Schema.Kind as K
2124import Rel8.Schema.Reify ( Reify, hreify, hunreify )
22−import Rel8.Schema.Result ( Result )
25+import Rel8.Schema.Result ( Result, absurd )
2326import Rel8.Table
2427 ( Table, Columns, Context, fromColumns, toColumns
25− , Unreify, reify, unreify
28+ , Unreify, reify, unreify, coherence, congruence
2629 )
2730import Rel8.Table.Rel8able ()
2831import Rel8.Table.HKD ( HKD( HKD ), HKDable, fromHKD, toHKD )
@@ -54,6 +57,20 @@ instance (Reifiable context, HKDable a) =>
5457 reify _ = ALift
5558 unreify _ (ALift a) = a
5659
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+
5774
5875instance (Reifiable context, Reifiable context', HKDable a) =>
5976 Recontextualize
src/Rel8/Column/List.hs+52−25
@@ -2,7 +2,10 @@
22{-# language FlexibleContexts #-}
33{-# language LambdaCase #-}
44{-# language MultiParamTypeClasses #-}
5+{-# language RankNTypes #-}
6+{-# language ScopedTypeVariables #-}
57{-# language StandaloneKindSignatures #-}
8+{-# language TypeApplications #-}
69{-# language TypeFamilyDependencies #-}
710{-# language UndecidableInstances #-}
811
@@ -12,27 +15,28 @@ module Rel8.Column.List
1215where
1316
1417-- base
18+import Control.Category ( id )
1519import Data.Kind ( Type )
16−import Data.Type.Equality ( (:~:)( Refl ) )
17−import Prelude
20+import Data.Type.Equality ( (:~:)( Refl ), apply )
21+import Prelude hiding ( id )
1822
1923-- rel8
2024import Rel8.Aggregate ( Aggregate )
2125import Rel8.Expr ( Expr )
2226import Rel8.Kind.Context ( SContext(..), Reifiable( contextSing ) )
2327import Rel8.Schema.Context ( Col )
28+import Rel8.Schema.Context.Abstract ( exclusivity, virtualOrResult )
2429import Rel8.Schema.HTable.List ( HListTable )
2530import qualified Rel8.Schema.Kind as K
2631import Rel8.Schema.Name ( Name )
2732import Rel8.Schema.Reify ( Reify, hreify, hunreify )
28−import Rel8.Schema.Result ( Result )
33+import Rel8.Schema.Result ( Result, absurd )
2934import Rel8.Table
3035 ( Table, Columns, Congruent, Context, fromColumns, toColumns
31− , Unreify, reify, unreify
36+ , Unreify, reify, unreify, coherence, congruence
3237 )
3338import Rel8.Table.List ( ListTable( ListTable ) )
3439import Rel8.Table.Recontextualize ( Recontextualize )
35−import Rel8.Table.Unreify ( Unreifiability(..), Unreifiable, unreifiability )
3640
3741
3842-- | Nest a list within a 'Rel8able'. @HList f a@ will produce a 'ListTable'
@@ -50,7 +54,7 @@ type AHList :: K.Context -> Type -> Type
5054newtype AHList context a = AHList (HList context a)
5155
5256
53−instance (Reifiable context, Unreifiable a, Table (Reify context) a) =>
57+instance (Reifiable context, Table (Reify context) a) =>
5458 Table (Reify context) (AHList context a)
5559 where
5660 type Context (AHList context a) = Reify context
@@ -60,13 +64,26 @@ instance (Reifiable context, Unreifiable a, Table (Reify context) a) =>
6064 fromColumns = sfromColumnsList contextSing
6165 toColumns = stoColumnsList contextSing
6266
63− reify _ = sreifyList (unreifiability contextSing)
64− unreify _ = sunreifyList (unreifiability contextSing)
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
6583
6684
6785instance
6886 ( Reifiable context, Reifiable context'
69− , Unreifiable a, Unreifiable a'
7087 , Recontextualize (Reify context) (Reify context') a a'
7188 )
7289 => Recontextualize
@@ -123,23 +140,33 @@ stoColumnsList = \case
123140 (\(AHList a) -> a)
124141
125142
126−sreifyList :: Table (Reify context) a
127− => Unreifiability context a
143+sreifyList :: forall context a. Table (Reify context) a
144+ => SContext context
128145 -> HList context (Unreify a)
129146 -> AHList context a
130−sreifyList = \case
131− UResult -> AHList . fmap (reify Refl)
132− Unreifiability context ->
133− smapList context (reify Refl) hreify .
134− AHList
135−
136−
137−sunreifyList :: Table (Reify context) a
138− => Unreifiability 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
139161 -> AHList context a
140162 -> HList context (Unreify a)
141−sunreifyList = \case
142− UResult -> fmap (unreify Refl) . (\(AHList a) -> a)
143− Unreifiability context ->
144− (\(AHList a) -> a) .
145− smapList context (unreify Refl) hunreify
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+21−3
@@ -3,7 +3,9 @@
33{-# language GADTs #-}
44{-# language LambdaCase #-}
55{-# language MultiParamTypeClasses #-}
6+{-# language ScopedTypeVariables #-}
67{-# language StandaloneKindSignatures #-}
8+{-# language TypeApplications #-}
79{-# language TypeFamilyDependencies #-}
810{-# language UndecidableInstances #-}
911
@@ -13,8 +15,10 @@ module Rel8.Column.Maybe
1315where
1416
1517-- base
18+import Control.Category ( id )
1619import Data.Kind ( Type )
17−import Prelude
20+import Data.Type.Equality ( (:~:)( Refl ), apply )
21+import Prelude hiding ( id )
1822
1923-- rel8
2024import Rel8.Aggregate ( Aggregate )
@@ -25,10 +29,10 @@ import Rel8.Schema.HTable.Maybe ( HMaybeTable )
2529import qualified Rel8.Schema.Kind as K
2630import Rel8.Schema.Name ( Name )
2731import Rel8.Schema.Reify ( Reify, hreify, hunreify )
28−import Rel8.Schema.Result ( Result )
32+import Rel8.Schema.Result ( Result, absurd )
2933import Rel8.Table
3034 ( Table, Columns, Context, fromColumns, toColumns
31− , Unreify, reify, unreify
35+ , Unreify, reify, unreify, coherence, congruence
3236 )
3337import Rel8.Table.Maybe ( MaybeTable )
3438import Rel8.Table.Recontextualize ( Recontextualize )
@@ -66,6 +70,20 @@ instance (Reifiable context, Table (Reify context) a) =>
6670 reify proof = fmap fmap reify proof . AHMaybe
6771 unreify proof = (\(AHMaybe a) -> a) . fmap fmap unreify proof
6872
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+
6987
7088instance
7189 ( Reifiable context, Reifiable context'
src/Rel8/Column/NonEmpty.hs+51−25
@@ -2,7 +2,9 @@
22{-# language FlexibleContexts #-}
33{-# language LambdaCase #-}
44{-# language MultiParamTypeClasses #-}
5+{-# language ScopedTypeVariables #-}
56{-# language StandaloneKindSignatures #-}
7+{-# language TypeApplications #-}
68{-# language TypeFamilyDependencies #-}
79{-# language UndecidableInstances #-}
810
@@ -12,28 +14,29 @@ module Rel8.Column.NonEmpty
1214where
1315
1416-- base
17+import Control.Category ( id )
1518import Data.Kind ( Type )
1619import Data.List.NonEmpty ( NonEmpty )
17−import Data.Type.Equality ( (:~:)( Refl ) )
18−import Prelude
20+import Data.Type.Equality ( (:~:)( Refl ), apply )
21+import Prelude hiding ( id )
1922
2023-- rel8
2124import Rel8.Aggregate ( Aggregate )
2225import Rel8.Expr ( Expr )
2326import Rel8.Kind.Context ( SContext(..), Reifiable( contextSing ) )
2427import Rel8.Schema.Context ( Col )
28+import Rel8.Schema.Context.Abstract ( exclusivity, virtualOrResult )
2529import Rel8.Schema.HTable.NonEmpty ( HNonEmptyTable )
2630import qualified Rel8.Schema.Kind as K
2731import Rel8.Schema.Name ( Name )
2832import Rel8.Schema.Reify ( Reify, hreify, hunreify )
29−import Rel8.Schema.Result ( Result )
33+import Rel8.Schema.Result ( Result, absurd )
3034import Rel8.Table
3135 ( Table, Columns, Congruent, Context, fromColumns, toColumns
32− , Unreify, reify, unreify
36+ , Unreify, reify, unreify, coherence, congruence
3337 )
3438import Rel8.Table.NonEmpty ( NonEmptyTable( NonEmptyTable ) )
3539import Rel8.Table.Recontextualize ( Recontextualize )
36−import Rel8.Table.Unreify ( Unreifiability(..), Unreifiable, unreifiability )
3740
3841
3942-- | Nest a 'NonEmpty' list within a 'Rel8able'. @HNonEmpty f a@ will produce a
@@ -52,7 +55,7 @@ type AHNonEmpty :: K.Context -> Type -> Type
5255newtype AHNonEmpty context a = AHNonEmpty (HNonEmpty context a)
5356
5457
55−instance (Reifiable context, Unreifiable a, Table (Reify context) a) =>
58+instance (Reifiable context, Table (Reify context) a) =>
5659 Table (Reify context) (AHNonEmpty context a)
5760 where
5861 type Context (AHNonEmpty context a) = Reify context
@@ -62,13 +65,26 @@ instance (Reifiable context, Unreifiable a, Table (Reify context) a) =>
6265 fromColumns = sfromColumnsNonEmpty contextSing
6366 toColumns = stoColumnsNonEmpty contextSing
6467
65− reify _ = sreifyNonEmpty (unreifiability contextSing)
66− unreify _ = sunreifyNonEmpty (unreifiability contextSing)
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
6784
6885
6986instance
7087 ( Reifiable context, Reifiable context'
71− , Unreifiable a, Unreifiable a'
7288 , Recontextualize (Reify context) (Reify context') a a'
7389 )
7490 => Recontextualize
@@ -126,23 +142,33 @@ stoColumnsNonEmpty = \case
126142 (\(AHNonEmpty a) -> a)
127143
128144
129−sreifyNonEmpty :: Table (Reify context) a
130− => Unreifiability context a
145+sreifyNonEmpty :: forall context a. Table (Reify context) a
146+ => SContext context
131147 -> HNonEmpty context (Unreify a)
132148 -> AHNonEmpty context a
133−sreifyNonEmpty = \case
134− UResult -> AHNonEmpty . fmap (reify Refl)
135− Unreifiability context ->
136− smapNonEmpty context (reify Refl) hreify .
137− AHNonEmpty
138−
139−
140−sunreifyNonEmpty :: Table (Reify context) a
141− => Unreifiability 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
142163 -> AHNonEmpty context a
143164 -> HNonEmpty context (Unreify a)
144−sunreifyNonEmpty = \case
145− UResult -> fmap (unreify Refl) . (\(AHNonEmpty a) -> a)
146− Unreifiability context ->
147− (\(AHNonEmpty a) -> a) .
148− smapNonEmpty context (unreify Refl) hunreify
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+33−3
@@ -3,7 +3,9 @@
33{-# language GADTs #-}
44{-# language LambdaCase #-}
55{-# language MultiParamTypeClasses #-}
6+{-# language ScopedTypeVariables #-}
67{-# language StandaloneKindSignatures #-}
8+{-# language TypeApplications #-}
79{-# language TypeFamilyDependencies #-}
810{-# language UndecidableInstances #-}
911
@@ -14,9 +16,11 @@ where
1416
1517-- base
1618import Control.Applicative ( liftA2 )
19+import Control.Category ( id )
1720import Data.Bifunctor ( Bifunctor, bimap )
1821import Data.Kind ( Type )
19−import Prelude
22+import Data.Type.Equality ( (:~:)( Refl ), apply )
23+import Prelude hiding ( id )
2024
2125-- rel8
2226import Rel8.Aggregate ( Aggregate )
@@ -27,10 +31,10 @@ import Rel8.Schema.HTable.These ( HTheseTable )
2731import qualified Rel8.Schema.Kind as K
2832import Rel8.Schema.Name ( Name )
2933import Rel8.Schema.Reify ( Reify, hreify, hunreify )
30−import Rel8.Schema.Result ( Result )
34+import Rel8.Schema.Result ( Result, absurd )
3135import Rel8.Table
3236 ( Table, Columns, Context, fromColumns, toColumns
33− , Unreify, reify, unreify
37+ , Unreify, reify, unreify, coherence, congruence
3438 )
3539import Rel8.Table.Recontextualize ( Recontextualize )
3640import Rel8.Table.These ( TheseTable )
@@ -75,6 +79,32 @@ instance (Reifiable context, Table (Reify context) a, Table (Reify context) b)
7579 reify proof = liftA2 bimap reify reify proof . AHThese
7680 unreify proof = (\(AHThese a) -> a) . liftA2 bimap unreify unreify proof
7781
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+
78108
79109instance
80110 ( Reifiable context, Reifiable context'
src/Rel8/Expr.hs+4−1
@@ -45,7 +45,8 @@ import Rel8.Schema.Reify ( notReify )
4545import Rel8.Schema.Result ( Result )
4646import Rel8.Schema.Spec ( Spec( Spec ) )
4747import Rel8.Table
48− ( Table, Columns, Context, fromColumns, toColumns, reify, unreify
48+ ( Table, Columns, Context, fromColumns, toColumns
49+ , reify, unreify, coherence, congruence
4950 )
5051import Rel8.Table.Recontextualize ( Recontextualize )
5152import Rel8.Type ( DBType )
@@ -138,6 +139,8 @@ instance Sql DBType a => Table Expr (Expr a) where
138139 fromColumns (HType (E a)) = a
139140 reify = notReify
140141 unreify = notReify
142+ coherence = notReify
143+ congruence = notReify
141144
142145
143146instance 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 @@
88{-# language LambdaCase #-}
99{-# language MultiParamTypeClasses #-}
1010{-# language NamedFieldPuns #-}
11−{-# language QuantifiedConstraints #-}
1211{-# language RankNTypes #-}
1312{-# language RecordWildCards #-}
1413{-# language ScopedTypeVariables #-}
src/Rel8/Schema/HTable/Vectorize.hs−1
@@ -10,7 +10,6 @@
1010{-# language LambdaCase #-}
1111{-# language MultiParamTypeClasses #-}
1212{-# language NamedFieldPuns #-}
13−{-# language QuantifiedConstraints #-}
1413{-# language RankNTypes #-}
1514{-# language RecordWildCards #-}
1615{-# language ScopedTypeVariables #-}
src/Rel8/Schema/Name.hs+4−1
@@ -34,7 +34,8 @@ import Rel8.Schema.Reify ( notReify )
3434import Rel8.Schema.Result ( Result )
3535import Rel8.Schema.Spec ( Spec( Spec ) )
3636import Rel8.Table
37− ( Table, Columns, Context, fromColumns, toColumns, reify, unreify
37+ ( Table, Columns, Context, fromColumns, toColumns
38+ , reify, unreify, coherence, congruence
3839 )
3940import Rel8.Table.Recontextualize ( Recontextualize )
4041import Rel8.Type ( DBType )
@@ -64,6 +65,8 @@ instance Sql DBType a => Table Name (Name a) where
6465 fromColumns (HType (N a)) = a
6566 reify = notReify
6667 unreify = notReify
68+ coherence = notReify
69+ congruence = notReify
6770
6871
6972instance Sql DBType a => Recontextualize Expr Name (Expr a) (Name a)
src/Rel8/Schema/Result.hs+19
@@ -1,17 +1,21 @@
11{-# language DataKinds #-}
2+{-# language EmptyCase #-}
23{-# language GADTs #-}
4+{-# language LambdaCase #-}
35{-# language NamedFieldPuns #-}
46{-# language StandaloneKindSignatures #-}
57{-# language TypeFamilies #-}
68
79module Rel8.Schema.Result
810 ( Col( R, unR ), Result
11+ , NotResult( NotResult ), absurd
912 , null, nullifier, unnullifier
1013 , vectorizer, unvectorizer
1114 )
1215where
1316
1417-- base
18+import Data.Kind ( Type )
1519import Prelude hiding ( null )
1620
1721-- rel8
@@ -34,6 +38,21 @@ instance Interpretation Result where
3438 R :: {unR :: !a} -> Col Result ('Spec a)
3539
3640
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+
3756null :: Col Result ('Spec (Maybe a))
3857null = R Nothing
3958
src/Rel8/Table.hs+87−14
@@ -15,7 +15,10 @@
1515{-# language UndecidableInstances #-}
1616
1717module Rel8.Table
18− ( Table (Columns, Context, Unreify, toColumns, fromColumns, reify, unreify)
18+ ( Table
19+ ( Columns, Context, toColumns, fromColumns
20+ , Unreify, reify, unreify, coherence, congruence
21+ )
1922 , Congruent
2023 , TTable, TColumns, TContext, TUnreify
2124 )
@@ -33,7 +36,11 @@ import Prelude hiding ( null )
3336
3437-- rel8
3538import 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 )
3744import Rel8.Generic.Map ( GMap, GMappable, gmap, gunmap )
3845import Rel8.Generic.Table
3946 ( GGTable, GGColumns, GGContext, ggfromColumns, ggtoColumns
@@ -60,6 +67,7 @@ import Rel8.Schema.Reify
6067 )
6168import Rel8.Schema.Result
6269 ( Col( R ), Result
70+ , NotResult
6371 , null, nullifier, unnullifier
6472 , vectorizer, unvectorizer
6573 )
@@ -98,6 +106,9 @@ class (HTable (Columns a), context ~ Context a) => Table context a | a -> contex
98106
99107 reify :: context :~: Reify ctx -> Unreify a -> a
100108 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+
101112
102113 type Columns a = Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))
103114 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
169180 from .
170181 Record
171182
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+
172220
173221data TTable :: K.Context -> Type -> Exp Constraint
174222type instance Eval (TTable context a) = Table context a
@@ -213,6 +261,8 @@ instance HTable t => Table context (t (Col context)) where
213261
214262 reify Refl = hreify
215263 unreify Refl = hunreify
264+ coherence Refl _ = Refl
265+ congruence Refl _ = Refl
216266
217267
218268-- | Any context is trivially a table.
@@ -226,6 +276,8 @@ instance KnownSpec spec => Table context (Col context spec) where
226276
227277 reify Refl = Reify
228278 unreify Refl (Reify a) = a
279+ coherence Refl _ = Refl
280+ congruence Refl _ = Refl
229281
230282
231283instance Sql DBType a => Table Result (Identity a) where
@@ -237,11 +289,15 @@ instance Sql DBType a => Table Result (Identity a) where
237289
238290 reify = notReify
239291 unreify = notReify
292+ coherence = notReify
293+ congruence = notReify
240294
241295
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
243299 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
245301
246302 toColumns = \case
247303 Left table -> HEitherTable
@@ -262,18 +318,24 @@ instance (Table Result a, Table Result b) => Table Result (Either a b) where
262318 where
263319 err = error "Either.fromColumns: mismatch between tag and data"
264320
321+ coherence = notReify
322+ congruence = notReify
265323
266−instance Table Result a => Table Result [a] where
324+
325+instance (context ~ Result, Table context a) => Table context [a] where
267326 type Columns [a] = HListTable (Columns a)
268− type Context [a] = Result
327+ type Context [a] = Context a
269328
270329 toColumns = hvectorize vectorizer . fmap toColumns
271330 fromColumns = fmap fromColumns . hunvectorize unvectorizer
272331
332+ coherence = notReify
333+ congruence = notReify
334+
273335
274−instance Table Result a => Table Result (Maybe a) where
336+instance (context ~ Result, Table context a) => Table context (Maybe a) where
275337 type Columns (Maybe a) = HMaybeTable (Columns a)
276− type Context (Maybe a) = Result
338+ type Context (Maybe a) = Context a
277339
278340 toColumns = \case
279341 Nothing -> HMaybeTable
@@ -291,18 +353,27 @@ instance Table Result a => Table Result (Maybe a) where
291353 Nothing -> error "Maybe.fromColumns: mismatch between tag and data"
292354 Just just -> fromColumns just
293355
356+ coherence = notReify
357+ congruence = notReify
294358
295−instance Table Result a => Table Result (NonEmpty a) where
359+
360+instance (context ~ Result, Table context a) => Table context (NonEmpty a)
361+ where
296362 type Columns (NonEmpty a) = HNonEmptyTable (Columns a)
297− type Context (NonEmpty a) = Result
363+ type Context (NonEmpty a) = Context a
298364
299365 toColumns = hvectorize vectorizer . fmap toColumns
300366 fromColumns = fmap fromColumns . hunvectorize unvectorizer
301367
368+ coherence = notReify
369+ congruence = notReify
370+
302371
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
304375 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
306377
307378 toColumns tables = HTheseTable
308379 { hhereTag = hrelabel hhereTag
@@ -336,9 +407,11 @@ instance (Table Result a, Table Result b) => Table Result (These a b) where
336407 , hjust = hrelabel hthere
337408 }
338409
410+ coherence = notReify
411+ congruence = notReify
412+
339413
340−instance (Table context a, Table context b)
341− => Table context (a, b)
414+instance (Table context a, Table context b) => Table context (a, b)
342415
343416
344417instance
src/Rel8/Table/Either.hs+10−2
@@ -24,10 +24,12 @@ where
2424
2525-- base
2626import Control.Applicative ( liftA2 )
27+import Control.Category ( id )
2728import Data.Bifunctor ( Bifunctor, bimap )
2829import Data.Functor.Identity ( runIdentity )
2930import Data.Kind ( Type )
30−import Prelude hiding ( undefined )
31+import Data.Type.Equality ( apply )
32+import Prelude hiding ( id, undefined )
3133
3234-- rel8
3335import Rel8.Aggregate ( Col( A ), Aggregate )
@@ -45,7 +47,7 @@ import Rel8.Schema.Name ( Col( N ), Name )
4547import Rel8.Schema.Spec ( Spec( Spec ) )
4648import Rel8.Table
4749 ( Table, Columns, Context, fromColumns, toColumns
48− , reify, unreify
50+ , reify, unreify, coherence, congruence
4951 )
5052import Rel8.Table.Bool ( bool )
5153import Rel8.Table.Eq ( EqTable, eqTable )
@@ -139,6 +141,12 @@ instance
139141 reify = liftA2 bimap reify reify
140142 unreify = liftA2 bimap unreify unreify
141143
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+
142150
143151instance
144152 ( Nullifiable from, from ~ from'
src/Rel8/Table/HKD.hs+4−2
@@ -68,8 +68,8 @@ import Rel8.Schema.Name ( Name )
6868import Rel8.Schema.Reify ( Col( Reify ), Reify, hreify, hunreify, notReify )
6969import Rel8.Schema.Result ( Result )
7070import Rel8.Table
71− ( Table, Columns, Context, Unreify
72− , fromColumns, toColumns, reify, unreify
71+ ( Table, Columns, Context, fromColumns, toColumns
72+ , Unreify, reify, unreify, coherence, congruence
7373 , TTable, TColumns, TUnreify
7474 )
7575import Rel8.Table.Serialize ( ToExprs, fromResult, toResult )
@@ -150,6 +150,8 @@ instance HKDable a => Table Result (HKDT a) where
150150 toColumns = (\(HKD a) -> a) . toHKD . (\(HKDT a) -> a)
151151 reify = notReify
152152 unreify = notReify
153+ coherence = notReify
154+ congruence = notReify
153155
154156
155157instance
src/Rel8/Table/List.hs+25−10
@@ -16,14 +16,16 @@ module Rel8.Table.List
1616where
1717
1818-- base
19+import Control.Category ( id )
1920import Data.Functor.Identity ( Identity( Identity ) )
2021import Data.Kind ( Type )
21−import Data.Type.Equality ( (:~:)( Refl ) )
22−import Prelude
22+import Data.Type.Equality ( (:~:)( Refl ), apply )
23+import Prelude hiding ( id )
2324
2425-- rel8
2526import Rel8.Expr ( Expr, Col( E, unE ) )
2627import Rel8.Expr.Array ( sappend, sempty, slistOf )
28+import Rel8.Schema.Context.Abstract ( Abstract, exclusivity, virtual )
2729import Rel8.Schema.Dict ( Dict( Dict ) )
2830import Rel8.Schema.HTable.List ( HListTable )
2931import Rel8.Schema.HTable.Vectorize ( happend, hempty, hvectorize )
@@ -34,7 +36,7 @@ import Rel8.Schema.Spec ( SSpec(..) )
3436import Rel8.Schema.Reify ( hreify, hunreify )
3537import Rel8.Table
3638 ( Table, Context, Columns, fromColumns, toColumns
37− , reify, unreify
39+ , reify, unreify, coherence, congruence
3840 )
3941import Rel8.Table.Alternative
4042 ( AltTable, (<|>:)
@@ -44,7 +46,6 @@ import Rel8.Table.Eq ( EqTable, eqTable )
4446import Rel8.Table.Ord ( OrdTable, ordTable )
4547import Rel8.Table.Recontextualize ( Recontextualize )
4648import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
47−import Rel8.Table.Unreify ( Unreifies )
4849
4950
5051-- | A @ListTable@ value contains zero or more instances of @a@. You construct
@@ -54,7 +55,7 @@ newtype ListTable context a =
5455 ListTable (HListTable (Columns a) (Col (Context a)))
5556
5657
57−instance (Table context a, Unreifies context a, context ~ context') =>
58+instance (Table context a, Abstract context, context ~ context') =>
5859 Table context' (ListTable context a)
5960 where
6061 type Columns (ListTable context a) = HListTable (Columns a)
@@ -63,14 +64,28 @@ instance (Table context a, Unreifies context a, context ~ context') =>
6364 fromColumns = ListTable
6465 toColumns (ListTable a) = a
6566
66− reify Refl (ListTable a) = ListTable (hreify a)
67− unreify Refl (ListTable a) = ListTable (hunreify 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+
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
6883
6984
7085instance
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'
7489 )
7590 => Recontextualize from to (ListTable from' a) (ListTable to' b)
7691
src/Rel8/Table/Maybe.hs+7−2
@@ -22,9 +22,11 @@ module Rel8.Table.Maybe
2222where
2323
2424-- base
25+import Control.Category ( id )
2526import Data.Functor.Identity ( runIdentity )
2627import Data.Kind ( Type )
27−import Prelude hiding ( null, undefined )
28+import Data.Type.Equality ( apply )
29+import Prelude hiding ( id, null, undefined )
2830
2931-- rel8
3032import Rel8.Aggregate ( Col( A ), Aggregate )
@@ -44,7 +46,7 @@ import Rel8.Schema.Null ( Nullify, Nullity( Null, NotNull ), Sql, nullable )
4446import Rel8.Schema.Spec ( Spec( Spec ) )
4547import Rel8.Table
4648 ( Table, Columns, Context, fromColumns, toColumns
47− , reify, unreify
49+ , coherence, congruence, reify, unreify
4850 )
4951import Rel8.Table.Alternative
5052 ( AltTable, (<|>:)
@@ -142,6 +144,9 @@ instance (Table context a, Nullifiable context, context ~ context') =>
142144 reify = fmap fmap reify
143145 unreify = fmap fmap unreify
144146
147+ coherence = coherence @context @a
148+ congruence proof abstract = id `apply` congruence @context @a proof abstract
149+
145150
146151instance
147152 ( Nullifiable from, from ~ from'
src/Rel8/Table/NonEmpty.hs+25−10
@@ -16,15 +16,17 @@ module Rel8.Table.NonEmpty
1616where
1717
1818-- base
19+import Control.Category ( id )
1920import Data.Functor.Identity ( Identity( Identity ) )
2021import Data.Kind ( Type )
2122import Data.List.NonEmpty ( NonEmpty )
22−import Data.Type.Equality ( (:~:)( Refl ) )
23−import Prelude
23+import Data.Type.Equality ( (:~:)( Refl ), apply )
24+import Prelude hiding ( id )
2425
2526-- rel8
2627import Rel8.Expr ( Expr, Col( E, unE ) )
2728import Rel8.Expr.Array ( sappend1, snonEmptyOf )
29+import Rel8.Schema.Context.Abstract ( Abstract, exclusivity, virtual )
2830import Rel8.Schema.Dict ( Dict( Dict ) )
2931import Rel8.Schema.HTable.NonEmpty ( HNonEmptyTable )
3032import Rel8.Schema.HTable.Vectorize ( happend, hvectorize )
@@ -35,14 +37,13 @@ import Rel8.Schema.Reify ( hreify, hunreify )
3537import Rel8.Schema.Spec ( SSpec(..) )
3638import Rel8.Table
3739 ( Table, Context, Columns, fromColumns, toColumns
38− , reify, unreify
40+ , reify, unreify, coherence, congruence
3941 )
4042import Rel8.Table.Alternative ( AltTable, (<|>:) )
4143import Rel8.Table.Eq ( EqTable, eqTable )
4244import Rel8.Table.Ord ( OrdTable, ordTable )
4345import Rel8.Table.Recontextualize ( Recontextualize )
4446import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
45−import Rel8.Table.Unreify ( Unreifies )
4647
4748
4849-- | A @NonEmptyTable@ value contains one or more instances of @a@. You
@@ -52,7 +53,7 @@ newtype NonEmptyTable context a =
5253 NonEmptyTable (HNonEmptyTable (Columns a) (Col (Context a)))
5354
5455
55−instance (Table context a, Unreifies context a, context ~ context') =>
56+instance (Table context a, Abstract context, context ~ context') =>
5657 Table context' (NonEmptyTable context a)
5758 where
5859 type Columns (NonEmptyTable context a) = HNonEmptyTable (Columns a)
@@ -61,14 +62,28 @@ instance (Table context a, Unreifies context a, context ~ context') =>
6162 fromColumns = NonEmptyTable
6263 toColumns (NonEmptyTable a) = a
6364
64− reify Refl (NonEmptyTable a) = NonEmptyTable (hreify a)
65− unreify Refl (NonEmptyTable a) = NonEmptyTable (hunreify 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+
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
6681
6782
6883instance
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'
7287 )
7388 => Recontextualize from to (NonEmptyTable from' a) (NonEmptyTable to' b)
7489
src/Rel8/Table/Recontextualize.hs+33−1
@@ -14,7 +14,8 @@ where
1414-- base
1515import Data.Functor.Identity ( Identity )
1616import Data.Kind ( Constraint, Type )
17−import Prelude ()
17+import Data.List.NonEmpty ( NonEmpty)
18+import Prelude
1819
1920-- rel8
2021import Rel8.Schema.Context ( Col )
@@ -26,6 +27,9 @@ import Rel8.Schema.Spec ( KnownSpec )
2627import Rel8.Table ( Table, Congruent )
2728import Rel8.Type ( DBType )
2829
30+-- these
31+import Data.These ( These)
32+
2933
3034-- | @Recontextualize from to a b@ is evidence that the types @a@ and @b@ are
3135-- 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)
5458instance HTable t => Recontextualize from to (t (Col from)) (t (Col to))
5559
5660
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+
5789instance
5890 ( Recontextualize from to a1 b1
5991 , Recontextualize from to a2 b2
src/Rel8/Table/Rel8able.hs+4−1
@@ -41,7 +41,7 @@ import Rel8.Schema.Reify ( hreify, hunreify, UnwrapReify )
4141import Rel8.Schema.Result ( Result )
4242import Rel8.Table
4343 ( Table, Columns, Context, Congruent, fromColumns, toColumns
44− , Unreify, reify, unreify
44+ , Unreify, reify, unreify, coherence, congruence
4545 )
4646import Rel8.Schema.Spec.Constrain ( ConstrainSpec )
4747import Rel8.Table.ADT ( ADT( ADT ), ADTable, fromADT, toADT )
@@ -72,6 +72,9 @@ instance (Rel8able t, Reifiable context) =>
7272 SReify context -> case sReifiable context of
7373 Dict -> gunreify
7474
75+ coherence Refl _ = Refl
76+ congruence Refl _ = Refl
77+
7578
7679instance
7780 ( Rel8able t
src/Rel8/Table/These.hs+10−2
@@ -27,10 +27,12 @@ where
2727
2828-- base
2929import Control.Applicative ( liftA2 )
30+import Control.Category ( id )
3031import Data.Bifunctor ( Bifunctor, bimap )
3132import Data.Functor.Identity ( runIdentity )
3233import Data.Kind ( Type )
33−import Prelude hiding ( undefined )
34+import Data.Type.Equality ( apply )
35+import Prelude hiding ( id, undefined )
3436
3537-- rel8
3638import Rel8.Aggregate ( Aggregate )
@@ -47,7 +49,7 @@ import qualified Rel8.Schema.Kind as K
4749import Rel8.Schema.Name ( Name )
4850import Rel8.Table
4951 ( Table, Columns, Context, fromColumns, toColumns
50− , reify, unreify
52+ , coherence, congruence, reify, unreify
5153 )
5254import Rel8.Table.Eq ( EqTable, eqTable )
5355import Rel8.Table.Maybe
@@ -178,6 +180,12 @@ instance
178180 reify = liftA2 bimap reify reify
179181 unreify = liftA2 bimap unreify unreify
180182
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+
181189
182190instance
183191 ( 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)