git.iko.soy/rel8
on b2e2fc9 help sign in
rel8/src/Rel8/Schema/Reify.hs
75 lines 2.0 kB history raw
1{-# language AllowAmbiguousTypes #-}
2{-# language EmptyCase #-}
3{-# language DataKinds #-}
4{-# language FlexibleInstances #-}
5{-# language ScopedTypeVariables #-}
6{-# language StandaloneKindSignatures #-}
7{-# language TypeApplications #-}
8{-# language TypeFamilies #-}
9{-# language TypeOperators #-}
10{-# language UndecidableInstances #-}
12module Rel8.Schema.Reify
13 ( Reify, Col( Reify ), hreify, hunreify
14 , UnwrapReify
15 , NotReify, notReify
16 )
17where
19-- base
20import Data.Kind ( Constraint )
21import Data.Type.Equality ( (:~:)( Refl ) )
22import Prelude
24-- rel8
25import Rel8.Schema.Context ( Interpretation, Col )
26import Rel8.Schema.Context.Label ( Labelable, labeler, unlabeler )
27import Rel8.Schema.HTable ( HTable, hfield, htabulate )
28import Rel8.Schema.Kind ( Context )
31type Reify :: Context -> Context
32data Reify context a
35instance Interpretation (Reify context) where
36 newtype Col (Reify context) spec = Reify (Col context spec)
39instance Labelable context => Labelable (Reify context) where
40 labeler (Reify a) = Reify (labeler a)
41 unlabeler (Reify a) = Reify (unlabeler a)
44hreify :: HTable t => t (Col context) -> t (Col (Reify context))
45hreify a = htabulate $ \field -> Reify (hfield a field)
48hunreify :: HTable t => t (Col (Reify context)) -> t (Col context)
49hunreify a = htabulate $ \field -> case hfield a field of
50 Reify x -> x
53type UnwrapReify :: Context -> Context
54type family UnwrapReify context where
55 UnwrapReify (Reify context) = context
58type IsReify :: Context -> Bool
59type family IsReify context where
60 IsReify (Reify _) = 'True
61 IsReify _ = 'False
64type NotReify :: Context -> Constraint
65class IsReify context ~ 'False => NotReify context
66instance IsReify context ~ 'False => NotReify context
69notReify :: forall context ctx a. NotReify context => context :~: Reify ctx -> a
70notReify refl = case lemma @context of
71 Refl -> case refl of
74lemma :: NotReify context => IsReify context :~: 'False
75lemma = Refl