git.iko.soy/rel8
on be54907 help sign in
rel8/src/Rel8/Column/NonEmpty.hs
174 lines 6.1 kB history raw
1{-# language DataKinds #-}
2{-# language FlexibleContexts #-}
3{-# language LambdaCase #-}
4{-# language MultiParamTypeClasses #-}
5{-# language ScopedTypeVariables #-}
6{-# language StandaloneKindSignatures #-}
7{-# language TypeApplications #-}
8{-# language TypeFamilyDependencies #-}
9{-# language UndecidableInstances #-}
11module Rel8.Column.NonEmpty
12 ( HNonEmpty, AHNonEmpty(..)
13 )
14where
16-- base
17import Control.Category ( id )
18import Data.Kind ( Type )
19import Data.List.NonEmpty ( NonEmpty )
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.NonEmpty ( HNonEmptyTable )
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.NonEmpty ( NonEmptyTable( NonEmptyTable ) )
39import Rel8.Table.Recontextualize ( Recontextualize )
42-- | Nest a 'NonEmpty' list within a 'Rel8able'. @HNonEmpty f a@ will produce a
43-- 'NonEmptyTable' @a@ in the 'Expr' context, and a 'NonEmpty' @a@ in the
44-- 'Result' context.
45type HNonEmpty :: K.Context -> Type -> Type
46type family HNonEmpty context = nonEmpty | nonEmpty -> context where
47 HNonEmpty (Reify context) = AHNonEmpty context
48 HNonEmpty Aggregate = NonEmptyTable Aggregate
49 HNonEmpty Expr = NonEmptyTable Expr
50 HNonEmpty Name = NonEmptyTable Name
51 HNonEmpty Result = NonEmpty
54type AHNonEmpty :: K.Context -> Type -> Type
55newtype AHNonEmpty context a = AHNonEmpty (HNonEmpty context a)
58instance (Reifiable context, Table (Reify context) a) =>
59 Table (Reify context) (AHNonEmpty context a)
60 where
61 type Context (AHNonEmpty context a) = Reify context
62 type Columns (AHNonEmpty context a) = HNonEmptyTable (Columns a)
63 type Unreify (AHNonEmpty context a) = HNonEmpty context (Unreify a)
65 fromColumns = sfromColumnsNonEmpty contextSing
66 toColumns = stoColumnsNonEmpty contextSing
68 reify _ = sreifyNonEmpty contextSing
69 unreify _ = sunreifyNonEmpty contextSing
71 coherence = case contextSing @context of
72 SAggregate -> coherence @(Reify context) @a
73 SExpr -> coherence @(Reify context) @a
74 SName -> coherence @(Reify context) @a
75 SResult -> \Refl -> absurd
76 SReify _ -> \Refl _ -> Refl
78 congruence proof@Refl abstract = case contextSing @context of
79 SAggregate -> id `apply` congruence @(Reify context) @a proof abstract
80 SExpr -> id `apply` congruence @(Reify context) @a proof abstract
81 SName -> id `apply` congruence @(Reify context) @a proof abstract
82 SResult -> absurd abstract
83 SReify _ -> id `apply` congruence @(Reify context) @a proof abstract
86instance
87 ( Reifiable context, Reifiable context'
88 , Recontextualize (Reify context) (Reify context') a a'
89 )
90 => Recontextualize
91 (Reify context)
92 (Reify context')
93 (AHNonEmpty context a)
94 (AHNonEmpty context' a')
97smapNonEmpty :: Congruent a b
98 => SContext context
99 -> (a -> b)
100 -> (HNonEmptyTable (Columns a) (Col (Context a)) -> HNonEmptyTable (Columns b) (Col (Context b)))
101 -> AHNonEmpty context a
102 -> AHNonEmpty context b
103smapNonEmpty = \case
104 SAggregate -> \_ f (AHNonEmpty (NonEmptyTable a)) -> AHNonEmpty (NonEmptyTable (f a))
105 SExpr -> \_ f (AHNonEmpty (NonEmptyTable a)) -> AHNonEmpty (NonEmptyTable (f a))
106 SResult -> \f _ (AHNonEmpty as) -> AHNonEmpty (fmap f as)
107 SName -> \_ f (AHNonEmpty (NonEmptyTable a)) -> AHNonEmpty (NonEmptyTable (f a))
108 SReify context -> \f g (AHNonEmpty as) -> AHNonEmpty (smapNonEmpty context f g as)
111sfromColumnsNonEmpty :: Table (Reify context) a
112 => SContext context
113 -> HNonEmptyTable (Columns a) (Col (Reify context))
114 -> AHNonEmpty context a
115sfromColumnsNonEmpty = \case
116 SAggregate -> AHNonEmpty . NonEmptyTable
117 SExpr -> AHNonEmpty . NonEmptyTable
118 SResult ->
119 AHNonEmpty . fmap (fromColumns . hreify) . fromColumns . hunreify
120 SName -> AHNonEmpty . NonEmptyTable
121 SReify context ->
122 AHNonEmpty .
123 smapNonEmpty context (fromColumns . hreify) hreify .
124 sfromColumnsNonEmpty context .
125 hunreify
128stoColumnsNonEmpty :: Table (Reify context) a
129 => SContext context
130 -> AHNonEmpty context a
131 -> HNonEmptyTable (Columns a) (Col (Reify context))
132stoColumnsNonEmpty = \case
133 SAggregate -> \(AHNonEmpty (NonEmptyTable a)) -> a
134 SExpr -> \(AHNonEmpty (NonEmptyTable a)) -> a
135 SResult ->
136 hreify . toColumns . fmap (hunreify . toColumns) . (\(AHNonEmpty a) -> a)
137 SName -> \(AHNonEmpty (NonEmptyTable a)) -> a
138 SReify context ->
139 hreify .
140 stoColumnsNonEmpty context .
141 smapNonEmpty context (hunreify . toColumns) hunreify .
142 (\(AHNonEmpty a) -> a)
145sreifyNonEmpty :: forall context a. Table (Reify context) a
146 => SContext context
147 -> HNonEmpty context (Unreify a)
148 -> AHNonEmpty context a
149sreifyNonEmpty context = case virtualOrResult context of
150 Left Refl -> AHNonEmpty . fmap (reify Refl)
151 Right virtual ->
152 case coherence @(Reify context) @a Refl abstract of
153 Refl -> case congruence @(Reify context) @a Refl abstract of
154 Refl ->
155 smapNonEmpty context (reify Refl) hreify .
156 AHNonEmpty
157 where
158 abstract = exclusivity virtual
161sunreifyNonEmpty :: forall context a. Table (Reify context) a
162 => SContext context
163 -> AHNonEmpty context a
164 -> HNonEmpty context (Unreify a)
165sunreifyNonEmpty context = case virtualOrResult context of
166 Left Refl -> fmap (unreify Refl) . (\(AHNonEmpty a) -> a)
167 Right virtual ->
168 case coherence @(Reify context) @a Refl abstract of
169 Refl -> case congruence @(Reify context) @a Refl abstract of
170 Refl ->
171 (\(AHNonEmpty a) -> a) .
172 smapNonEmpty context (unreify Refl) hunreify
173 where
174 abstract = exclusivity virtual