git.iko.soy/rel8
on 5a47018 help sign in
rel8/src/Rel8/Table.hs
452 lines 15 kB history raw
1{-# language AllowAmbiguousTypes #-}
2{-# language DataKinds #-}
3{-# language DefaultSignatures #-}
4{-# language DisambiguateRecordFields #-}
5{-# language FlexibleContexts #-}
6{-# language FlexibleInstances #-}
7{-# language FunctionalDependencies #-}
8{-# language LambdaCase #-}
9{-# language NamedFieldPuns #-}
10{-# language ScopedTypeVariables #-}
11{-# language StandaloneKindSignatures #-}
12{-# language TypeApplications #-}
13{-# language TypeFamilies #-}
14{-# language TypeOperators #-}
15{-# language UndecidableInstances #-}
17module Rel8.Table
18 ( Table
19 ( Columns, Context, toColumns, fromColumns
20 , Unreify, reify, unreify, coherence, congruence
21 )
22 , Congruent
23 , TTable, TColumns, TContext, TUnreify
24 )
25where
27-- base
28import Data.Functor ( ($>) )
29import Data.Functor.Identity ( Identity( Identity ) )
30import Data.Kind ( Constraint, Type )
31import Data.List.NonEmpty ( NonEmpty )
32import Data.Proxy ( Proxy( Proxy ) )
33import Data.Type.Equality ( (:~:)( Refl ) )
34import GHC.Generics ( Generic, Rep, from, to )
35import Prelude hiding ( null )
37-- rel8
38import Rel8.FCF ( Eval, Exp )
39import Rel8.Kind.Algebra
40 ( SAlgebra( SSum, SProduct )
41 , KnownAlgebra, algebraSing
42 )
43import Rel8.Generic.Coherence ( GCoherent, gcoherence, gcongruence )
44import Rel8.Generic.Map ( GMap, GMappable, gmap, gunmap )
45import Rel8.Generic.Table
46 ( GGTable, GGColumns, GGContext, ggfromColumns, ggtoColumns
47 , GAlgebra
48 )
49import Rel8.Generic.Record ( Record(..) )
50import Rel8.Generic.Reify ( ARep )
51import Rel8.Schema.HTable ( HTable )
52import Rel8.Schema.HTable.Either ( HEitherTable(..) )
53import Rel8.Schema.HTable.Identity ( HIdentity(..), HType )
54import Rel8.Schema.HTable.Label ( hlabel, hrelabel, hunlabel )
55import Rel8.Schema.HTable.List ( HListTable )
56import Rel8.Schema.HTable.Maybe ( HMaybeTable(..) )
57import Rel8.Schema.HTable.NonEmpty ( HNonEmptyTable )
58import Rel8.Schema.HTable.Nullify ( hnulls, hnullify, hunnullify )
59import Rel8.Schema.HTable.These ( HTheseTable(..) )
60import Rel8.Schema.HTable.Vectorize ( hvectorize, hunvectorize )
61import qualified Rel8.Schema.Kind as K
62import Rel8.Schema.Null ( Sql )
63import Rel8.Schema.Reify
64 ( Reify, Col( Reify ), hreify, hunreify
65 , UnwrapReify
66 , notReify
67 )
68import Rel8.Schema.Result
69 ( Col( R ), Result
70 , NotResult
71 , null, nullifier, unnullifier
72 , vectorizer, unvectorizer
73 )
74import Rel8.Schema.Spec ( KnownSpec )
75import Rel8.Type ( DBType )
76import Rel8.Type.Tag ( EitherTag( IsLeft, IsRight ), MaybeTag( IsJust ) )
78-- these
79import Data.These ( These( This, That, These ) )
80import Data.These.Combinators ( justHere, justThere )
83-- | @Table@s are one of the foundational elements of Rel8, and describe data
84-- types that have a finite number of columns. Each of these columns contains
85-- data under a shared context, and contexts describe how to interpret the
86-- metadata about a column to a particular Haskell type. In Rel8, we have
87-- contexts for expressions (the 'Rel8.Expr' context), aggregations (the
88-- 'Rel8.Aggregate' context), insert values (the 'Rel8.Insert' contex), among
89-- others.
90--
91-- In typical usage of Rel8 you don't need to derive instances of 'Table'
92-- yourself, as anything that's an instance of 'Rel8.Rel8able' is always a
93-- 'Table'.
94type Table :: K.Context -> Type -> Constraint
95class (HTable (Columns a), context ~ Context a) => Table context a | a -> context where
96 -- | The 'HTable' functor that describes the schema of this table.
97 type Columns a :: K.HTable
99 -- | The common context that all columns use as an interpretation.
100 type Context a :: K.Context
102 type Unreify a :: Type
104 toColumns :: a -> Columns a (Col context)
105 fromColumns :: Columns a (Col context) -> a
107 reify :: context :~: Reify ctx -> Unreify a -> a
108 unreify :: context :~: Reify ctx -> a -> Unreify a
109 coherence :: context :~: Reify ctx -> NotResult ctx -> Context (Unreify a) :~: ctx
110 congruence :: context :~: Reify ctx -> NotResult ctx -> Columns a :~: Columns (Unreify a)
113 type Columns a = Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))
114 type Context a = Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record a)))
115 type Unreify a = DefaultUnreify a
117 default toColumns ::
118 ( Generic (Record a)
119 , KnownAlgebra (GAlgebra (Rep (Record a)))
120 , Eval (GGTable (GAlgebra (Rep (Record a))) (TTable context) TColumns (Col context) (Rep (Record a)))
121 , Columns a ~ Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))
122 , Context a ~ Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record a)))
123 )
124 => a -> Columns a (Col context)
125 toColumns =
126 ggtoColumns
127 @(GAlgebra (Rep (Record a)))
128 @(TTable context)
129 @TColumns
130 id
131 id
132 toColumns .
133 from .
134 Record
136 default fromColumns ::
137 ( Generic (Record a)
138 , KnownAlgebra (GAlgebra (Rep (Record a)))
139 , Eval (GGTable (GAlgebra (Rep (Record a))) (TTable context) TColumns (Col context) (Rep (Record a)))
140 , Columns a ~ Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))
141 , Context a ~ Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record a)))
142 )
143 => Columns a (Col context) -> a
144 fromColumns =
145 unrecord .
146 to .
147 ggfromColumns
148 @(GAlgebra (Rep (Record a)))
149 @(TTable context)
150 @TColumns
151 id
152 id
153 fromColumns
155 default reify ::
156 ( Generic (Record a)
157 , Generic (Record (Unreify a))
158 , GMappable (TTable context) (Rep (Record a))
159 , Rep (Record (Unreify a)) ~ GMap TUnreify (Rep (Record a))
160 )
161 => context :~: Reify ctx -> Unreify a -> a
162 reify Refl =
163 unrecord .
164 to .
165 gunmap @(TTable context) (Proxy @TUnreify) (reify Refl) .
166 from .
167 Record
169 default unreify ::
170 ( Generic (Record a)
171 , Generic (Record (Unreify a))
172 , GMappable (TTable context) (Rep (Record a))
173 , Rep (Record (Unreify a)) ~ GMap TUnreify (Rep (Record a))
174 )
175 => context :~: Reify ctx -> a -> Unreify a
176 unreify Refl =
177 unrecord .
178 to .
179 gmap @(TTable context) (Proxy @TUnreify) (unreify Refl) .
180 from .
181 Record
183 default coherence ::
184 ( KnownAlgebra (GAlgebra (Rep (Record a)))
185 , GCoherent (TTable context) (Rep (Record a))
186 , Context a ~ Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record a)))
187 , Context (Unreify a) ~ Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record (Unreify a))))
188 , Rep (Record (Unreify a)) ~ GMap TUnreify (Rep (Record a))
189 )
190 => context :~: Reify ctx -> NotResult ctx -> Context (Unreify a) :~: ctx
191 coherence = case algebraSing @(GAlgebra (Rep (Record a))) of
192 SSum -> notReify
193 SProduct -> \proof abstract ->
194 gcoherence
195 @(TTable context)
196 @(Rep (Record a))
197 (Proxy @TContext)
198 (Proxy @TUnreify)
199 (\(_ :: _proxy x) -> coherence @context @x proof abstract)
201 default congruence ::
202 ( KnownAlgebra (GAlgebra (Rep (Record a)))
203 , GCoherent (TTable context) (Rep (Record a))
204 , Context a ~ Eval (GGContext (GAlgebra (Rep (Record a))) TContext (Rep (Record a)))
205 , Columns a ~ Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record a)))
206 , Columns (Unreify a) ~ Eval (GGColumns (GAlgebra (Rep (Record a))) TColumns (Rep (Record (Unreify a))))
207 , Rep (Record (Unreify a)) ~ GMap TUnreify (Rep (Record a))
208 )
209 => context :~: Reify ctx -> NotResult ctx -> Columns a :~: Columns (Unreify a)
210 congruence = case algebraSing @(GAlgebra (Rep (Record a))) of
211 SSum -> notReify
212 SProduct -> \proof abstract ->
213 gcongruence
214 @(TTable context)
215 @(Rep (Record a))
216 (Proxy @TColumns)
217 (Proxy @TUnreify)
218 (\(_ :: _proxy x) -> congruence @context @x proof abstract)
221data TTable :: K.Context -> Type -> Exp Constraint
222type instance Eval (TTable context a) = Table context a
225data TColumns :: Type -> Exp K.HTable
226type instance Eval (TColumns a) = Columns a
229data TContext :: Type -> Exp K.Context
230type instance Eval (TContext a) = Context a
233data TUnreify :: Type -> Exp Type
234type instance Eval (TUnreify a) = Unreify a
237type DefaultUnreify :: Type -> Type
238type family DefaultUnreify a where
239 DefaultUnreify (t a b c d e f g) =
240 t (Unreify a) (Unreify b) (Unreify c) (Unreify d) (Unreify e) (Unreify f) (Unreify g)
241 DefaultUnreify (t a b c d e f) =
242 t (Unreify a) (Unreify b) (Unreify c) (Unreify d) (Unreify e) (Unreify f)
243 DefaultUnreify (t a b c d e) =
244 t (Unreify a) (Unreify b) (Unreify c) (Unreify d) (Unreify e)
245 DefaultUnreify (t a b c d) =
246 t (Unreify a) (Unreify b) (Unreify c) (Unreify d)
247 DefaultUnreify (t a b c) = t (Unreify a) (Unreify b) (Unreify c)
248 DefaultUnreify (t a b) = t (Unreify a) (Unreify b)
249 DefaultUnreify (t a) = t (Unreify a)
250 DefaultUnreify a = ARep (GMap TUnreify (Rep a))
253-- | Any 'HTable' is also a 'Table'.
254instance HTable t => Table context (t (Col context)) where
255 type Columns (t (Col context)) = t
256 type Context (t (Col context)) = context
257 type Unreify (t (Col context)) = t (Col (UnwrapReify context))
259 toColumns = id
260 fromColumns = id
262 reify Refl = hreify
263 unreify Refl = hunreify
264 coherence Refl _ = Refl
265 congruence Refl _ = Refl
268-- | Any context is trivially a table.
269instance KnownSpec spec => Table context (Col context spec) where
270 type Columns (Col context spec) = HIdentity spec
271 type Context (Col context spec) = context
272 type Unreify (Col context spec) = Col (UnwrapReify context) spec
274 toColumns = HIdentity
275 fromColumns = unHIdentity
277 reify Refl = Reify
278 unreify Refl (Reify a) = a
279 coherence Refl _ = Refl
280 congruence Refl _ = Refl
283instance Sql DBType a => Table Result (Identity a) where
284 type Columns (Identity a) = HType a
285 type Context (Identity a) = Result
287 toColumns (Identity a) = HType (R a)
288 fromColumns (HType (R a)) = Identity a
290 reify = notReify
291 unreify = notReify
292 coherence = notReify
293 congruence = notReify
296instance (context ~ Result, Table context a, Table context b) =>
297 Table context (Either a b)
298 where
299 type Columns (Either a b) = HEitherTable (Columns a) (Columns b)
300 type Context (Either a b) = Context a
302 toColumns = \case
303 Left table -> HEitherTable
304 { htag = hlabel (HType (R IsLeft))
305 , hleft = hlabel (hnullify nullifier (toColumns table))
306 , hright = hlabel (hnulls (const null))
307 }
308 Right table -> HEitherTable
309 { htag = hlabel (HType (R IsRight))
310 , hleft = hlabel (hnulls (const null))
311 , hright = hlabel (hnullify nullifier (toColumns table))
312 }
314 fromColumns HEitherTable {htag, hleft, hright} = case hunlabel htag of
315 HType (R tag) -> case tag of
316 IsLeft -> maybe err (Left . fromColumns) $ hunnullify unnullifier (hunlabel hleft)
317 IsRight -> maybe err (Right . fromColumns) $ hunnullify unnullifier (hunlabel hright)
318 where
319 err = error "Either.fromColumns: mismatch between tag and data"
321 coherence = notReify
322 congruence = notReify
325instance (context ~ Result, Table context a) => Table context [a] where
326 type Columns [a] = HListTable (Columns a)
327 type Context [a] = Context a
329 toColumns = hvectorize vectorizer . fmap toColumns
330 fromColumns = fmap fromColumns . hunvectorize unvectorizer
332 coherence = notReify
333 congruence = notReify
336instance (context ~ Result, Table context a) => Table context (Maybe a) where
337 type Columns (Maybe a) = HMaybeTable (Columns a)
338 type Context (Maybe a) = Context a
340 toColumns = \case
341 Nothing -> HMaybeTable
342 { htag = hlabel (HIdentity (R Nothing))
343 , hjust = hlabel (hnulls (const null))
344 }
345 Just table -> HMaybeTable
346 { htag = hlabel (HIdentity (R (Just IsJust)))
347 , hjust = hlabel (hnullify nullifier (toColumns table))
348 }
350 fromColumns HMaybeTable {htag, hjust} = case hunlabel htag of
351 HType (R tag) -> tag $>
352 case hunnullify unnullifier (hunlabel hjust) of
353 Nothing -> error "Maybe.fromColumns: mismatch between tag and data"
354 Just just -> fromColumns just
356 coherence = notReify
357 congruence = notReify
360instance (context ~ Result, Table context a) => Table context (NonEmpty a)
361 where
362 type Columns (NonEmpty a) = HNonEmptyTable (Columns a)
363 type Context (NonEmpty a) = Context a
365 toColumns = hvectorize vectorizer . fmap toColumns
366 fromColumns = fmap fromColumns . hunvectorize unvectorizer
368 coherence = notReify
369 congruence = notReify
372instance (context ~ Result, Table context a, Table context b) =>
373 Table context (These a b)
374 where
375 type Columns (These a b) = HTheseTable (Columns a) (Columns b)
376 type Context (These a b) = Context a
378 toColumns tables = HTheseTable
379 { hhereTag = hrelabel hhereTag
380 , hhere = hrelabel (toColumns hhere)
381 , hthereTag = hrelabel hthereTag
382 , hthere = hrelabel (toColumns hthere)
383 }
384 where
385 HMaybeTable
386 { htag = hhereTag
387 , hjust = hhere
388 } = toColumns (justHere tables)
389 HMaybeTable
390 { htag = hthereTag
391 , hjust = hthere
392 } = toColumns (justThere tables)
394 fromColumns HTheseTable {hhereTag, hhere, hthereTag, hthere} =
395 case (fromColumns mhere, fromColumns mthere) of
396 (Just a, Nothing) -> This (fromColumns a)
397 (Nothing, Just b) -> That (fromColumns b)
398 (Just a, Just b) -> These (fromColumns a) (fromColumns b)
399 _ -> error "These.fromColumns: mismatch between tags and data"
400 where
401 mhere = HMaybeTable
402 { htag = hrelabel hhereTag
403 , hjust = hrelabel hhere
404 }
405 mthere = HMaybeTable
406 { htag = hrelabel hthereTag
407 , hjust = hrelabel hthere
408 }
410 coherence = notReify
411 congruence = notReify
414instance (Table context a, Table context b) => Table context (a, b)
417instance
418 ( Table context a, Table context b, Table context c
419 )
420 => Table context (a, b, c)
423instance
424 ( Table context a, Table context b, Table context c, Table context d
425 )
426 => Table context (a, b, c, d)
429instance
430 ( Table context a, Table context b, Table context c, Table context d
431 , Table context e
432 )
433 => Table context (a, b, c, d, e)
436instance
437 ( Table context a, Table context b, Table context c, Table context d
438 , Table context e, Table context f
439 )
440 => Table context (a, b, c, d, e, f)
443instance
444 ( Table context a, Table context b, Table context c, Table context d
445 , Table context e, Table context f, Table context g
446 )
447 => Table context (a, b, c, d, e, f, g)
450type Congruent :: Type -> Type -> Constraint
451class Columns a ~ Columns b => Congruent a b
452instance Columns a ~ Columns b => Congruent a b