be54907 · rel8 · git.iko.soy

git.iko.soy/rel8

Introduce Rel8.Table.Nullify (#104)

This factors out some of the common code that was duplicated in Rel8.Table.Either, Rel8.Table.Maybe and Rel8.Table.These. But it's also more complex than this code was, because it allows for the possibility of a `MaybeTable` in a non-`Nullifiable` context which is a `Table`, but not a `Functor`. This is relevant for the `Projection` work.

commitbe54907e928e8669aea5ca3683ac996b7d806640 authorShane <shane.obrien@circuithub.com> dateMon 5 Jul 2021, 02:42 (5 years ago) parent991998a

11 files changed+476−175

compare with master

unifiedsplit

rel8.cabal+2 src/Rel8/Generic/Construction.hs+2−3 src/Rel8/Query/Either.hs+5−2 src/Rel8/Query/Maybe.hs+10−6 src/Rel8/Query/These.hs+9−6 src/Rel8/Schema/Context/Nullify.hs+109−47 src/Rel8/Schema/HTable/Nullify.hs+26−8 src/Rel8/Table/Either.hs+46−41 src/Rel8/Table/Maybe.hs+36−30 src/Rel8/Table/Nullify.hs+204 src/Rel8/Table/These.hs+27−32

rel8.cabal+2

@@ -23,6 +23,7 @@ library

2323 , base ^>= 4.14 || ^>=4.15

2424 , bytestring

2525 , case-insensitive

26+ , comonad

2627 , contravariant

2728 , hasql ^>= 1.4.5.1

2829 , opaleye ^>= 0.7.3.0

@@ -158,6 +159,7 @@ library

158159 Rel8.Table.Maybe

159160 Rel8.Table.Name

160161 Rel8.Table.NonEmpty

162+ Rel8.Table.Nullify

161163 Rel8.Table.Opaleye

162164 Rel8.Table.Ord

163165 Rel8.Table.Order

src/Rel8/Generic/Construction.hs+2−3

@@ -3,7 +3,6 @@

33{-# language DataKinds #-}

44{-# language FlexibleContexts #-}

55{-# language FlexibleInstances #-}

6−{-# language LambdaCase #-}

76{-# language MultiParamTypeClasses #-}

87{-# language NamedFieldPuns #-}

98{-# language ScopedTypeVariables #-}

@@ -59,7 +58,7 @@ import Rel8.Kind.Algebra

5958 , KnownAlgebra, algebraSing

6059 )

6160import qualified Rel8.Kind.Algebra as K

62−import Rel8.Schema.Context.Nullify ( guardExpr, snullify )

61+import Rel8.Schema.Context.Nullify ( sguard, snullify )

6362import Rel8.Schema.HTable ( HTable )

6463import Rel8.Schema.HTable.Identity ( HIdentity( HType ) )

6564import qualified Rel8.Schema.Kind as K

@@ -349,7 +348,7 @@ ggaggregate gfromColumns gtoColumns agg es = case algebraSing @algebra of

349348 @(Eval (rep (Reify Aggregate)))

350349 (\(_ :: proxy x) -> toColumns . reify @_ @x Refl)

351350 (\tag' SSpec {nullity} (Reify (A (Aggregate a))) ->

352− Reify $ A $ Aggregate $ guardExpr (tag ==. litExpr tag') . snullify nullity <$> a)

351+ Reify $ A $ Aggregate $ sguard (tag ==. litExpr tag') . snullify nullity <$> a)

353352 (HType (Reify (A (groupByExpr tag))))

354353 where

355354 f =

src/Rel8/Query/Either.hs+5−2

@@ -10,6 +10,9 @@ where

1010-- base

1111import Prelude

1212

13+-- comonad

14+import Control.Comonad ( extract )

15+

1316-- rel8

1417import Rel8.Expr ( Expr )

1518import Rel8.Expr.Eq ( (==.) )

@@ -27,14 +30,14 @@ import Rel8.Table.Maybe ( MaybeTable( MaybeTable ), isJustTable )

2730keepLeftTable :: EitherTable Expr a b -> Query a

2831keepLeftTable e@(EitherTable _ a _) = do

2932 where_ $ isLeftTable e

30− pure a

33+ pure (extract a)

3134

3235

3336-- | Filter 'EitherTable's, keeping only 'rightTable's.

3437keepRightTable :: EitherTable Expr a b -> Query b

3538keepRightTable e@(EitherTable _ _ b) = do

3639 where_ $ isRightTable e

37− pure b

40+ pure (extract b)

3841

3942

4043-- | @bitraverseEitherTable f g x@ will pass all @leftTable@s through @f@ and

src/Rel8/Query/Maybe.hs+10−6

@@ -1,4 +1,5 @@

11{-# language GADTs #-}

2+{-# language NamedFieldPuns #-}

34module Rel8.Query.Maybe

45 ( optional

@@ -10,6 +11,9 @@ where

1011-- base

1112import Prelude

1213

14+-- comonad

15+import Control.Comonad ( extract )

16+

1317-- opaleye

1418import qualified Opaleye.Internal.MaybeFields as Opaleye

1519

@@ -20,7 +24,7 @@ import Rel8.Expr.Opaleye ( fromColumn, fromPrimExpr )

2024import Rel8.Query ( Query )

2125import Rel8.Query.Filter ( where_ )

2226import Rel8.Query.Opaleye ( mapOpaleye )

23−import Rel8.Table.Maybe ( MaybeTable( MaybeTable ), isJustTable )

27+import Rel8.Table.Maybe ( MaybeTable(..), isJustTable )

2428

2529

2630-- | Convert a query that might return zero rows to a query that always returns

@@ -29,10 +33,10 @@ import Rel8.Table.Maybe ( MaybeTable( MaybeTable ), isJustTable )

2933-- To speak in more concrete terms, 'optional' is most useful to write @LEFT

3034-- JOIN@s.

3135optional :: Query a -> Query (MaybeTable Expr a)

32−optional =

33− mapOpaleye $

34− Opaleye.optionalInternal $

35− MaybeTable . E . fromPrimExpr . fromColumn

36+optional = mapOpaleye $ Opaleye.optionalInternal $ \tag a -> MaybeTable

37+ { tag = E $ fromPrimExpr $ fromColumn tag

38+ , just = pure a

39+ }

3640

3741

3842-- | Filter out 'MaybeTable's, returning only the tables that are not-null.

@@ -43,7 +47,7 @@ optional =

4347catMaybeTable :: MaybeTable Expr a -> Query a

4448catMaybeTable ma@(MaybeTable _ a) = do

4549 where_ $ isJustTable ma

46− pure a

50+ pure (extract a)

4751

4852

4953-- | Extend an optional query with another query. This is useful if you want

src/Rel8/Query/These.hs+9−6

@@ -15,6 +15,9 @@ where

1515-- base

1616import Prelude

1717

18+-- comonad

19+import Control.Comonad ( extract )

20+

1821-- opaleye

1922import qualified Opaleye.Internal.PackMap as Opaleye

2023import qualified Opaleye.Internal.PrimQuery as Opaleye

@@ -59,7 +62,7 @@ alignBy condition = zipOpaleyeWith $ \left right -> Opaleye.QueryArr $ \i -> cas

5962 tag''' = Opaleye.next tag''

6063 join lateral = Opaleye.Join Opaleye.FullJoin on left'' right''

6164 where

62− on = toPrimExpr $ condition a b

65+ on = toPrimExpr $ condition (extract a) (extract b)

6366 left'' = (lateral, Opaleye.Rebind True lbindings left')

6467 right'' = (lateral, Opaleye.Rebind True rbindings right')

6568 ma' = MaybeTable (E hasHere') a

@@ -87,31 +90,31 @@ loseThereTable = keepThisTable

8790keepThisTable :: TheseTable Expr a b -> Query a

8891keepThisTable t@(TheseTable (MaybeTable _ a) _) = do

8992 where_ $ isThisTable t

90− pure a

93+ pure (extract a)

9194

9295

9396loseThisTable :: TheseTable Expr a b -> Query (MaybeTable Expr a, b)

9497loseThisTable t@(TheseTable ma (MaybeTable _ b)) = do

9598 where_ $ not_ $ isThisTable t

96− pure (ma, b)

99+ pure (ma, extract b)

97100

98101

99102keepThatTable :: TheseTable Expr a b -> Query b

100103keepThatTable t@(TheseTable _ (MaybeTable _ b)) = do

101104 where_ $ isThatTable t

102− pure b

105+ pure (extract b)

103106

104107

105108loseThatTable :: TheseTable Expr a b -> Query (a, MaybeTable Expr b)

106109loseThatTable t@(TheseTable (MaybeTable _ a) mb) = do

107110 where_ $ not_ $ isThatTable t

108− pure (a, mb)

111+ pure (extract a, mb)

109112

110113

111114keepThoseTable :: TheseTable Expr a b -> Query (a, b)

112115keepThoseTable t@(TheseTable (MaybeTable _ a) (MaybeTable _ b)) = do

113116 where_ $ isThoseTable t

114− pure (a, b)

117+ pure (extract a, extract b)

115118

116119

117120loseThoseTable :: TheseTable Expr a b -> Query (EitherTable Expr a b)

src/Rel8/Schema/Context/Nullify.hs+109−47

@@ -1,17 +1,23 @@

11{-# language DataKinds #-}

2+{-# language EmptyCase #-}

23{-# language FlexibleContexts #-}

34{-# language GADTs #-}

5+{-# language LambdaCase #-}

46{-# language NamedFieldPuns #-}

57{-# language StandaloneKindSignatures #-}

79module Rel8.Schema.Context.Nullify

8− ( Nullifiable, nullifier, unnullifier

9− , guardExpr, snullify

10+ ( Nullifiability(..), NonNullifiability(..), nullifiableOrNot, absurd

11+ , Nullifiable, nullifiability

12+ , guarder, nullifier, unnullifier

13+ , sguard, snullify

1014 )

1115where

1216

1317-- base

14−import Data.Kind ( Constraint )

18+import Data.Bifunctor ( bimap )

19+import Data.Bool ( bool )

20+import Data.Kind ( Constraint, Type )

1521import Data.Monoid ( getFirst )

1622import Prelude hiding ( null )

1723

@@ -20,73 +26,129 @@ import qualified Opaleye.Internal.HaskellDB.PrimQuery as Opaleye

2026

2127-- rel8

2228import Rel8.Aggregate

23− ( Aggregate( Aggregate ), Col( A )

29+ ( Col( A ), Aggregate( Aggregate )

2430 , foldInputs, mapInputs

2531 )

26−import Rel8.Expr ( Expr, Col( E ) )

32+import Rel8.Expr ( Col( E ), Expr )

2733import Rel8.Expr.Bool ( boolExpr )

2834import Rel8.Expr.Null ( nullify, unsafeUnnullify )

2935import Rel8.Expr.Opaleye ( fromPrimExpr, toPrimExpr )

36+import Rel8.Kind.Context ( SContext(..) )

3037import qualified Rel8.Schema.Kind as K

31−import Rel8.Schema.Name ( Name( Name ), Col( N ) )

32−import Rel8.Schema.Null ( Nullify, Nullity( Null, NotNull ), Sql )

33−import Rel8.Schema.Reify ( Reify, Col( Reify ) )

38+import Rel8.Schema.Name ( Col( N ), Name( Name ) )

39+import Rel8.Schema.Null ( Nullify, Nullity( Null, NotNull ) )

40+import Rel8.Schema.Reify ( Col( Reify ), Reify )

41+import Rel8.Schema.Result ( Col( R ), Result )

3442import Rel8.Schema.Spec ( Spec( Spec ), SSpec(..) )

35−import Rel8.Type ( DBType )

43+

44+

45+type Nullifiability :: K.Context -> Type

46+data Nullifiability context where

47+ NAggregate :: Nullifiability Aggregate

48+ NExpr :: Nullifiability Expr

49+ NName :: Nullifiability Name

50+ NReify :: Nullifiability context -> Nullifiability (Reify context)

3651

3752

3853type Nullifiable :: K.Context -> Constraint

3954class Nullifiable context where

40− nullifier :: Sql DBType tag

41− => Col context ('Spec tag)

42− -> (Expr tag -> Expr Bool)

43− -> SSpec ('Spec a)

44− -> Col context ('Spec a)

45− -> Col context ('Spec (Nullify a))

46−

47− unnullifier :: ()

48− => SSpec ('Spec a)

49− -> Col context ('Spec (Nullify a))

50− -> Col context ('Spec a)

55+ nullifiability :: Nullifiability context

5156

5257

5358instance Nullifiable Aggregate where

54− nullifier (A tag) isNonNull SSpec {nullity} (A (Aggregate a)) =

55− A $

56− mapInputs (toPrimExpr . run . fromPrimExpr) $

57− Aggregate $

58− run <$> a

59− where

60− mtag = foldInputs (\_ -> pure . fromPrimExpr) tag

61− run = maybe id (guardExpr . isNonNull) (getFirst mtag) . snullify nullity

62−

63− unnullifier SSpec {nullity} (A (Aggregate a)) =

64− A $ Aggregate $ sunnullify nullity <$> a

59+ nullifiability = NAggregate

6560

6661

6762instance Nullifiable Expr where

68− nullifier (E tag) isNonNull SSpec {nullity} (E a) =

69− E $ guardExpr condition (snullify nullity a)

70− where

71− condition = isNonNull tag

72−

73− unnullifier SSpec {nullity} (E a) = E $ sunnullify nullity a

63+ nullifiability = NExpr

7464

7565

7666instance Nullifiable Name where

77− nullifier _ _ _ (N (Name a)) = N $ Name a

78− unnullifier _ (N (Name a)) = N $ Name a

67+ nullifiability = NName

7968

8069

8170instance Nullifiable context => Nullifiable (Reify context) where

82− nullifier (Reify tag) isNonNull spec (Reify a) =

83− Reify $ nullifier tag isNonNull spec a

84−

85− unnullifier spec (Reify a) = Reify (unnullifier spec a)

86−

87−

88−guardExpr :: Expr Bool -> Expr (Maybe a) -> Expr (Maybe a)

89−guardExpr condition a = boolExpr null a condition

71+ nullifiability = NReify nullifiability

72+

73+

74+type NonNullifiability :: K.Context -> Type

75+data NonNullifiability context where

76+ NNResult :: NonNullifiability Result

77+ NNReify :: NonNullifiability context -> NonNullifiability (Reify context)

78+

79+

80+nullifiableOrNot :: ()

81+ => SContext context

82+ -> Either (NonNullifiability context) (Nullifiability context)

83+nullifiableOrNot = \case

84+ SAggregate -> Right NAggregate

85+ SExpr -> Right NExpr

86+ SName -> Right NName

87+ SResult -> Left NNResult

88+ SReify context -> bimap NNReify NReify $ nullifiableOrNot context

89+

90+

91+absurd :: Nullifiability context -> NonNullifiability context -> a

92+absurd = \case

93+ NAggregate -> \case

94+ NExpr -> \case

95+ NName -> \case

96+ NReify context -> \case

97+ NNReify context' -> absurd context context'

98+

99+

100+guarder :: ()

101+ => SContext context

102+ -> Col context ('Spec tag)

103+ -> (tag -> Bool)

104+ -> (Expr tag -> Expr Bool)

105+ -> Col context ('Spec (Maybe a))

106+ -> Col context ('Spec (Maybe a))

107+guarder SAggregate (A tag) _ isNonNull (A (Aggregate a)) =

108+ A $

109+ mapInputs (toPrimExpr . run . fromPrimExpr) $

110+ Aggregate $

111+ run <$> a

112+ where

113+ mtag = foldInputs (\_ -> pure . fromPrimExpr) tag

114+ run = maybe id (sguard . isNonNull) (getFirst mtag)

115+guarder SExpr (E tag) _ isNonNull (E a) = E $ sguard condition a

116+ where

117+ condition = isNonNull tag

118+guarder SName _ _ _ name = name

119+guarder SResult (R tag) isNonNull _ (R a) = R (bool Nothing a condition)

120+ where

121+ condition = isNonNull tag

122+guarder (SReify context) (Reify tag) isNonNull isNonNullExpr (Reify a) =

123+ Reify $ guarder context tag isNonNull isNonNullExpr a

124+

125+

126+nullifier :: ()

127+ => Nullifiability context

128+ -> SSpec ('Spec a)

129+ -> Col context ('Spec a)

130+ -> Col context ('Spec (Nullify a))

131+nullifier NAggregate SSpec {nullity} (A (Aggregate a)) =

132+ A $ Aggregate $ snullify nullity <$> a

133+nullifier NExpr SSpec {nullity} (E a) = E $ snullify nullity a

134+nullifier NName _ (N (Name a)) = N $ Name a

135+nullifier (NReify context) spec (Reify a) = Reify $ nullifier context spec a

136+

137+

138+unnullifier :: ()

139+ => Nullifiability context

140+ -> SSpec ('Spec a)

141+ -> Col context ('Spec (Nullify a))

142+ -> Col context ('Spec a)

143+unnullifier NAggregate SSpec {nullity} (A (Aggregate a)) =

144+ A $ Aggregate $ sunnullify nullity <$> a

145+unnullifier NExpr SSpec {nullity} (E a) = E $ sunnullify nullity a

146+unnullifier NName _ (N (Name a)) = N $ Name a

147+unnullifier (NReify context) spec (Reify a) = Reify (unnullifier context spec a)

148+

149+

150+sguard :: Expr Bool -> Expr (Maybe a) -> Expr (Maybe a)

151+sguard condition a = boolExpr null a condition

90152 where

91153 null = fromPrimExpr $ Opaleye.ConstExpr Opaleye.NullLit

92154

src/Rel8/Schema/HTable/Nullify.hs+26−8

@@ -8,6 +8,7 @@

88{-# language LambdaCase #-}

99{-# language MultiParamTypeClasses #-}

1010{-# language NamedFieldPuns #-}

11+{-# language QuantifiedConstraints #-}

1112{-# language RankNTypes #-}

1213{-# language RecordWildCards #-}

1314{-# language ScopedTypeVariables #-}

@@ -18,15 +19,24 @@

1819module Rel8.Schema.HTable.Nullify

1920 ( HNullify( HNullify )

2021 , Nullify

21− , hnulls, hnullify, hunnullify

22+ , hguard

23+ , hnulls

24+ , hnullify

25+ , hunnullify

2226 )

2327where

2428

2529-- base

30+import GHC.Generics ( Generic )

2631import Prelude hiding ( null )

2732

2833-- rel8

34+import Rel8.FCF ( Eval, Exp )

2935import Rel8.Schema.HTable ( HTable, hfield, htabulate, htabulateA, hspecs )

36+import Rel8.Schema.HTable.MapTable

37+ ( HMapTable, HMapTableField( HMapTableField )

38+ , MapSpec, mapInfo

39+ )

3040import qualified Rel8.Schema.Kind as K

3141import Rel8.Schema.Null ( Nullity( Null, NotNull ) )

3242import qualified Rel8.Schema.Null as Type ( Nullify )

@@ -34,9 +44,6 @@ import Rel8.Schema.Spec ( Spec( Spec ), SSpec(..) )

3444

3545-- semigroupoids

3646import Data.Functor.Apply ( Apply )

37−import Rel8.Schema.HTable.MapTable

38−import Rel8.FCF

39−import GHC.Generics (Generic)

4047

4148

4249type HNullify :: K.HTable -> K.HTable

@@ -45,7 +52,6 @@ newtype HNullify table context = HNullify (HMapTable Nullify table context)

4552 deriving anyclass HTable

4653

4754

48−

4955-- | Transform a 'Spec' by allowing it to be @null@.

5056data Nullify :: Spec -> Exp Spec

5157

@@ -61,7 +67,18 @@ instance MapSpec Nullify where

6167 Null -> Null

6268 NotNull -> Null

6369 , ..

64− }

70+ }

71+

72+

73+hguard :: HTable t

74+ => (forall a. context ('Spec (Maybe a)) -> context ('Spec (Maybe a)))

75+ -> HNullify t context -> HNullify t context

76+hguard guarder (HNullify as) = HNullify $ htabulate $ \(HMapTableField field) ->

77+ case hfield hspecs field of

78+ SSpec {nullity} -> case hfield as (HMapTableField field) of

79+ a -> case nullity of

80+ Null -> guarder a

81+ NotNull -> guarder a

6582

6683

6784hnulls :: HTable t

@@ -69,8 +86,9 @@ hnulls :: HTable t

6986 => SSpec ('Spec a)

7087 -> context ('Spec (Type.Nullify a)))

7188 -> HNullify t context

72−hnulls null = HNullify $ htabulate $ \(HMapTableField field) -> case hfield hspecs field of

73− spec@SSpec {} -> null spec

89+hnulls null = HNullify $ htabulate $ \(HMapTableField field) ->

90+ case hfield hspecs field of

91+ spec@SSpec {} -> null spec

7492{-# INLINABLE hnulls #-}

7593

7694

src/Rel8/Table/Either.hs+46−41

@@ -23,25 +23,27 @@ module Rel8.Table.Either

2323where

2424

2525-- base

26−import Control.Applicative ( liftA2 )

2726import Control.Category ( id )

2827import Data.Bifunctor ( Bifunctor, bimap )

29−import Data.Functor.Identity ( runIdentity )

3028import Data.Kind ( Type )

3129import Data.Type.Equality ( apply )

3230import Prelude hiding ( id, undefined )

3331

32+-- comonad

33+import Control.Comonad ( extract )

34+

3435-- rel8

3536import Rel8.Aggregate ( Col( A ), Aggregate )

3637import Rel8.Expr ( Col( E ), Expr )

3738import Rel8.Expr.Aggregate ( groupByExpr )

3839import Rel8.Expr.Serialize ( litExpr )

39−import Rel8.Schema.Context.Nullify ( Nullifiable, nullifier, unnullifier )

40+import Rel8.Kind.Context ( Reifiable )

41+import Rel8.Schema.Context.Abstract ( Abstract )

42+import Rel8.Schema.Context.Nullify ( Nullifiable )

4043import Rel8.Schema.Dict ( Dict( Dict ) )

4144import Rel8.Schema.HTable.Either ( HEitherTable(..) )

4245import Rel8.Schema.HTable.Identity ( HIdentity(..) )

4346import Rel8.Schema.HTable.Label ( hlabel, hunlabel )

44−import Rel8.Schema.HTable.Nullify ( hnullify, hunnullify )

4547import qualified Rel8.Schema.Kind as K

4648import Rel8.Schema.Name ( Col( N ), Name )

4749import Rel8.Schema.Spec ( Spec( Spec ) )

@@ -51,6 +53,7 @@ import Rel8.Table

5153 )

5254import Rel8.Table.Bool ( bool )

5355import Rel8.Table.Eq ( EqTable, eqTable )

56+import Rel8.Table.Nullify ( Nullify, aggregateNullify, guard )

5457import Rel8.Table.Ord ( OrdTable, ordTable )

5558import Rel8.Table.Recontextualize ( Recontextualize )

5659import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )

@@ -71,19 +74,19 @@ import Data.Functor.Bind ( Bind, (>>-) )

7174type EitherTable :: K.Context -> Type -> Type -> Type

7275data EitherTable context a b = EitherTable

7376 { tag :: Col context ('Spec EitherTag)

74− , left :: a

75− , right :: b

77+ , left :: Nullify context a

78+ , right :: Nullify context b

7679 }

7780 deriving stock Functor

7881

7982

80−instance Bifunctor (EitherTable context) where

81− bimap f g (EitherTable tag a b) = EitherTable tag (f a) (g b)

83+instance Nullifiable context => Bifunctor (EitherTable context) where

84+ bimap f g (EitherTable tag a b) = EitherTable tag (fmap f a) (fmap g b)

8285

8386

8487instance (context ~ Expr, Table Expr a) => Apply (EitherTable context a) where

8588 EitherTable (E tag) l1 f <.> EitherTable (E tag') l2 a =

86− EitherTable (E (tag <> tag')) (bool l1 l2 (isLeft tag)) (f a)

89+ EitherTable (E (tag <> tag')) (bool l1 l2 (isLeft tag)) (f <.> a)

8790

8891

8992instance (context ~ Expr, Table Expr a) => Applicative (EitherTable context a) where

@@ -92,7 +95,7 @@ instance (context ~ Expr, Table Expr a) => Applicative (EitherTable context a) w

9295

9396

9497instance (context ~ Expr, Table Expr a) => Bind (EitherTable context a) where

95− EitherTable (E tag) l1 a >>- f = case f a of

98+ EitherTable (E tag) l1 a >>- f = case f (extract a) of

9699 EitherTable (E tag') l2 b ->

97100 EitherTable (E (tag <> tag')) (bool l1 l2 (isRight tag)) b

98101

@@ -109,7 +112,7 @@ instance (context ~ Expr, Table Expr a, Table Expr b) =>

109112

110113instance

111114 ( Table context a, Table context b

112− , Nullifiable context, context ~ context'

115+ , Reifiable context, Abstract context, context ~ context'

113116 )

114117 => Table context' (EitherTable context a b)

115118 where

@@ -117,29 +120,28 @@ instance

117120 type Context (EitherTable context a b) = Context a

118121

119122 toColumns EitherTable {tag, left, right} = HEitherTable

120− { htag = hlabel (HType tag)

121− , hleft = hlabel $ hnullify (nullifier tag isLeft) $ toColumns left

122− , hright = hlabel $ hnullify (nullifier tag isRight) $ toColumns right

123+ { htag = hlabel $ HType tag

124+ , hleft = hlabel $ guard tag (== IsLeft) isLeft $ toColumns left

125+ , hright = hlabel $ guard tag (== IsRight) isRight $ toColumns right

123126 }

124127

125128 fromColumns HEitherTable {htag, hleft, hright} = EitherTable

126− { tag = unHIdentity (hunlabel htag)

127− , left =

128− fromColumns $

129− runIdentity $

130− hunnullify (\spec -> pure . unnullifier spec) $

131− hunlabel

132− hleft

133− , right =

134− fromColumns $

135− runIdentity $

136− hunnullify (\spec -> pure . unnullifier spec) $

137− hunlabel

138− hright

129+ { tag = unHIdentity $ hunlabel htag

130+ , left = fromColumns $ hunlabel hleft

131+ , right = fromColumns $ hunlabel hright

139132 }

140133

141− reify = liftA2 bimap reify reify

142− unreify = liftA2 bimap unreify unreify

134+ reify proof EitherTable {tag, left, right} = EitherTable

135+ { tag

136+ , left = reify proof left

137+ , right = reify proof right

138+ }

139+

140+ unreify proof EitherTable {tag, left, right} = EitherTable

141+ { tag

142+ , left = unreify proof left

143+ , right = unreify proof right

144+ }

143145

144146 coherence = coherence @context @a

145147 congruence proof abstract =

@@ -149,8 +151,8 @@ instance

149151

150152

151153instance

152− ( Nullifiable from, from ~ from'

153− , Nullifiable to, to ~ to'

154+ ( Reifiable from, Abstract from, from ~ from'

155+ , Reifiable to, Abstract to, to ~ to'

154156 , Recontextualize from to a1 b1

155157 , Recontextualize from to a2 b2

156158 )

@@ -162,8 +164,8 @@ instance (EqTable a, EqTable b, context ~ Expr) =>

162164 where

163165 eqTable = HEitherTable

164166 { htag = hlabel (HType Dict)

165− , hleft = hlabel (hnullify (\_ Dict -> Dict) (eqTable @a))

166− , hright = hlabel (hnullify (\_ Dict -> Dict) (eqTable @b))

167+ , hleft = hlabel (eqTable @(Nullify context a))

168+ , hright = hlabel (eqTable @(Nullify context b))

167169 }

168170

169171

@@ -172,8 +174,8 @@ instance (OrdTable a, OrdTable b, context ~ Expr) =>

172174 where

173175 ordTable = HEitherTable

174176 { htag = hlabel (HType Dict)

175− , hleft = hlabel (hnullify (\_ Dict -> Dict) (ordTable @a))

176− , hright = hlabel (hnullify (\_ Dict -> Dict) (ordTable @b))

177+ , hleft = hlabel (ordTable @(Nullify context a))

178+ , hright = hlabel (ordTable @(Nullify context b))

177179 }

178180

179181

@@ -207,17 +209,17 @@ isRightTable EitherTable {tag = E tag} = isRight tag

207209eitherTable :: Table Expr c

208210 => (a -> c) -> (b -> c) -> EitherTable Expr a b -> c

209211eitherTable f g EitherTable {tag = E tag, left, right} =

210− bool (f left) (g right) (isRight tag)

212+ bool (f (extract left)) (g (extract right)) (isRight tag)

211213

212214

213215-- | Construct a left 'EitherTable'. Like 'Left'.

214216leftTable :: Table Expr b => a -> EitherTable Expr a b

215−leftTable a = EitherTable (E (litExpr IsLeft)) a undefined

217+leftTable a = EitherTable (E (litExpr IsLeft)) (pure a) undefined

216218

217219

218220-- | Construct a right 'EitherTable'. Like 'Right'.

219221rightTable :: Table Expr a => b -> EitherTable Expr a b

220−rightTable = EitherTable (E (litExpr IsRight)) undefined

222+rightTable = EitherTable (E (litExpr IsRight)) undefined . pure

221223

222224

223225-- | Lift a pair of aggregating functions to operate on an 'EitherTable'.

@@ -227,8 +229,11 @@ aggregateEitherTable :: ()

227229 -> (exprs' -> aggregates')

228230 -> EitherTable Expr exprs exprs'

229231 -> EitherTable Aggregate aggregates aggregates'

230−aggregateEitherTable f g (EitherTable (E tag) a b) =

231− EitherTable (A (groupByExpr tag)) (f a) (g b)

232+aggregateEitherTable f g (EitherTable (E tag) a b) = EitherTable

233+ { tag = A (groupByExpr tag)

234+ , left = aggregateNullify f a

235+ , right = aggregateNullify g b

236+ }

232237

233238

234239-- | Construct a 'EitherTable' in the 'Name' context. This can be useful if you

@@ -243,4 +248,4 @@ nameEitherTable

243248 -> b

244249 -- ^ Names of the columns in the @b@ table.

245250 -> EitherTable Name a b

246−nameEitherTable = EitherTable . N

251+nameEitherTable tag left right = EitherTable (N tag) (pure left) (pure right)

src/Rel8/Table/Maybe.hs+36−30

@@ -23,26 +23,30 @@ where

2323

2424-- base

2525import Control.Category ( id )

26−import Data.Functor.Identity ( runIdentity )

2726import Data.Kind ( Type )

27+import Data.Maybe ( isJust )

2828import Data.Type.Equality ( apply )

2929import Prelude hiding ( id, null, undefined )

3030

31+-- comonad

32+import Control.Comonad ( extract )

33+

3134-- rel8

3235import Rel8.Aggregate ( Col( A ), Aggregate )

3336import Rel8.Expr ( Col( E ), Expr )

3437import Rel8.Expr.Aggregate ( groupByExpr )

3538import Rel8.Expr.Bool ( boolExpr )

3639import Rel8.Expr.Null ( isNull, isNonNull, null, nullify )

37−import Rel8.Schema.Context.Nullify ( Nullifiable, nullifier, unnullifier )

40+import Rel8.Kind.Context ( Reifiable )

41+import Rel8.Schema.Context.Abstract ( Abstract )

3842import Rel8.Schema.Dict ( Dict( Dict ) )

3943import qualified Rel8.Schema.Kind as K

4044import Rel8.Schema.HTable.Identity ( HIdentity(..) )

4145import Rel8.Schema.HTable.Label ( hlabel, hunlabel )

4246import Rel8.Schema.HTable.Maybe ( HMaybeTable(..) )

43−import Rel8.Schema.HTable.Nullify ( hnullify, hunnullify )

4447import Rel8.Schema.Name ( Col( N ), Name )

45−import Rel8.Schema.Null ( Nullify, Nullity( Null, NotNull ), Sql, nullable )

48+import Rel8.Schema.Null ( Nullity( Null, NotNull ), Sql, nullable )

49+import qualified Rel8.Schema.Null as N

4650import Rel8.Schema.Spec ( Spec( Spec ) )

4751import Rel8.Table

4852 ( Table, Columns, Context, fromColumns, toColumns

@@ -55,6 +59,7 @@ import Rel8.Table.Alternative

5559import Rel8.Table.Bool ( bool )

5660import Rel8.Table.Eq ( EqTable, eqTable )

5761import Rel8.Table.Ord ( OrdTable, ordTable )

62+import Rel8.Table.Nullify ( Nullify, aggregateNullify, guard )

5863import Rel8.Table.Recontextualize ( Recontextualize )

5964import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )

6065import Rel8.Table.Undefined ( undefined )

@@ -77,14 +82,14 @@ import Data.Functor.Bind ( Bind, (>>-) )

7782type MaybeTable :: K.Context -> Type -> Type

7883data MaybeTable context a = MaybeTable

7984 { tag :: Col context ('Spec (Maybe MaybeTag))

80− , just :: a

85+ , just :: Nullify context a

8186 }

8287 deriving stock Functor

8388

8489

8590instance context ~ Expr => Apply (MaybeTable context) where

8691 MaybeTable (E tag) f <.> MaybeTable (E tag') a =

87− MaybeTable (E (tag <> tag')) (f a)

92+ MaybeTable (E (tag <> tag')) (f <.> a)

8893

8994

9095-- | Has the same behavior as the @Applicative@ instance for @Maybe@. See also:

@@ -95,7 +100,7 @@ instance context ~ Expr => Applicative (MaybeTable context) where

95100

96101

97102instance context ~ Expr => Bind (MaybeTable context) where

98− MaybeTable (E tag) a >>- f = case f a of

103+ MaybeTable (E tag) a >>- f = case f (extract a) of

99104 MaybeTable (E tag') b -> MaybeTable (E (tag <> tag')) b

100105

101106

@@ -124,34 +129,35 @@ instance (context ~ Expr, Table Expr a, Semigroup a) =>

124129 mempty = nothingTable

125130

126131

127−instance (Table context a, Nullifiable context, context ~ context') =>

128− Table context' (MaybeTable context a)

132+instance

133+ ( Table context a

134+ , Reifiable context, Abstract context, context ~ context'

135+ )

136+ => Table context' (MaybeTable context a)

129137 where

130138 type Columns (MaybeTable context a) = HMaybeTable (Columns a)

131139 type Context (MaybeTable context a) = Context a

132140

133141 toColumns MaybeTable {tag, just} = HMaybeTable

134− { htag = hlabel (HIdentity tag)

135− , hjust = hlabel $ hnullify (nullifier tag isNonNull) $ toColumns just

142+ { htag = hlabel $ HIdentity tag

143+ , hjust = hlabel $ guard tag isJust isNonNull $ toColumns just

136144 }

137145

138146 fromColumns HMaybeTable {htag, hjust} = MaybeTable

139− { tag = unHIdentity (hunlabel htag)

140− , just = fromColumns $ runIdentity $

141− hunnullify ((pure .) . unnullifier) (hunlabel hjust)

147+ { tag = unHIdentity $ hunlabel htag

148+ , just = fromColumns $ hunlabel hjust

142149 }

143150

144− reify = fmap fmap reify

145− unreify = fmap fmap unreify

146−

151+ reify proof (MaybeTable tag a) = MaybeTable tag (reify proof a)

152+ unreify proof (MaybeTable tag a) = MaybeTable tag (unreify proof a)

147153 coherence = coherence @context @a

148154 congruence proof abstract = id `apply` congruence @context @a proof abstract

149155

150156

151157instance

152− ( Nullifiable from, from ~ from'

153− , Nullifiable to, to ~ to'

154− , Recontextualize from to a b

158+ ( Recontextualize from to a b

159+ , Reifiable from, Abstract from, from ~ from'

160+ , Reifiable to, Abstract to, to ~ to'

155161 )

156162 => Recontextualize from to (MaybeTable from' a) (MaybeTable to' b)

157163

@@ -159,14 +165,14 @@ instance

159165instance (EqTable a, context ~ Expr) => EqTable (MaybeTable context a) where

160166 eqTable = HMaybeTable

161167 { htag = hlabel (HType Dict)

162− , hjust = hlabel (hnullify (\_ Dict -> Dict) (eqTable @a))

168+ , hjust = hlabel (eqTable @(Nullify context a))

163169 }

164170

165171

166172instance (OrdTable a, context ~ Expr) => OrdTable (MaybeTable context a) where

167173 ordTable = HMaybeTable

168174 { htag = hlabel (HType Dict)

169− , hjust = hlabel (hnullify (\_ Dict -> Dict) (ordTable @a))

175+ , hjust = hlabel (ordTable @(Nullify context a))

170176 }

171177

172178

@@ -192,29 +198,29 @@ isJustTable (MaybeTable (E tag) _) = isNonNull tag

192198

193199-- | Perform case analysis on a 'MaybeTable'. Like 'maybe'.

194200maybeTable :: Table Expr b => b -> (a -> b) -> MaybeTable Expr a -> b

195−maybeTable b f ma@(MaybeTable _ a) = bool (f a) b (isNothingTable ma)

201+maybeTable b f ma@(MaybeTable _ a) = bool (f (extract a)) b (isNothingTable ma)

196202{-# INLINABLE maybeTable #-}

197203

198204

199205-- | The null table. Like 'Nothing'.

200206nothingTable :: Table Expr a => MaybeTable Expr a

201−nothingTable = MaybeTable (E null) undefined

207+nothingTable = MaybeTable (E null) (pure undefined)

202208

203209

204210-- | Lift any table into 'MaybeTable'. Like 'Just'. Note you can also use

205211-- 'pure'.

206212justTable :: a -> MaybeTable Expr a

207−justTable = MaybeTable (E mempty)

213+justTable = MaybeTable (E mempty) . pure

208214

209215

210216-- | Project a single expression out of a 'MaybeTable'. You can think of this

211217-- operator like the '$' operator, but it also has the ability to return

212218-- @null@.

213219($?) :: forall a b. Sql DBType b

214− => (a -> Expr b) -> MaybeTable Expr a -> Expr (Nullify b)

220+ => (a -> Expr b) -> MaybeTable Expr a -> Expr (N.Nullify b)

215221f $? ma@(MaybeTable _ a) = case nullable @b of

216− Null -> boolExpr (f a) null (isNothingTable ma)

217− NotNull -> boolExpr (nullify (f a)) null (isNothingTable ma)

222+ Null -> boolExpr (f (extract a)) null (isNothingTable ma)

223+ NotNull -> boolExpr (nullify (f (extract a))) null (isNothingTable ma)

218224infixl 4 $?

219225

220226

@@ -225,7 +231,7 @@ aggregateMaybeTable :: ()

225231 -> MaybeTable Expr exprs

226232 -> MaybeTable Aggregate aggregates

227233aggregateMaybeTable f (MaybeTable (E tag) a) =

228− MaybeTable (A (groupByExpr tag)) (f a)

234+ MaybeTable (A (groupByExpr tag)) (aggregateNullify f a)

229235

230236

231237-- | Construct a 'MaybeTable' in the 'Name' context. This can be useful if you

@@ -238,4 +244,4 @@ nameMaybeTable

238244 -> a

239245 -- ^ Names of the columns in @a@.

240246 -> MaybeTable Name a

241−nameMaybeTable = MaybeTable . N

247+nameMaybeTable tag = MaybeTable (N tag) . pure

src/Rel8/Table/Nullify.hsnew file+204

@@ -0,0 +1,204 @@

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 #-}

10+

11+module Rel8.Table.Nullify

12+ ( Nullify

13+ , aggregateNullify

14+ , guard

15+ )

16+where

17+

18+-- base

19+import Control.Applicative ( liftA2 )

20+import Control.Category ( id )

21+import Data.Functor.Identity ( runIdentity )

22+import Data.Kind ( Type )

23+import Data.Type.Equality ( (:~:)( Refl ), apply )

24+import Prelude hiding ( id )

25+

26+-- comonad

27+import Control.Comonad ( Comonad, duplicate, extract, ComonadApply, (<@>) )

28+

29+-- rel8

30+import Rel8.Aggregate ( Aggregate )

31+import Rel8.Expr ( Expr )

32+import Rel8.Kind.Context ( Reifiable, contextSing )

33+import Rel8.Schema.Context ( Col )

34+import Rel8.Schema.Context.Abstract ( Abstract, exclusivity, virtual )

35+import Rel8.Schema.Context.Nullify

36+ ( Nullifiability( NAggregate, NExpr )

37+ , NonNullifiability( NNReify )

38+ , Nullifiable, nullifiability

39+ , nullifiableOrNot, absurd

40+ , guarder

41+ , nullifier

42+ , unnullifier

43+ )

44+import Rel8.Schema.Dict ( Dict( Dict ) )

45+import Rel8.Schema.HTable ( HTable )

46+import Rel8.Schema.HTable.Nullify ( HNullify, hnullify, hunnullify, hguard )

47+import qualified Rel8.Schema.Kind as K

48+import Rel8.Schema.Reify ( hreify, hunreify )

49+import Rel8.Schema.Spec ( Spec( Spec ) )

50+import Rel8.Table

51+ ( Table, Columns, Context, toColumns, fromColumns

52+ , reify, unreify, coherence, congruence

53+ )

54+import Rel8.Table.Eq ( EqTable, eqTable )

55+import Rel8.Table.Ord ( OrdTable, ordTable )

56+import Rel8.Table.Recontextualize ( Recontextualize )

57+

58+-- semigroupoids

59+import Data.Functor.Apply ( Apply, (<.>), liftF2 )

60+import Data.Functor.Bind ( Bind, (>>-) )

61+import Data.Functor.Extend ( Extend, duplicated )

62+

63+

64+type Nullify :: K.Context -> Type -> Type

65+data Nullify context a

66+ = Table (Nullifiability context) a

67+ | Fields (NonNullifiability context) (HNullify (Columns a) (Col (Context a)))

68+

69+

70+instance Nullifiable context => Functor (Nullify context) where

71+ fmap f = \case

72+ Table nullifiable a -> Table nullifiable (f a)

73+ Fields notNullifiable _ -> absurd nullifiability notNullifiable

74+

75+

76+instance Nullifiable context => Foldable (Nullify context) where

77+ foldMap f = \case

78+ Table _ a -> f a

79+ Fields notNullifiable _ -> absurd nullifiability notNullifiable

80+

81+

82+instance Nullifiable context => Traversable (Nullify context) where

83+ traverse f = \case

84+ Table nullifiable a -> Table nullifiable <$> f a

85+ Fields notNullifiable _ -> absurd nullifiability notNullifiable

86+

87+

88+instance 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

94+

95+

96+instance Nullifiable context => Applicative (Nullify context) where

97+ pure = Table nullifiability

98+ liftA2 = liftF2

99+

100+

101+instance Nullifiable context => Bind (Nullify context) where

102+ Table _ a >>- f = f a

103+ Fields notNullifiable _ >>- _ = absurd nullifiability notNullifiable

104+

105+

106+instance Nullifiable context => Monad (Nullify context) where

107+ (>>=) = (>>-)

108+

109+

110+instance Nullifiable context => Extend (Nullify context) where

111+ duplicated = \case

112+ Table nullifiable a -> Table nullifiable (Table nullifiable a)

113+ Fields notNullifiable _ -> absurd nullifiability notNullifiable

114+

115+

116+instance Nullifiable context => Comonad (Nullify context) where

117+ extract = \case

118+ Table _ a -> a

119+ Fields notNullifiable _ -> absurd nullifiability notNullifiable

120+ duplicate = duplicated

121+

122+

123+instance Nullifiable context => ComonadApply (Nullify context) where

124+ (<@>) = (<.>)

125+

126+

127+instance

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

135+

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)

143+

144+ toColumns = \case

145+ Table nullifiable a -> hnullify (nullifier nullifiable) (toColumns a)

146+ Fields _ a -> a

147+

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)

157+

158+ unreify proof@Refl = \case

159+ Table nullifiable a -> Table nullifiable (unreify proof a)

160+ Fields notNullifiable a -> case notNullifiable of

161+ NNReify (_ :: NonNullifiability ctx) ->

162+ case coherence @context @a proof abstract of

163+ Refl -> case congruence @context @a proof abstract of

164+ Refl -> Fields notNullifiable (hunreify a)

165+ where

166+ abstract = exclusivity (virtual @ctx)

167+

168+ coherence = coherence @context @a

169+ congruence proof abstract = id `apply` congruence @context @a proof abstract

170+

171+

172+instance

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)

178+

179+

180+instance (EqTable a, context ~ Expr) => EqTable (Nullify context a) where

181+ eqTable = hnullify (\_ Dict -> Dict) (eqTable @a)

182+

183+

184+instance (OrdTable a, context ~ Expr) => OrdTable (Nullify context a) where

185+ ordTable = hnullify (\_ Dict -> Dict) (ordTable @a)

186+

187+

188+aggregateNullify :: ()

189+ => (exprs -> aggregates)

190+ -> Nullify Expr exprs

191+ -> Nullify Aggregate aggregates

192+aggregateNullify f = \case

193+ Table _ a -> Table NAggregate (f a)

194+ Fields notNullifiable _ -> absurd NExpr notNullifiable

195+

196+

197+guard :: (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)

203+guard tag isNonNull isNonNullExpr =

204+ hguard (guarder contextSing tag isNonNull isNonNullExpr)

src/Rel8/Table/These.hs+27−32

@@ -26,11 +26,10 @@ module Rel8.Table.These

2626where

2727

2828-- base

29−import Control.Applicative ( liftA2 )

3029import Control.Category ( id )

3130import Data.Bifunctor ( Bifunctor, bimap )

32−import Data.Functor.Identity ( runIdentity )

3331import Data.Kind ( Type )

32+import Data.Maybe ( isJust )

3433import Data.Type.Equality ( apply )

3534import Prelude hiding ( id, undefined )

3635

@@ -39,11 +38,12 @@ import Rel8.Aggregate ( Aggregate )

3938import Rel8.Expr ( Expr )

4039import Rel8.Expr.Bool ( (&&.), not_ )

4140import Rel8.Expr.Null ( isNonNull )

42−import Rel8.Schema.Context.Nullify ( Nullifiable, nullifier, unnullifier )

41+import Rel8.Kind.Context ( Reifiable )

42+import Rel8.Schema.Context.Abstract ( Abstract )

43+import Rel8.Schema.Context.Nullify ( Nullifiable )

4344import Rel8.Schema.Dict ( Dict( Dict ) )

4445import Rel8.Schema.HTable.Label ( hlabel, hunlabel )

4546import Rel8.Schema.HTable.Identity ( HIdentity(..) )

46−import Rel8.Schema.HTable.Nullify ( hnullify, hunnullify )

4747import Rel8.Schema.HTable.These ( HTheseTable(..) )

4848import qualified Rel8.Schema.Kind as K

4949import Rel8.Schema.Name ( Name )

@@ -59,6 +59,7 @@ import Rel8.Table.Maybe

5959 , aggregateMaybeTable

6060 , nameMaybeTable

6161 )

62+import Rel8.Table.Nullify ( Nullify, guard )

6263import Rel8.Table.Ord ( OrdTable, ordTable )

6364import Rel8.Table.Recontextualize ( Recontextualize )

6465import Rel8.Table.Serialize ( FromExprs, ToExprs, fromResult, toResult )

@@ -88,7 +89,7 @@ data TheseTable context a b = TheseTable

8889 deriving stock Functor

8990

9091

91−instance Bifunctor (TheseTable context) where

92+instance Nullifiable context => Bifunctor (TheseTable context) where

9293 bimap f g (TheseTable a b) = TheseTable (fmap f a) (fmap g b)

9394

9495

@@ -138,7 +139,7 @@ instance (context ~ Expr, Table Expr a, Table Expr b, Semigroup a, Semigroup b)

138139

139140instance

140141 ( Table context a, Table context b

141− , Nullifiable context, context ~ context'

142+ , Reifiable context, Abstract context, context ~ context'

142143 )

143144 => Table context' (TheseTable context a b)

144145 where

@@ -146,39 +147,33 @@ instance

146147 type Context (TheseTable context a b) = Context a

147148

148149 toColumns TheseTable {here, there} = HTheseTable

149− { hhereTag = hlabel (HIdentity (tag here))

150+ { hhereTag = hlabel $ HIdentity $ tag here

150151 , hhere =

151− hlabel $ hnullify (nullifier (tag here) isNonNull) $ toColumns $

152− just here

153− , hthereTag = hlabel (HIdentity (tag there))

152+ hlabel $ guard (tag here) isJust isNonNull $ toColumns $ just here

153+ , hthereTag = hlabel $ HIdentity $ tag there

154154 , hthere =

155− hlabel $ hnullify (nullifier (tag there) isNonNull) $ toColumns $

156− just there

155+ hlabel $ guard (tag there) isJust isNonNull $ toColumns $ just there

157156 }

158157

159158 fromColumns HTheseTable {hhereTag, hhere, hthereTag, hthere} = TheseTable

160159 { here = MaybeTable

161160 { tag = unHIdentity $ hunlabel hhereTag

162− , just =

163− fromColumns $

164− runIdentity $

165− hunnullify (\a -> pure . unnullifier a) $

166− hunlabel

167− hhere

161+ , just = fromColumns $ hunlabel hhere

168162 }

169163 , there = MaybeTable

170164 { tag = unHIdentity $ hunlabel hthereTag

171− , just =

172− fromColumns $

173− runIdentity $

174− hunnullify (\a -> pure . unnullifier a) $

175− hunlabel

176− hthere

165+ , just = fromColumns $ hunlabel hthere

177166 }

178167 }

179168

180− reify = liftA2 bimap reify reify

181− unreify = liftA2 bimap unreify unreify

169+ reify proof TheseTable {here, there} = TheseTable

170+ { here = reify proof here

171+ , there = reify proof there

172+ }

173+ unreify proof TheseTable {here, there} = TheseTable

174+ { here = unreify proof here

175+ , there = unreify proof there

176+ }

182177

183178 coherence = coherence @context @a

184179 congruence proof abstract =

@@ -188,8 +183,8 @@ instance

188183

189184

190185instance

191− ( Nullifiable from, from ~ from'

192− , Nullifiable to, to ~ to'

186+ ( Reifiable from, Abstract from, from ~ from'

187+ , Reifiable to, Abstract to, to ~ to'

193188 , Recontextualize from to a1 b1

194189 , Recontextualize from to a2 b2

195190 )

@@ -201,9 +196,9 @@ instance (EqTable a, EqTable b, context ~ Expr) =>

201196 where

202197 eqTable = HTheseTable

203198 { hhereTag = hlabel (HType Dict)

204− , hhere = hlabel (hnullify (\_ Dict -> Dict) (eqTable @a))

199+ , hhere = hlabel (eqTable @(Nullify context a))

205200 , hthereTag = hlabel (HType Dict)

206− , hthere = hlabel (hnullify (\_ Dict -> Dict) (eqTable @b))

201+ , hthere = hlabel (eqTable @(Nullify context b))

207202 }

208203

209204

@@ -212,9 +207,9 @@ instance (OrdTable a, OrdTable b, context ~ Expr) =>

212207 where

213208 ordTable = HTheseTable

214209 { hhereTag = hlabel (HType Dict)

215− , hhere = hlabel (hnullify (\_ Dict -> Dict) (ordTable @a))

210+ , hhere = hlabel (ordTable @(Nullify context a))

216211 , hthereTag = hlabel (HType Dict)

217− , hthere = hlabel (hnullify (\_ Dict -> Dict) (ordTable @b))

212+ , hthere = hlabel (ordTable @(Nullify context b))

218213 }

219214

220215