on eb180fa help sign in
rel8/src/Rel8/Schema/Nullability.hs
100 lines 2.6 kB history raw
1{-# language ConstraintKinds #-}
2{-# language DataKinds #-}
3{-# language FlexibleContexts #-}
4{-# language FlexibleInstances #-}
5{-# language FunctionalDependencies #-}
6{-# language GADTs #-}
7{-# language MultiParamTypeClasses #-}
8{-# language QuantifiedConstraints #-}
9{-# language StandaloneKindSignatures #-}
10{-# language TypeFamilies #-}
11{-# language UndecidableInstances #-}
12{-# language UndecidableSuperClasses #-}
14module Rel8.Schema.Nullability
15 ( IsMaybe, Nullify, Unnullify
16 , Nullability( Nullable, NonNullable )
17 , Sql
18 , Nullabilizes, nullabilization
19 )
20where
22-- base
23import Data.Kind ( Constraint, Type )
24import Prelude
26-- rel8
27import Rel8.Opaque ( Opaque )
30type IsMaybe :: Type -> Bool
31type family IsMaybe a where
32 IsMaybe (Maybe _) = 'True
33 IsMaybe _ = 'False
36type Unnullify' :: Bool -> Type -> Type
37type family Unnullify' isMaybe ma where
38 Unnullify' 'False a = a
39 Unnullify' 'True (Maybe a) = a
42type Unnullify :: Type -> Type
43type Unnullify a = Unnullify' (IsMaybe a) a
46type Nullify' :: Bool -> Type -> Type
47type family Nullify' isMaybe a where
48 Nullify' 'False a = a
49 Nullify' 'True a = Maybe a
52type Nullify :: Type -> Type
53type Nullify a = Maybe (Unnullify a)
56type Nullability :: Type -> Type -> Type
57data Nullability a ma where
58 NonNullable :: IsMaybe a ~ 'False => Nullability a a
59 Nullable :: IsMaybe a ~ 'False => Nullability a (Maybe a)
62type Nullabilizes' :: Bool -> Type -> Type -> Constraint
63class
64 ( IsMaybe ma ~ isMaybe
65 , IsMaybe a ~ 'False
66 , Unnullify ma ~ a
67 , Nullify' isMaybe a ~ ma
68 ) => Nullabilizes' isMaybe a ma | isMaybe ma -> a, isMaybe a -> ma
69 where
70 nullabilization' :: Nullability a ma
73instance IsMaybe a ~ 'False => Nullabilizes' 'False a a where
74 nullabilization' = NonNullable
77instance IsMaybe a ~ 'False => Nullabilizes' 'True a (Maybe a) where
78 nullabilization' = Nullable
81type Nullabilizes :: Type -> Type -> Constraint
82class Nullabilizes' (IsMaybe ma) a ma => Nullabilizes a ma
83instance Nullabilizes' (IsMaybe ma) a ma => Nullabilizes a ma
84instance {-# OVERLAPPING #-} Nullabilizes Opaque Opaque
87type Sql :: (Type -> Constraint) -> Type -> Constraint
88class
89 ( (forall c. (forall x. (constraint x => c x)) => Sql c a)
90 , Nullabilizes (Unnullify a) a
91 , constraint (Unnullify a)
92 )
93 => Sql constraint a
94instance (constraint db, Nullabilizes db a) => Sql constraint a
95instance {-# OVERLAPPING #-} (constraint Opaque, Sql constraint Opaque) => Sql constraint Opaque
96-- instance {-# OVERLAPPING #-} Sql OpaqueC Opaque => Sql OpaqueC Opaque
99nullabilization :: forall a db. Nullabilizes db a => Nullability db a
100nullabilization = nullabilization'