git.iko.soy/rel8
on be54907 help sign in
rel8/src/Rel8/Column/Maybe.hs
145 lines 4.8 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.Maybe
13 ( HMaybe, AHMaybe(..)
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.HTable.Maybe ( HMaybeTable )
29import qualified Rel8.Schema.Kind as K
30import Rel8.Schema.Name ( Name )
31import Rel8.Schema.Reify ( Reify, hreify, hunreify )
32import Rel8.Schema.Result ( Result, absurd )
33import Rel8.Table
34 ( Table, Columns, Context, fromColumns, toColumns
35 , Unreify, reify, unreify, coherence, congruence
36 )
37import Rel8.Table.Maybe ( MaybeTable )
38import Rel8.Table.Recontextualize ( Recontextualize )
41-- | Nest a 'Maybe' value within a 'Rel8able'. @HMaybe f a@ will produce a
42-- 'MaybeTable' @a@ in the 'Expr' context, and a 'Maybe' @a@ in the 'Result'
43-- context.
44type HMaybe :: K.Context -> Type -> Type
45type family HMaybe context = maybe | maybe -> context where
46 HMaybe (Reify context) = AHMaybe context
47 HMaybe Aggregate = MaybeTable Aggregate
48 HMaybe Expr = MaybeTable Expr
49 HMaybe Name = MaybeTable Name
50 HMaybe Result = Maybe
53type AHMaybe :: K.Context -> Type -> Type
54newtype AHMaybe context a = AHMaybe (HMaybe context a)
57instance Reifiable context => Functor (AHMaybe context) where
58 fmap = smapMaybe contextSing
61instance (Reifiable context, Table (Reify context) a) =>
62 Table (Reify context) (AHMaybe context a)
63 where
64 type Context (AHMaybe context a) = Reify context
65 type Columns (AHMaybe context a) = HMaybeTable (Columns a)
66 type Unreify (AHMaybe context a) = HMaybe context (Unreify a)
68 fromColumns = sfromColumnsMaybe contextSing
69 toColumns = stoColumnsMaybe contextSing
70 reify proof = fmap fmap reify proof . AHMaybe
71 unreify proof = (\(AHMaybe a) -> a) . fmap fmap unreify proof
73 coherence = case contextSing @context of
74 SAggregate -> coherence @(Reify context) @a
75 SExpr -> coherence @(Reify context) @a
76 SName -> coherence @(Reify context) @a
77 SResult -> \Refl -> absurd
78 SReify _ -> \Refl _ -> Refl
80 congruence proof@Refl abstract = case contextSing @context of
81 SAggregate -> id `apply` congruence @(Reify context) @a proof abstract
82 SExpr -> id `apply` congruence @(Reify context) @a proof abstract
83 SName -> id `apply` congruence @(Reify context) @a proof abstract
84 SResult -> absurd abstract
85 SReify _ -> id `apply` congruence @(Reify context) @a proof abstract
88instance
89 ( Reifiable context, Reifiable context'
90 , Recontextualize (Reify context) (Reify context') a a'
91 )
92 => Recontextualize
93 (Reify context)
94 (Reify context')
95 (AHMaybe context a)
96 (AHMaybe context' a')
99smapMaybe :: ()
100 => SContext context
101 -> (a -> b)
102 -> AHMaybe context a
103 -> AHMaybe context b
104smapMaybe = \case
105 SAggregate -> \f (AHMaybe a) -> AHMaybe (fmap f a)
106 SExpr -> \f (AHMaybe a) -> AHMaybe (fmap f a)
107 SResult -> \f (AHMaybe a) -> AHMaybe (fmap f a)
108 SName -> \f (AHMaybe a) -> AHMaybe (fmap f a)
109 SReify context -> \f (AHMaybe a) -> AHMaybe (smapMaybe context f a)
112sfromColumnsMaybe :: Table (Reify context) a
113 => SContext context
114 -> HMaybeTable (Columns a) (Col (Reify context))
115 -> AHMaybe context a
116sfromColumnsMaybe = \case
117 SAggregate -> AHMaybe . fmap (fromColumns . hreify) . fromColumns . hunreify
118 SExpr -> AHMaybe . fmap (fromColumns . hreify) . fromColumns . hunreify
119 SResult -> AHMaybe . fmap (fromColumns . hreify) . fromColumns . hunreify
120 SName -> AHMaybe . fmap (fromColumns . hreify) . fromColumns . hunreify
121 SReify context ->
122 AHMaybe .
123 smapMaybe context (fromColumns . hreify) .
124 sfromColumnsMaybe context .
125 hunreify
128stoColumnsMaybe :: Table (Reify context) a
129 => SContext context
130 -> AHMaybe context a
131 -> HMaybeTable (Columns a) (Col (Reify context))
132stoColumnsMaybe = \case
133 SAggregate ->
134 hreify . toColumns . fmap (hunreify . toColumns) . (\(AHMaybe a) -> a)
135 SExpr ->
136 hreify . toColumns . fmap (hunreify . toColumns) . (\(AHMaybe a) -> a)
137 SResult ->
138 hreify . toColumns . fmap (hunreify . toColumns) . (\(AHMaybe a) -> a)
139 SName ->
140 hreify . toColumns . fmap (hunreify . toColumns) . (\(AHMaybe a) -> a)
141 SReify context ->
142 hreify .
143 stoColumnsMaybe context .
144 smapMaybe context (hunreify . toColumns) .
145 (\(AHMaybe a) -> a)