git.iko.soy/rel8
on master help sign in
Better unreification; allow more nesting inside HLists
f8b1a55Shane O'Brien
src/Rel8/Column/List.hs+31−17
compare with master
unifiedsplit
@@ -1,6 +1,5 @@
1{-# language DataKinds #-}
1{-# language DataKinds #-}
2{-# language FlexibleContexts #-}
2{-# language FlexibleContexts #-}
3−{-# language GADTs #-}
4{-# language LambdaCase #-}
3{-# language LambdaCase #-}
5{-# language MultiParamTypeClasses #-}
4{-# language MultiParamTypeClasses #-}
6{-# language StandaloneKindSignatures #-}
5{-# language StandaloneKindSignatures #-}
@@ -14,6 +13,7 @@ where
14
13
15-- base
14-- base
16import Data.Kind ( Type )
15import Data.Kind ( Type )
16+import Data.Type.Equality ( (:~:)( Refl ) )
17import Prelude
17import Prelude
18
18
19-- rel8
19-- rel8
@@ -33,7 +33,10 @@ import Rel8.Table
33 )
33 )
34import Rel8.Table.List ( ListTable( ListTable ) )
34import Rel8.Table.List ( ListTable( ListTable ) )
35import Rel8.Table.Recontextualize ( Recontextualize )
35import Rel8.Table.Recontextualize ( Recontextualize )
36−import Rel8.Table.Unreify ( Unreifiable )
36+import Rel8.Table.Unreify
37+ ( Unreifiability( Unreifiability )
38+ , Unreifiable, unreifiability
39+ )
37
40
38
41
39type HList :: K.Context -> Type -> Type
42type HList :: K.Context -> Type -> Type
@@ -50,12 +53,8 @@ type AHList :: K.Context -> Type -> Type
50newtype AHList context a = AHList (HList context a)
53newtype AHList context a = AHList (HList context a)
51
54
52
55
53−instance
54− ( Reifiable context
55− , Table (Reify context) a
56− , Unreifiable (Reify context) a
56+instance (Reifiable context, Unreifiable a, Table (Reify context) a) =>
57− )
58− => Table (Reify context) (AHList context a)
57+ Table (Reify context) (AHList context a)
59 where
58 where
60 type Context (AHList context a) = Reify context
59 type Context (AHList context a) = Reify context
61 type Columns (AHList context a) = HListTable (Columns a)
60 type Columns (AHList context a) = HListTable (Columns a)
@@ -63,20 +62,17 @@ instance
63
62
64 fromColumns = sfromColumnsList contextSing
63 fromColumns = sfromColumnsList contextSing
65 toColumns = stoColumnsList contextSing
64 toColumns = stoColumnsList contextSing
66− reify proof =
65+
67− smapList contextSing (reify proof) hreify .
66+ reify _ = sreifyList (unreifiability contextSing)
68− AHList
67+ unreify _ = sunreifyList (unreifiability contextSing)
69− unreify proof =
70− (\(AHList a) -> a) .
71− smapList contextSing (unreify proof) hunreify
72
68
73
69
74instance
70instance
75 ( Reifiable context, Reifiable context'
71 ( Reifiable context, Reifiable context'
76− , Unreifiable (Reify context) a, Unreifiable (Reify context') a'
72+ , Unreifiable a, Unreifiable a'
77 , Recontextualize (Reify context) (Reify context') a a'
73 , Recontextualize (Reify context) (Reify context') a a'
78− ) =>
74+ )
79− Recontextualize
75+ => Recontextualize
80 (Reify context)
76 (Reify context)
81 (Reify context')
77 (Reify context')
82 (AHList context a)
78 (AHList context a)
@@ -131,3 +127,21 @@ stoColumnsList = \case
131 stoColumnsList context .
127 stoColumnsList context .
132 smapList context (hunreify . toColumns) hunreify .
128 smapList context (hunreify . toColumns) hunreify .
133 (\(AHList a) -> a)
129 (\(AHList a) -> a)
130+
131+
132+sreifyList :: ()
133+ => Unreifiability context a
134+ -> HList context (Unreify a)
135+ -> AHList context a
136+sreifyList (Unreifiability context) =
137+ smapList context (reify Refl) hreify .
138+ AHList
139+
140+
141+sunreifyList :: ()
142+ => Unreifiability context a
143+ -> AHList context a
144+ -> HList context (Unreify a)
145+sunreifyList (Unreifiability context) =
146+ (\(AHList a) -> a) .
147+ smapList context (unreify Refl) hunreify
src/Rel8/Column/NonEmpty.hs+31−17
@@ -1,6 +1,5 @@
1{-# language DataKinds #-}
1{-# language DataKinds #-}
2{-# language FlexibleContexts #-}
2{-# language FlexibleContexts #-}
3−{-# language GADTs #-}
4{-# language LambdaCase #-}
3{-# language LambdaCase #-}
5{-# language MultiParamTypeClasses #-}
4{-# language MultiParamTypeClasses #-}
6{-# language StandaloneKindSignatures #-}
5{-# language StandaloneKindSignatures #-}
@@ -15,6 +14,7 @@ where
15-- base
14-- base
16import Data.Kind ( Type )
15import Data.Kind ( Type )
17import Data.List.NonEmpty ( NonEmpty )
16import Data.List.NonEmpty ( NonEmpty )
17+import Data.Type.Equality ( (:~:)( Refl ) )
18import Prelude
18import Prelude
19
19
20-- rel8
20-- rel8
@@ -34,7 +34,10 @@ import Rel8.Table
34 )
34 )
35import Rel8.Table.NonEmpty ( NonEmptyTable( NonEmptyTable ) )
35import Rel8.Table.NonEmpty ( NonEmptyTable( NonEmptyTable ) )
36import Rel8.Table.Recontextualize ( Recontextualize )
36import Rel8.Table.Recontextualize ( Recontextualize )
37−import Rel8.Table.Unreify ( Unreifiable )
37+import Rel8.Table.Unreify
38+ ( Unreifiability( Unreifiability )
39+ , Unreifiable, unreifiability
40+ )
38
41
39
42
40type HNonEmpty :: K.Context -> Type -> Type
43type HNonEmpty :: K.Context -> Type -> Type
@@ -51,12 +54,8 @@ type AHNonEmpty :: K.Context -> Type -> Type
51newtype AHNonEmpty context a = AHNonEmpty (HNonEmpty context a)
54newtype AHNonEmpty context a = AHNonEmpty (HNonEmpty context a)
52
55
53
56
54−instance
55− ( Reifiable context
56− , Table (Reify context) a
57− , Unreifiable (Reify context) a
57+instance (Reifiable context, Unreifiable a, Table (Reify context) a) =>
58− )
59− => Table (Reify context) (AHNonEmpty context a)
58+ Table (Reify context) (AHNonEmpty context a)
60 where
59 where
61 type Context (AHNonEmpty context a) = Reify context
60 type Context (AHNonEmpty context a) = Reify context
62 type Columns (AHNonEmpty context a) = HNonEmptyTable (Columns a)
61 type Columns (AHNonEmpty context a) = HNonEmptyTable (Columns a)
@@ -64,20 +63,17 @@ instance
64
63
65 fromColumns = sfromColumnsNonEmpty contextSing
64 fromColumns = sfromColumnsNonEmpty contextSing
66 toColumns = stoColumnsNonEmpty contextSing
65 toColumns = stoColumnsNonEmpty contextSing
67− reify proof =
66+
68− smapNonEmpty contextSing (reify proof) hreify .
67+ reify _ = sreifyNonEmpty (unreifiability contextSing)
69− AHNonEmpty
68+ unreify _ = sunreifyNonEmpty (unreifiability contextSing)
70− unreify proof =
71− (\(AHNonEmpty a) -> a) .
72− smapNonEmpty contextSing (unreify proof) hunreify
73
69
74
70
75instance
71instance
76 ( Reifiable context, Reifiable context'
72 ( Reifiable context, Reifiable context'
77− , Unreifiable (Reify context) a, Unreifiable (Reify context') a'
73+ , Unreifiable a, Unreifiable a'
78 , Recontextualize (Reify context) (Reify context') a a'
74 , Recontextualize (Reify context) (Reify context') a a'
79− ) =>
75+ )
80− Recontextualize
76+ => Recontextualize
81 (Reify context)
77 (Reify context)
82 (Reify context')
78 (Reify context')
83 (AHNonEmpty context a)
79 (AHNonEmpty context a)
@@ -133,3 +129,21 @@ stoColumnsNonEmpty = \case
133 stoColumnsNonEmpty context .
129 stoColumnsNonEmpty context .
134 smapNonEmpty context (hunreify . toColumns) hunreify .
130 smapNonEmpty context (hunreify . toColumns) hunreify .
135 (\(AHNonEmpty a) -> a)
131 (\(AHNonEmpty a) -> a)
132+
133+
134+sreifyNonEmpty :: ()
135+ => Unreifiability context a
136+ -> HNonEmpty context (Unreify a)
137+ -> AHNonEmpty context a
138+sreifyNonEmpty (Unreifiability context) =
139+ smapNonEmpty context (reify Refl) hreify .
140+ AHNonEmpty
141+
142+
143+sunreifyNonEmpty :: ()
144+ => Unreifiability context a
145+ -> AHNonEmpty context a
146+ -> HNonEmpty context (Unreify a)
147+sunreifyNonEmpty (Unreifiability context) =
148+ (\(AHNonEmpty a) -> a) .
149+ smapNonEmpty context (unreify Refl) hunreify
src/Rel8/Generic/Rel8able/Test.hs+8
@@ -82,6 +82,14 @@ data TableNonEmpty f = TableNonEmpty
82 deriving anyclass Rel8able
82 deriving anyclass Rel8able
83
83
84
84
85+data TableNest f = TableNest
86+ { foo :: Column f Bool
87+ , bars :: HList f (HMaybe f (TablePair f))
88+ }
89+ deriving stock Generic
90+ deriving anyclass Rel8able
91+
92+
85data S3Object = S3Object
93data S3Object = S3Object
86 { bucketName :: Text
94 { bucketName :: Text
87 , objectKey :: Text
95 , objectKey :: Text
src/Rel8/Table/List.hs+3−3
@@ -45,7 +45,7 @@ import Rel8.Table.Eq ( EqTable, eqTable )
45import Rel8.Table.Ord ( OrdTable, ordTable )
45import Rel8.Table.Ord ( OrdTable, ordTable )
46import Rel8.Table.Recontextualize ( Recontextualize )
46import Rel8.Table.Recontextualize ( Recontextualize )
47import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
47import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
48−import Rel8.Table.Unreify ( Unreifiable )
48+import Rel8.Table.Unreify ( Unreifies )
49
49
50
50
51-- | 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 +54,7 @@ type ListTable :: Type -> Type
54newtype ListTable a = ListTable (HListTable (Columns a) (Col (Context a)))
54newtype ListTable a = ListTable (HListTable (Columns a) (Col (Context a)))
55
55
56
56
57−instance (Table context a, Unreifiable context a) =>
57+instance (Table context a, Unreifies context a) =>
58 Table context (ListTable a)
58 Table context (ListTable a)
59 where
59 where
60 type Columns (ListTable a) = HListTable (Columns a)
60 type Columns (ListTable a) = HListTable (Columns a)
@@ -68,7 +68,7 @@ instance (Table context a, Unreifiable context a) =>
68
68
69
69
70instance
70instance
71− ( Unreifiable from a, Unreifiable to b
71+ ( Unreifies from a, Unreifies to b
72 , Recontextualize from to a b
72 , Recontextualize from to a b
73 )
73 )
74 => Recontextualize from to (ListTable a) (ListTable b)
74 => Recontextualize from to (ListTable a) (ListTable b)
src/Rel8/Table/NonEmpty.hs+3−3
@@ -43,7 +43,7 @@ import Rel8.Table.Eq ( EqTable, eqTable )
43import Rel8.Table.Ord ( OrdTable, ordTable )
43import Rel8.Table.Ord ( OrdTable, ordTable )
44import Rel8.Table.Recontextualize ( Recontextualize )
44import Rel8.Table.Recontextualize ( Recontextualize )
45import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
45import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )
46−import Rel8.Table.Unreify ( Unreifiable )
46+import Rel8.Table.Unreify ( Unreifies )
47
47
48
48
49-- | A @NonEmptyTable@ value contains one or more instances of @a@. You
49-- | A @NonEmptyTable@ value contains one or more instances of @a@. You
@@ -53,7 +53,7 @@ newtype NonEmptyTable a =
53 NonEmptyTable (HNonEmptyTable (Columns a) (Col (Context a)))
53 NonEmptyTable (HNonEmptyTable (Columns a) (Col (Context a)))
54
54
55
55
56−instance (Table context a, Unreifiable context a) =>
56+instance (Table context a, Unreifies context a) =>
57 Table context (NonEmptyTable a)
57 Table context (NonEmptyTable a)
58 where
58 where
59 type Columns (NonEmptyTable a) = HNonEmptyTable (Columns a)
59 type Columns (NonEmptyTable a) = HNonEmptyTable (Columns a)
@@ -67,7 +67,7 @@ instance (Table context a, Unreifiable context a) =>
67
67
68
68
69instance
69instance
70− ( Unreifiable from a, Unreifiable to b
70+ ( Unreifies from a, Unreifies to b
71 , Recontextualize from to a b
71 , Recontextualize from to a b
72 )
72 )
73 => Recontextualize from to (NonEmptyTable a) (NonEmptyTable b)
73 => Recontextualize from to (NonEmptyTable a) (NonEmptyTable b)
src/Rel8/Table/Unreify.hs+75−9
@@ -1,4 +1,11 @@
1{-# language DataKinds #-}
1{-# language DataKinds #-}
2+{-# language FlexibleContexts #-}
3+{-# language FlexibleInstances #-}
4+{-# language GADTs #-}
5+{-# language LambdaCase #-}
6+{-# language MultiParamTypeClasses #-}
7+{-# language QuantifiedConstraints #-}
8+{-# language RankNTypes #-}
2{-# language StandaloneKindSignatures #-}
9{-# language StandaloneKindSignatures #-}
3{-# language TypeFamilies #-}
10{-# language TypeFamilies #-}
4{-# language UndecidableInstances #-}
11{-# language UndecidableInstances #-}
@@ -20,7 +27,8 @@
20-- @Table@)
27-- @Table@)
21
28
22module Rel8.Table.Unreify
29module Rel8.Table.Unreify
23− ( Unreifiable
30+ ( Unreifiable, Unreifiability( Unreifiability ), unreifiability
31+ , Unreifies
24 )
32 )
25where
33where
26
34
@@ -29,15 +37,73 @@ import Data.Kind ( Constraint, Type )
29import Prelude ()
37import Prelude ()
30
38
31-- rel8
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 Rel8.Schema.Insert ( Insert )
32import qualified Rel8.Schema.Kind as K
45import qualified Rel8.Schema.Kind as K
46+import Rel8.Schema.Name ( Name )
33import Rel8.Schema.Reify ( Reify )
47import Rel8.Schema.Reify ( Reify )
48+import Rel8.Schema.Result ( Result )
34−import Rel8.Table ( Table, Columns, Unreify )
49+import Rel8.Table ( Table, Context, Congruent, Unreify )
35
50
36
51
37−type Unreifiable :: K.Context -> Type -> Constraint
52+type Unreifies :: K.Context -> Type -> Constraint
38−type family Unreifiable context a where
53+type family Unreifies context a where
39− Unreifiable (Reify context) a =
54+ Unreifies (Reify context) a = Unreifier context a
55+ Unreifies _ _ = ()
56+
57+
58+type Unreifiable :: Type -> Constraint
59+class
60+ ( Context a ~ Reify Aggregate => Unreifier Aggregate a
61+ , Context a ~ Reify Expr => Unreifier Expr a
62+ , Context a ~ Reify Insert => Unreifier Insert a
63+ , Context a ~ Reify Name => Unreifier Name a
64+ , Context a ~ Reify Result => Unreifier Result a
65+ , (forall ctx. (Context a ~ Reify (Reify ctx), Reifiable ctx) => Unreifier (Reify ctx) a)
66+ )
67+ => Unreifiable a
68+instance
69+ ( Context a ~ Reify Aggregate => Unreifier Aggregate a
70+ , Context a ~ Reify Expr => Unreifier Expr a
71+ , Context a ~ Reify Insert => Unreifier Insert a
72+ , Context a ~ Reify Name => Unreifier Name a
73+ , Context a ~ Reify Result => Unreifier Result a
74+ , (forall ctx. (Context a ~ Reify (Reify ctx), Reifiable ctx) => Unreifier (Reify ctx) a)
75+ )
76+ => Unreifiable a
77+
78+
79+type Unreifier :: K.Context -> Type -> Constraint
80+class
81+ ( Table (Reify context) a
40− ( Table context (Unreify a)
82+ , Table context (Unreify a)
41− , Columns a ~ Columns (Unreify a)
83+ , Congruent a (Unreify a)
42− )
84+ )
43− Unreifiable _ _ = ()
85+ => Unreifier context a
86+instance
87+ ( Table (Reify context) a
88+ , Table context (Unreify a)
89+ , Congruent a (Unreify a)
90+ )
91+ => Unreifier context a
92+
93+
94+type Unreifiability :: K.Context -> Type -> Type
95+data Unreifiability context a where
96+ Unreifiability :: Unreifier context a
97+ => SContext context -> Unreifiability context a
98+
99+
100+unreifiability :: (Context a ~ Reify context, Unreifiable a)
101+ => SContext context -> Unreifiability context a
102+unreifiability = \case
103+ SAggregate -> Unreifiability SAggregate
104+ SExpr -> Unreifiability SExpr
105+ SInsert -> Unreifiability SInsert
106+ SName -> Unreifiability SName
107+ SResult -> Unreifiability SResult
108+ SReify context -> case sReifiable context of
109+ Dict -> Unreifiability (SReify context)