git.iko.soy/rel8
on fadfc3e help sign in
rel8/src/Rel8/Schema/Nullability.hs
86 lines 2.1 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 #-}
13module Rel8.Schema.Nullability
14 ( IsMaybe, Nullify, Unnullify
15 , Nullability( Nullable, NonNullable )
16 , Nullabilizes, nullabilization
17 )
18where
20-- base
21import Data.Kind ( Constraint, Type )
22import Prelude
24-- rel8
25import Rel8.Opaque ( Opaque )
28type IsMaybe :: Type -> Bool
29type family IsMaybe a where
30 IsMaybe (Maybe _) = 'True
31 IsMaybe _ = 'False
34type Unnullify' :: Bool -> Type -> Type
35type family Unnullify' isMaybe ma where
36 Unnullify' 'False a = a
37 Unnullify' 'True (Maybe a) = a
40type Unnullify :: Type -> Type
41type Unnullify a = Unnullify' (IsMaybe a) a
44type Nullify' :: Bool -> Type -> Type
45type family Nullify' isMaybe a where
46 Nullify' 'False a = a
47 Nullify' 'True a = Maybe a
50type Nullify :: Type -> Type
51type Nullify a = Maybe (Unnullify a)
54type Nullability :: Type -> Type -> Type
55data Nullability a ma where
56 NonNullable :: IsMaybe a ~ 'False => Nullability a a
57 Nullable :: IsMaybe a ~ 'False => Nullability a (Maybe a)
60type Nullabilizes' :: Bool -> Type -> Type -> Constraint
61class
62 ( IsMaybe ma ~ isMaybe
63 , IsMaybe a ~ 'False
64 , Unnullify ma ~ a
65 , Nullify' isMaybe a ~ ma
66 ) => Nullabilizes' isMaybe a ma | isMaybe ma -> a, isMaybe a -> ma
67 where
68 nullabilization' :: Nullability a ma
71instance IsMaybe a ~ 'False => Nullabilizes' 'False a a where
72 nullabilization' = NonNullable
75instance IsMaybe a ~ 'False => Nullabilizes' 'True a (Maybe a) where
76 nullabilization' = Nullable
79type Nullabilizes :: Type -> Type -> Constraint
80class Nullabilizes' (IsMaybe ma) a ma => Nullabilizes a ma
81instance Nullabilizes' (IsMaybe ma) a ma => Nullabilizes a ma
82instance {-# OVERLAPPING #-} Nullabilizes Opaque Opaque
85nullabilization :: forall a db. Nullabilizes db a => Nullability db a
86nullabilization = nullabilization'