git.iko.soy/rel8
on 5a47018 help sign in
rel8/src/Rel8/Column/List.hs
172 lines 5.6 kB history raw
1{-# language DataKinds #-}
2{-# language FlexibleContexts #-}
3{-# language LambdaCase #-}
4{-# language MultiParamTypeClasses #-}
5{-# language RankNTypes #-}
6{-# language ScopedTypeVariables #-}
7{-# language StandaloneKindSignatures #-}
8{-# language TypeApplications #-}
9{-# language TypeFamilyDependencies #-}
10{-# language UndecidableInstances #-}
12module Rel8.Column.List
13 ( HList, AHList(..)
14 )
15where
17-- base
18import Control.Category ( id )
19import Data.Kind ( Type )
20import Data.Type.Equality ( (:~:)( Refl ), apply )
21import Prelude hiding ( id )
23-- rel8
24import Rel8.Aggregate ( Aggregate )
25import Rel8.Expr ( Expr )
26import Rel8.Kind.Context ( SContext(..), Reifiable( contextSing ) )
27import Rel8.Schema.Context ( Col )
28import Rel8.Schema.Context.Abstract ( exclusivity, virtualOrResult )
29import Rel8.Schema.HTable.List ( HListTable )
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, Congruent, Context, fromColumns, toColumns
36 , Unreify, reify, unreify, coherence, congruence
37 )
38import Rel8.Table.List ( ListTable( ListTable ) )
39import Rel8.Table.Recontextualize ( Recontextualize )
42-- | Nest a list within a 'Rel8able'. @HList f a@ will produce a 'ListTable'
43-- @a@ in the 'Expr' context, and a @[a]@ in the 'Result' context.
44type HList :: K.Context -> Type -> Type
45type family HList context = list | list -> context where
46 HList (Reify context) = AHList context
47 HList Aggregate = ListTable Aggregate
48 HList Expr = ListTable Expr
49 HList Name = ListTable Name
50 HList Result = []
53type AHList :: K.Context -> Type -> Type
54newtype AHList context a = AHList (HList context a)
57instance (Reifiable context, Table (Reify context) a) =>
58 Table (Reify context) (AHList context a)
59 where
60 type Context (AHList context a) = Reify context
61 type Columns (AHList context a) = HListTable (Columns a)
62 type Unreify (AHList context a) = HList context (Unreify a)
64 fromColumns = sfromColumnsList contextSing
65 toColumns = stoColumnsList contextSing
67 reify _ = sreifyList contextSing
68 unreify _ = sunreifyList contextSing
70 coherence = case contextSing @context of
71 SAggregate -> coherence @(Reify context) @a
72 SExpr -> coherence @(Reify context) @a
73 SName -> coherence @(Reify context) @a
74 SResult -> \Refl -> absurd
75 SReify _ -> \Refl _ -> Refl
77 congruence proof@Refl abstract = case contextSing @context of
78 SAggregate -> id `apply` congruence @(Reify context) @a proof abstract
79 SExpr -> id `apply` congruence @(Reify context) @a proof abstract
80 SName -> id `apply` congruence @(Reify context) @a proof abstract
81 SResult -> absurd abstract
82 SReify _ -> id `apply` congruence @(Reify context) @a proof abstract
85instance
86 ( Reifiable context, Reifiable context'
87 , Recontextualize (Reify context) (Reify context') a a'
88 )
89 => Recontextualize
90 (Reify context)
91 (Reify context')
92 (AHList context a)
93 (AHList context' a')
96smapList :: Congruent a b
97 => SContext context
98 -> (a -> b)
99 -> (HListTable (Columns a) (Col (Context a)) -> HListTable (Columns b) (Col (Context b)))
100 -> AHList context a
101 -> AHList context b
102smapList = \case
103 SAggregate -> \_ f (AHList (ListTable a)) -> AHList (ListTable (f a))
104 SExpr -> \_ f (AHList (ListTable a)) -> AHList (ListTable (f a))
105 SResult -> \f _ (AHList as) -> AHList (fmap f as)
106 SName -> \_ f (AHList (ListTable a)) -> AHList (ListTable (f a))
107 SReify context -> \f g (AHList as) -> AHList (smapList context f g as)
110sfromColumnsList :: Table (Reify context) a
111 => SContext context
112 -> HListTable (Columns a) (Col (Reify context))
113 -> AHList context a
114sfromColumnsList = \case
115 SAggregate -> AHList . ListTable
116 SExpr -> AHList . ListTable
117 SResult -> AHList . fmap (fromColumns . hreify) . fromColumns . hunreify
118 SName -> AHList . ListTable
119 SReify context ->
120 AHList .
121 smapList context (fromColumns . hreify) hreify .
122 sfromColumnsList context .
123 hunreify
126stoColumnsList :: Table (Reify context) a
127 => SContext context
128 -> AHList context a
129 -> HListTable (Columns a) (Col (Reify context))
130stoColumnsList = \case
131 SAggregate -> \(AHList (ListTable a)) -> a
132 SExpr -> \(AHList (ListTable a)) -> a
133 SResult ->
134 hreify . toColumns . fmap (hunreify . toColumns) . (\(AHList a) -> a)
135 SName -> \(AHList (ListTable a)) -> a
136 SReify context ->
137 hreify .
138 stoColumnsList context .
139 smapList context (hunreify . toColumns) hunreify .
140 (\(AHList a) -> a)
143sreifyList :: forall context a. Table (Reify context) a
144 => SContext context
145 -> HList context (Unreify a)
146 -> AHList context a
147sreifyList context = case virtualOrResult context of
148 Left Refl -> AHList . fmap (reify Refl)
149 Right virtual ->
150 case coherence @(Reify context) @a Refl abstract of
151 Refl -> case congruence @(Reify context) @a Refl abstract of
152 Refl ->
153 smapList context (reify Refl) hreify .
154 AHList
155 where
156 abstract = exclusivity virtual
159sunreifyList :: forall context a. Table (Reify context) a
160 => SContext context
161 -> AHList context a
162 -> HList context (Unreify a)
163sunreifyList context = case virtualOrResult context of
164 Left Refl -> fmap (unreify Refl) . (\(AHList a) -> a)
165 Right virtual ->
166 case coherence @(Reify context) @a Refl abstract of
167 Refl -> case congruence @(Reify context) @a Refl abstract of
168 Refl ->
169 (\(AHList a) -> a) .
170 smapList context (unreify Refl) hunreify
171 where
172 abstract = exclusivity virtual