git.iko.soy/rel8
on 2ba99ea help sign in
rel8/src/Rel8/Table/Unreify.hs
102 lines 3.2 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 qualified Rel8.Schema.Kind as K
45import Rel8.Schema.Name ( Name )
46import Rel8.Schema.Reify ( Reify )
47import Rel8.Schema.Result ( Result )
48import Rel8.Table ( Table, Context, Congruent, Unreify )
51type Unreifies :: K.Context -> Type -> Constraint
52type family Unreifies context a where
53 Unreifies (Reify context) a = Unreifier context a
54 Unreifies _ _ = ()
57type Unreifiable :: Type -> Constraint
58class
59 ( Context a ~ Reify Aggregate => Unreifier Aggregate a
60 , Context a ~ Reify Expr => Unreifier Expr a
61 , Context a ~ Reify Name => Unreifier Name a
62 , (forall ctx. (Context a ~ Reify (Reify ctx), Reifiable ctx) => Unreifier (Reify ctx) a)
63 )
64 => Unreifiable a
65instance
66 ( Context a ~ Reify Aggregate => Unreifier Aggregate a
67 , Context a ~ Reify Expr => Unreifier Expr a
68 , Context a ~ Reify Name => Unreifier Name a
69 , (forall ctx. (Context a ~ Reify (Reify ctx), Reifiable ctx) => Unreifier (Reify ctx) a)
70 )
71 => Unreifiable a
74type Unreifier :: K.Context -> Type -> Constraint
75class
76 ( Table context (Unreify a)
77 , Congruent a (Unreify a)
78 )
79 => Unreifier context a
80instance
81 ( Table context (Unreify a)
82 , Congruent a (Unreify a)
83 )
84 => Unreifier context a
87type Unreifiability :: K.Context -> Type -> Type
88data Unreifiability context a where
89 UResult :: Unreifiability Result a
90 Unreifiability :: Unreifier context a
91 => SContext context -> Unreifiability context a
94unreifiability :: (Context a ~ Reify context, Unreifiable a)
95 => SContext context -> Unreifiability context a
96unreifiability = \case
97 SAggregate -> Unreifiability SAggregate
98 SExpr -> Unreifiability SExpr
99 SName -> Unreifiability SName
100 SResult -> UResult
101 SReify context -> case sReifiable context of
102 Dict -> Unreifiability (SReify context)