git.iko.soy/rel8
on 5a47018 help sign in
rel8/src/Rel8/Table/Nullify.hs
204 lines 6.3 kB history raw
1{-# language DataKinds #-}
2{-# language FlexibleInstances #-}
3{-# language LambdaCase #-}
4{-# language MultiParamTypeClasses #-}
5{-# language ScopedTypeVariables #-}
6{-# language StandaloneKindSignatures #-}
7{-# language TypeApplications #-}
8{-# language TypeFamilies #-}
9{-# language UndecidableInstances #-}
11module Rel8.Table.Nullify
12 ( Nullify
13 , aggregateNullify
14 , guard
15 )
16where
18-- base
19import Control.Applicative ( liftA2 )
20import Control.Category ( id )
21import Data.Functor.Identity ( runIdentity )
22import Data.Kind ( Type )
23import Data.Type.Equality ( (:~:)( Refl ), apply )
24import Prelude hiding ( id )
26-- comonad
27import Control.Comonad ( Comonad, duplicate, extract, ComonadApply, (<@>) )
29-- rel8
30import Rel8.Aggregate ( Aggregate )
31import Rel8.Expr ( Expr )
32import Rel8.Kind.Context ( Reifiable, contextSing )
33import Rel8.Schema.Context ( Col )
34import Rel8.Schema.Context.Abstract ( Abstract, exclusivity, virtual )
35import Rel8.Schema.Context.Nullify
36 ( Nullifiability( NAggregate, NExpr )
37 , NonNullifiability( NNReify )
38 , Nullifiable, nullifiability
39 , nullifiableOrNot, absurd
40 , guarder
41 , nullifier
42 , unnullifier
43 )
44import Rel8.Schema.Dict ( Dict( Dict ) )
45import Rel8.Schema.HTable ( HTable )
46import Rel8.Schema.HTable.Nullify ( HNullify, hnullify, hunnullify, hguard )
47import qualified Rel8.Schema.Kind as K
48import Rel8.Schema.Reify ( hreify, hunreify )
49import Rel8.Schema.Spec ( Spec( Spec ) )
50import Rel8.Table
51 ( Table, Columns, Context, toColumns, fromColumns
52 , reify, unreify, coherence, congruence
53 )
54import Rel8.Table.Eq ( EqTable, eqTable )
55import Rel8.Table.Ord ( OrdTable, ordTable )
56import Rel8.Table.Recontextualize ( Recontextualize )
58-- semigroupoids
59import Data.Functor.Apply ( Apply, (<.>), liftF2 )
60import Data.Functor.Bind ( Bind, (>>-) )
61import Data.Functor.Extend ( Extend, duplicated )
64type Nullify :: K.Context -> Type -> Type
65data Nullify context a
66 = Table (Nullifiability context) a
67 | Fields (NonNullifiability context) (HNullify (Columns a) (Col (Context a)))
70instance Nullifiable context => Functor (Nullify context) where
71 fmap f = \case
72 Table nullifiable a -> Table nullifiable (f a)
73 Fields notNullifiable _ -> absurd nullifiability notNullifiable
76instance Nullifiable context => Foldable (Nullify context) where
77 foldMap f = \case
78 Table _ a -> f a
79 Fields notNullifiable _ -> absurd nullifiability notNullifiable
82instance Nullifiable context => Traversable (Nullify context) where
83 traverse f = \case
84 Table nullifiable a -> Table nullifiable <$> f a
85 Fields notNullifiable _ -> absurd nullifiability notNullifiable
88instance Nullifiable context => Apply (Nullify context) where
89 liftF2 f = \case
90 Table nullifiable a -> \case
91 Table _ b -> Table nullifiable (f a b)
92 Fields notNullifiable _ -> absurd nullifiable notNullifiable
93 Fields notNullifiable _ -> absurd nullifiability notNullifiable
96instance Nullifiable context => Applicative (Nullify context) where
97 pure = Table nullifiability
98 liftA2 = liftF2
101instance Nullifiable context => Bind (Nullify context) where
102 Table _ a >>- f = f a
103 Fields notNullifiable _ >>- _ = absurd nullifiability notNullifiable
106instance Nullifiable context => Monad (Nullify context) where
107 (>>=) = (>>-)
110instance Nullifiable context => Extend (Nullify context) where
111 duplicated = \case
112 Table nullifiable a -> Table nullifiable (Table nullifiable a)
113 Fields notNullifiable _ -> absurd nullifiability notNullifiable
116instance Nullifiable context => Comonad (Nullify context) where
117 extract = \case
118 Table _ a -> a
119 Fields notNullifiable _ -> absurd nullifiability notNullifiable
120 duplicate = duplicated
123instance Nullifiable context => ComonadApply (Nullify context) where
124 (<@>) = (<.>)
127instance
128 ( Table context a
129 , Reifiable context, Abstract context, context ~ context'
130 )
131 => Table context' (Nullify context a)
132 where
133 type Columns (Nullify context a) = HNullify (Columns a)
134 type Context (Nullify context a) = Context a
136 fromColumns = case nullifiableOrNot contextSing of
137 Left notNullifiable -> Fields notNullifiable
138 Right nullifiable ->
139 Table nullifiable .
140 fromColumns .
141 runIdentity .
142 hunnullify (\spec -> pure . unnullifier nullifiable spec)
144 toColumns = \case
145 Table nullifiable a -> hnullify (nullifier nullifiable) (toColumns a)
146 Fields _ a -> a
148 reify proof@Refl = \case
149 Table nullifiable a -> Table nullifiable (reify proof a)
150 Fields notNullifiable a -> case notNullifiable of
151 NNReify (_ :: NonNullifiability ctx) ->
152 case coherence @context @a proof abstract of
153 Refl -> case congruence @context @a proof abstract of
154 Refl -> Fields notNullifiable (hreify a)
155 where
156 abstract = exclusivity (virtual @ctx)
158 unreify proof@Refl = \case
159 Table nullifiable a -> Table nullifiable (unreify proof a)
160 Fields notNullifiable a -> case notNullifiable of
161 NNReify (_ :: NonNullifiability ctx) ->
162 case coherence @context @a proof abstract of
163 Refl -> case congruence @context @a proof abstract of
164 Refl -> Fields notNullifiable (hunreify a)
165 where
166 abstract = exclusivity (virtual @ctx)
168 coherence = coherence @context @a
169 congruence proof abstract = id `apply` congruence @context @a proof abstract
172instance
173 ( Recontextualize from to a b
174 , Reifiable from, Abstract from, from ~ from'
175 , Reifiable to, Abstract to, to ~ to'
176 )
177 => Recontextualize from' to' (Nullify from a) (Nullify to b)
180instance (EqTable a, context ~ Expr) => EqTable (Nullify context a) where
181 eqTable = hnullify (\_ Dict -> Dict) (eqTable @a)
184instance (OrdTable a, context ~ Expr) => OrdTable (Nullify context a) where
185 ordTable = hnullify (\_ Dict -> Dict) (ordTable @a)
188aggregateNullify :: ()
189 => (exprs -> aggregates)
190 -> Nullify Expr exprs
191 -> Nullify Aggregate aggregates
192aggregateNullify f = \case
193 Table _ a -> Table NAggregate (f a)
194 Fields notNullifiable _ -> absurd NExpr notNullifiable
197guard :: (Reifiable context, HTable t)
198 => Col context ('Spec tag)
199 -> (tag -> Bool)
200 -> (Expr tag -> Expr Bool)
201 -> HNullify t (Col context)
202 -> HNullify t (Col context)
203guard tag isNonNull isNonNullExpr =
204 hguard (guarder contextSing tag isNonNull isNonNullExpr)