git.iko.soy/rel8
on 5a47018 help sign in
rel8/src/Rel8/Column/Lift.hs
104 lines 2.9 kB history raw
1{-# language DataKinds #-}
2{-# language LambdaCase #-}
3{-# language MultiParamTypeClasses #-}
4{-# language ScopedTypeVariables #-}
5{-# language StandaloneKindSignatures #-}
6{-# language TypeApplications #-}
7{-# language TypeFamilies #-}
9module Rel8.Column.Lift
10 ( Lift, ALift(..)
11 )
12where
14-- base
15import Data.Kind ( Type )
16import Data.Type.Equality ( (:~:)( Refl ) )
17import Prelude
19-- rel8
20import Rel8.Generic.Rel8able ( GColumns )
21import Rel8.Kind.Context ( Reifiable(..), SContext(..) )
22import Rel8.Schema.Context ( Col )
23import qualified Rel8.Schema.Kind as K
24import Rel8.Schema.Reify ( Reify, hreify, hunreify )
25import Rel8.Schema.Result ( Result, absurd )
26import Rel8.Table
27 ( Table, Columns, Context, fromColumns, toColumns
28 , Unreify, reify, unreify, coherence, congruence
29 )
30import Rel8.Table.Rel8able ()
31import Rel8.Table.HKD ( HKD( HKD ), HKDable, fromHKD, toHKD )
32import Rel8.Table.Recontextualize ( Recontextualize )
35type Lift :: K.Context -> Type -> Type
36type family Lift context a where
37 Lift (Reify context) a = ALift context a
38 Lift Result a = a
39 Lift context a = HKD a context
42type ALift :: K.Context -> Type -> Type
43newtype ALift context a = ALift
44 { unALift :: Lift context a
45 }
48instance (Reifiable context, HKDable a) =>
49 Table (Reify context) (ALift context a)
50 where
51 type Context (ALift context a) = Reify context
52 type Columns (ALift context a) = GColumns (HKD a)
53 type Unreify (ALift context a) = Lift context a
55 fromColumns = sfromColumnsLift contextSing
56 toColumns = stoColumnsLift contextSing
57 reify _ = ALift
58 unreify _ (ALift a) = a
60 coherence = case contextSing @context of
61 SAggregate -> \Refl _ -> Refl
62 SExpr -> \Refl _ -> Refl
63 SName -> \Refl _ -> Refl
64 SResult -> \Refl -> absurd
65 SReify _ -> \Refl _ -> Refl
67 congruence = case contextSing @context of
68 SAggregate -> \_ _ -> Refl
69 SExpr -> \_ _ -> Refl
70 SName -> \_ _ -> Refl
71 SResult -> \Refl -> absurd
72 SReify _ -> \_ _ -> Refl
75instance (Reifiable context, Reifiable context', HKDable a) =>
76 Recontextualize
77 (Reify context)
78 (Reify context')
79 (ALift context a)
80 (ALift context' a)
83sfromColumnsLift :: HKDable a
84 => SContext context
85 -> GColumns (HKD a) (Col (Reify context))
86 -> ALift context a
87sfromColumnsLift = \case
88 SAggregate -> ALift . fromColumns . hunreify
89 SExpr -> ALift . fromColumns . hunreify
90 SName -> ALift . fromColumns . hunreify
91 SResult -> ALift . fromHKD . HKD . hunreify
92 SReify context -> ALift . sfromColumnsLift context . hunreify
95stoColumnsLift :: HKDable a
96 => SContext context
97 -> ALift context a
98 -> GColumns (HKD a) (Col (Reify context))
99stoColumnsLift = \case
100 SAggregate -> hreify . toColumns . unALift
101 SExpr -> hreify . toColumns . unALift
102 SName -> hreify . toColumns . unALift
103 SResult -> hreify . (\(HKD a) -> a) . toHKD . unALift
104 SReify context -> hreify . stoColumnsLift context . unALift