git.iko.soy/rel8
on bdf2d87 help sign in
rel8/src/Rel8/Table/Unreify.hs
106 lines 3.4 kB history raw
1{-# language DataKinds #-}
2{-# language FlexibleContexts #-}
3{-# language FlexibleInstances #-}
4{-# language GADTs #-}
5{-# language LambdaCase #-}
6{-# language MultiParamTypeClasses #-}
7{-# language QuantifiedConstraints #-}
8{-# language RankNTypes #-}
9{-# language StandaloneKindSignatures #-}
10{-# language TypeFamilies #-}
11{-# language UndecidableInstances #-}
13-- | This module implements some machinery for implementing methods of the
14-- 'Table' class for a particular special (but important) class of polymorphic
15-- @Table@ types.
16--
17-- This special case is characterised by a @newtype@ wrapper around a bare
18-- 'HTable' which is constructed by applying a type family to the polymorphic
19-- type variable.
20--
21-- Examples of this class of @Table@ include @ListTable@ and @NonEmptyTable@.
22--
23-- The tricky part about implementing @Table@ for these types is 'reify' and
24-- 'unreify'. There is no guarantee in general that @'Unreify' a@ is itself
25-- a @Table@, let alone a @Table@ with the same 'Columns' as @a@
26-- (e.g., @Unreify (AColumn Result Bool) = Bool@, and @Bool@ is not a
27-- @Table@)
29module Rel8.Table.Unreify
30 ( Unreifiable, Unreifiability(..), unreifiability
31 , Unreifies
32 )
33where
35-- base
36import Data.Kind ( Constraint, Type )
37import Prelude ()
39-- rel8
40import Rel8.Aggregate ( Aggregate )
41import Rel8.Expr ( Expr )
42import Rel8.Kind.Context ( SContext(..), Reifiable, sReifiable )
43import Rel8.Schema.Dict ( Dict( Dict ) )
44import Rel8.Schema.Insert ( Insert )
45import qualified Rel8.Schema.Kind as K
46import Rel8.Schema.Name ( Name )
47import Rel8.Schema.Reify ( Reify )
48import Rel8.Schema.Result ( Result )
49import Rel8.Table ( Table, Context, Congruent, Unreify )
52type Unreifies :: K.Context -> Type -> Constraint
53type family Unreifies context a where
54 Unreifies (Reify context) a = Unreifier context a
55 Unreifies _ _ = ()
58type Unreifiable :: Type -> Constraint
59class
60 ( Context a ~ Reify Aggregate => Unreifier Aggregate a
61 , Context a ~ Reify Expr => Unreifier Expr a
62 , Context a ~ Reify Insert => Unreifier Insert a
63 , Context a ~ Reify Name => Unreifier Name a
64 , (forall ctx. (Context a ~ Reify (Reify ctx), Reifiable ctx) => Unreifier (Reify ctx) a)
65 )
66 => Unreifiable a
67instance
68 ( Context a ~ Reify Aggregate => Unreifier Aggregate a
69 , Context a ~ Reify Expr => Unreifier Expr a
70 , Context a ~ Reify Insert => Unreifier Insert a
71 , Context a ~ Reify Name => Unreifier Name a
72 , (forall ctx. (Context a ~ Reify (Reify ctx), Reifiable ctx) => Unreifier (Reify ctx) a)
73 )
74 => Unreifiable a
77type Unreifier :: K.Context -> Type -> Constraint
78class
79 ( Table context (Unreify a)
80 , Congruent a (Unreify a)
81 )
82 => Unreifier context a
83instance
84 ( Table context (Unreify a)
85 , Congruent a (Unreify a)
86 )
87 => Unreifier context a
90type Unreifiability :: K.Context -> Type -> Type
91data Unreifiability context a where
92 UResult :: Unreifiability Result a
93 Unreifiability :: Unreifier context a
94 => SContext context -> Unreifiability context a
97unreifiability :: (Context a ~ Reify context, Unreifiable a)
98 => SContext context -> Unreifiability context a
99unreifiability = \case
100 SAggregate -> Unreifiability SAggregate
101 SExpr -> Unreifiability SExpr
102 SInsert -> Unreifiability SInsert
103 SName -> Unreifiability SName
104 SResult -> UResult
105 SReify context -> case sReifiable context of
106 Dict -> Unreifiability (SReify context)