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