@@ -1,22 +1,131 @@
11{-# language ConstraintKinds #-}
2+{-# language DataKinds #-}
3+{-# language FlexibleContexts #-}
24{-# language FlexibleInstances #-}
3−{-# language MonoLocalBinds #-}
5+{-# language GADTs #-}
46{-# language MultiParamTypeClasses #-}
7+{-# language RankNTypes #-}
8+{-# language StandaloneKindSignatures #-}
9+{-# language TypeFamilies #-}
510{-# language UndecidableInstances #-}
6−
7−{-# options_ghc -fno-warn-orphans #-}
11+{-# language UndecidableSuperClasses #-}
812
913module Rel8.Schema.Nullability
10− ( module Rel8.Schema.Nullability.Internal
14+ ( Nullify, Unnullify
15+ , NotNull
16+ , Homonullable
17+ , Nullability( Nullable, NonNullable )
18+ , HasNullability, nullabilization
19+ , Sql, fromSql, mapSql, toSql
1120 )
1221where
1322
1423-- base
15−import Prelude ()
24+import Data.Kind ( Constraint, Type )
25+import Prelude
1626
1727-- rel8
18−import Rel8.Opaque ( Opaque )
19−import Rel8.Schema.Nullability.Internal
28+import Rel8.Schema.Dict ( Dict( Dict ) )
29+
30+
31+type IsMaybe :: Type -> Bool
32+type family IsMaybe a where
33+ IsMaybe (Maybe _) = 'True
34+ IsMaybe _ = 'False
35+
36+
37+type Unnullify' :: Bool -> Type -> Type
38+type family Unnullify' isMaybe ma where
39+ Unnullify' 'False a = a
40+ Unnullify' 'True (Maybe a) = a
41+
42+
43+type Unnullify :: Type -> Type
44+type Unnullify a = Unnullify' (IsMaybe a) a
45+
46+
47+type Nullify' :: Bool -> Type -> Type
48+type family Nullify' isMaybe a where
49+ Nullify' 'False a = a
50+ Nullify' 'True a = Maybe a
51+
52+
53+type Nullify :: Type -> Type
54+type Nullify a = Maybe (Unnullify a)
55+
56+
57+-- | @nullify a@ means @a@ cannot take @null@ as a value.
58+type NotNull :: Type -> Constraint
59+class (HasNullability a, IsMaybe a ~ 'False) => NotNull a
60+instance (HasNullability a, IsMaybe a ~ 'False) => NotNull a
61+
62+
63+-- | @Homonullable a b@ means that both @a@ and @b@ can be @null@, or neither
64+-- @a@ or @b@ can be @null@.
65+type Homonullable :: Type -> Type -> Constraint
66+class IsMaybe a ~ IsMaybe b => Homonullable a b
67+instance IsMaybe a ~ IsMaybe b => Homonullable a b
68+
69+
70+type Nullability :: Type -> Type
71+data Nullability a where
72+ NonNullable :: NotNull a => Nullability a
73+ Nullable :: NotNull a => Nullability (Maybe a)
74+
75+
76+type HasNullability' :: Bool -> Type -> Constraint
77+class
78+ ( IsMaybe a ~ isMaybe
79+ , IsMaybe (Unnullify a) ~ 'False
80+ , Nullify' isMaybe (Unnullify a) ~ a
81+ ) => HasNullability' isMaybe a
82+ where
83+ nullabilization' :: Nullability a
84+
85+
86+instance IsMaybe a ~ 'False => HasNullability' 'False a where
87+ nullabilization' = NonNullable
88+
89+
90+instance IsMaybe a ~ 'False => HasNullability' 'True (Maybe a) where
91+ nullabilization' = Nullable
92+
93+
94+-- | @HasNullability a@ means that @rel8@ is able to check if the type @a@ is a
95+-- type that can take @null@ values or not.
96+type HasNullability :: Type -> Constraint
97+class HasNullability' (IsMaybe a) a => HasNullability a
98+instance HasNullability' (IsMaybe a) a => HasNullability a
99+
100+
101+nullabilization :: HasNullability a => Nullability a
102+nullabilization = nullabilization'
103+
104+
105+-- | The @Sql@ type class describes both null and not null database values,
106+-- constrained by a specific class.
107+--
108+-- For example, if you see @Sql DBEq a@, this means any database type that
109+-- supports equality, and @a@ can either be exactly an @a@, or it could also be
110+-- @Maybe a@.
111+type Sql :: (Type -> Constraint) -> Type -> Constraint
112+class (constraint (Unnullify a), HasNullability a) => Sql constraint a
113+instance (constraint (Unnullify a), HasNullability a) => Sql constraint a
114+
115+
116+fromSql :: Dict (Sql constraint) a -> (Nullability a, Dict constraint (Unnullify a))
117+fromSql Dict = (nullabilization, Dict)
118+{-# INLINABLE fromSql #-}
119+
120+
121+mapSql :: ()
122+ => (forall x. Dict constraint x -> Dict constraint' x)
123+ -> Dict (Sql constraint) a -> Dict (Sql constraint') a
124+mapSql f dict = case fromSql dict of
125+ (nullability, dict') -> toSql nullability (f dict')
20126
21127
22−instance {-# OVERLAPPING #-} (c Opaque, Sql c Opaque) => Sql c Opaque
128+toSql :: Nullability a -> Dict constraint (Unnullify a) -> Dict (Sql constraint) a
129+toSql NonNullable Dict = Dict
130+toSql Nullable Dict = Dict
131+{-# INLINABLE toSql #-}