git.iko.soy/rel8
on 5a47018 help sign in
rel8/src/Rel8/Column/Either.hs
192 lines 5.9 kB history raw
1{-# language DataKinds #-}
2{-# language FlexibleContexts #-}
3{-# language LambdaCase #-}
4{-# language MultiParamTypeClasses #-}
5{-# language ScopedTypeVariables #-}
6{-# language StandaloneKindSignatures #-}
7{-# language TypeApplications #-}
8{-# language TypeFamilyDependencies #-}
9{-# language UndecidableInstances #-}
11module Rel8.Column.Either
12 ( HEither, AHEither(..)
13 )
14where
16-- base
17import Control.Applicative ( liftA2 )
18import Control.Category ( id )
19import Data.Bifunctor ( Bifunctor, bimap )
20import Data.Kind ( Type )
21import Data.Type.Equality ( (:~:)( Refl ), apply )
22import Prelude hiding ( id )
24-- rel8
25import Rel8.Aggregate ( Aggregate )
26import Rel8.Expr ( Expr )
27import Rel8.Kind.Context ( SContext(..), Reifiable( contextSing ) )
28import Rel8.Schema.Context ( Col )
29import Rel8.Schema.HTable.Either ( HEitherTable )
30import qualified Rel8.Schema.Kind as K
31import Rel8.Schema.Name ( Name(..) )
32import Rel8.Schema.Reify ( Reify, hreify, hunreify )
33import Rel8.Schema.Result ( Result, absurd )
34import Rel8.Table
35 ( Table, Columns, Context, fromColumns, toColumns
36 , Unreify, reify, unreify, coherence, congruence
37 )
38import Rel8.Table.Either ( EitherTable )
39import Rel8.Table.Recontextualize ( Recontextualize )
42-- | Nest an 'Either' value within a 'Rel8able'. @HEither f a b@ will produce a
43-- 'EitherTable' @a b@ in the 'Expr' context, and a 'Either' @a b@ in the
44-- 'Result' context.
45type HEither :: K.Context -> Type -> Type -> Type
46type family HEither context = either | either -> context where
47 HEither (Reify context) = AHEither context
48 HEither Aggregate = EitherTable Aggregate
49 HEither Expr = EitherTable Expr
50 HEither Name = EitherTable Name
51 HEither Result = Either
54type AHEither :: K.Context -> Type -> Type -> Type
55newtype AHEither context a b = AHEither (HEither context a b)
58instance Reifiable context => Bifunctor (AHEither context) where
59 bimap = sbimapEither contextSing
62instance Reifiable context => Functor (AHEither context a) where
63 fmap = bimap id
66instance (Reifiable context, Table (Reify context) a, Table (Reify context) b)
67 => Table (Reify context) (AHEither context a b)
68 where
69 type Context (AHEither context a b) = Reify context
70 type Columns (AHEither context a b) = HEitherTable (Columns a) (Columns b)
71 type Unreify (AHEither context a b) = HEither context (Unreify a) (Unreify b)
73 fromColumns = sfromColumnsEither contextSing
74 toColumns = stoColumnsEither contextSing
75 reify proof = liftA2 bimap reify reify proof . AHEither
76 unreify proof = (\(AHEither a) -> a) . liftA2 bimap unreify unreify proof
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
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
105instance
106 ( Reifiable context, Reifiable context'
107 , Recontextualize (Reify context) (Reify context') a a'
108 , Recontextualize (Reify context) (Reify context') b b'
109 ) =>
110 Recontextualize
111 (Reify context)
112 (Reify context')
113 (AHEither context a b)
114 (AHEither context' a' b')
117sbimapEither :: ()
118 => SContext context
119 -> (a -> c)
120 -> (b -> d)
121 -> AHEither context a b
122 -> AHEither context c d
123sbimapEither = \case
124 SAggregate -> \f g (AHEither a) -> AHEither (bimap f g a)
125 SExpr -> \f g (AHEither a) -> AHEither (bimap f g a)
126 SResult -> \f g (AHEither a) -> AHEither (bimap f g a)
127 SName -> \f g (AHEither a) -> AHEither (bimap f g a)
128 SReify context -> \f g (AHEither a) -> AHEither (sbimapEither context f g a)
131sfromColumnsEither :: (Table (Reify context) a, Table (Reify context) b)
132 => SContext context
133 -> HEitherTable (Columns a) (Columns b) (Col (Reify context))
134 -> AHEither context a b
135sfromColumnsEither = \case
136 SAggregate ->
137 AHEither .
138 bimap (fromColumns . hreify) (fromColumns . hreify) .
139 fromColumns .
140 hunreify
141 SExpr ->
142 AHEither .
143 bimap (fromColumns . hreify) (fromColumns . hreify) .
144 fromColumns .
145 hunreify
146 SResult ->
147 AHEither .
148 bimap (fromColumns . hreify) (fromColumns . hreify) .
149 fromColumns .
150 hunreify
151 SName ->
152 AHEither .
153 bimap (fromColumns . hreify) (fromColumns . hreify) .
154 fromColumns .
155 hunreify
156 SReify context ->
157 AHEither .
158 sbimapEither context (fromColumns . hreify) (fromColumns . hreify) .
159 sfromColumnsEither context .
160 hunreify
163stoColumnsEither :: (Table (Reify context) a, Table (Reify context) b)
164 => SContext context
165 -> AHEither context a b
166 -> HEitherTable (Columns a) (Columns b) (Col (Reify context))
167stoColumnsEither = \case
168 SAggregate ->
169 hreify .
170 toColumns .
171 bimap (hunreify . toColumns) (hunreify . toColumns) .
172 (\(AHEither a) -> a)
173 SExpr ->
174 hreify .
175 toColumns .
176 bimap (hunreify . toColumns) (hunreify . toColumns) .
177 (\(AHEither a) -> a)
178 SResult ->
179 hreify .
180 toColumns .
181 bimap (hunreify . toColumns) (hunreify . toColumns) .
182 (\(AHEither a) -> a)
183 SName ->
184 hreify .
185 toColumns .
186 bimap (hunreify . toColumns) (hunreify . toColumns) .
187 (\(AHEither a) -> a)
188 SReify context ->
189 hreify .
190 stoColumnsEither context .
191 sbimapEither context (hunreify . toColumns) (hunreify . toColumns) .
192 (\(AHEither a) -> a)