git.iko.soy/rel8
on be54907 help sign in
rel8/src/Rel8/Column/ADT.hs
106 lines 3.0 kB history raw
1{-# language DataKinds #-}
2{-# language LambdaCase #-}
3{-# language MultiParamTypeClasses #-}
4{-# language ScopedTypeVariables #-}
5{-# language StandaloneKindSignatures #-}
6{-# language TypeApplications #-}
7{-# language TypeFamilies #-}
8{-# language UndecidableInstances #-}
10module Rel8.Column.ADT
11 ( HADT, AHADT(..)
12 )
13where
15-- base
16import Data.Kind ( Type )
17import Data.Type.Equality ( (:~:)( Refl ) )
18import Prelude
20-- rel8
21import Rel8.Generic.Rel8able ( GColumns )
22import Rel8.Kind.Context ( SContext(..), Reifiable, contextSing )
23import Rel8.Schema.Context ( Col )
24import qualified Rel8.Schema.Kind as K
25import Rel8.Schema.Reify ( Reify, hreify, hunreify )
26import Rel8.Schema.Result ( Result, absurd )
27import Rel8.Table
28 ( Table, Columns, Context, fromColumns, toColumns
29 , Unreify, reify, unreify, coherence, congruence
30 )
31import Rel8.Table.ADT ( ADT( ADT ), ADTable, fromADT, toADT )
32import Rel8.Table.Rel8able ()
33import Rel8.Table.Recontextualize ( Recontextualize )
36type HADT :: K.Context -> K.Rel8able -> Type
37type family HADT context t where
38 HADT (Reify context) t = AHADT context t
39 HADT Result t = t Result
40 HADT context t = ADT t context
43type AHADT :: K.Context -> K.Rel8able -> Type
44newtype AHADT context t = AHADT (HADT context t)
47instance (ADTable t, Reifiable context) =>
48 Table (Reify context) (AHADT context t)
49 where
50 type Context (AHADT context t) = Reify context
51 type Columns (AHADT context t) = GColumns (ADT t)
52 type Unreify (AHADT context t) = HADT context t
54 fromColumns = sfromColumnsADT contextSing
55 toColumns = stoColumnsADT contextSing
56 reify _ = AHADT
57 unreify _ (AHADT a) = a
59 coherence = case contextSing @context of
60 SAggregate -> \Refl _ -> Refl
61 SExpr -> \Refl _ -> Refl
62 SName -> \Refl _ -> Refl
63 SResult -> \Refl -> absurd
64 SReify _ -> \Refl _ -> Refl
66 congruence = case contextSing @context of
67 SAggregate -> \_ _ -> Refl
68 SExpr -> \_ _ -> Refl
69 SName -> \_ _ -> Refl
70 SResult -> \Refl -> absurd
71 SReify _ -> \_ _ -> Refl
74instance
75 ( Reifiable context, Reifiable context'
76 , ADTable t, t ~ t'
77 )
78 => Recontextualize
79 (Reify context)
80 (Reify context')
81 (AHADT context t)
82 (AHADT context' t')
85sfromColumnsADT :: ADTable t
86 => SContext context
87 -> GColumns (ADT t) (Col (Reify context))
88 -> AHADT context t
89sfromColumnsADT = \case
90 SAggregate -> AHADT . ADT . hunreify
91 SExpr -> AHADT . ADT . hunreify
92 SName -> AHADT . ADT . hunreify
93 SResult -> AHADT . fromADT . ADT . hunreify
94 SReify context -> AHADT . sfromColumnsADT context . hunreify
97stoColumnsADT :: ADTable t
98 => SContext context
99 -> AHADT context t
100 -> GColumns (ADT t) (Col (Reify context))
101stoColumnsADT = \case
102 SAggregate -> hreify . (\(AHADT (ADT a)) -> a)
103 SExpr -> hreify . (\(AHADT (ADT a)) -> a)
104 SName -> hreify . (\(AHADT (ADT a)) -> a)
105 SResult -> hreify . (\(ADT a) -> a) . toADT . (\(AHADT a) -> a)
106 SReify context -> hreify . stoColumnsADT context . (\(AHADT a) -> a)