git.iko.soy/schematic
on union help sign in
schematic/src/Data/Schematic/Schema.hs
503 lines 18 kB history raw
1{-# LANGUAGE AllowAmbiguousTypes #-}
2{-# LANGUAGE OverloadedLists #-}
3{-# LANGUAGE OverloadedStrings #-}
4{-# OPTIONS_GHC -fprint-explicit-kinds #-}
6module Data.Schematic.Schema where
8import Control.Applicative ((<|>))
9import Control.Monad
10import Data.Aeson as J
11import Data.Aeson.Types as J
12import Data.HashMap.Strict as H
13import Data.Kind
14import Data.Maybe
15import Data.Schematic.Instances ()
16import Data.Scientific
17import Data.Singletons.Prelude.List hiding (All, Union)
18import Data.Singletons.TH
19import Data.Singletons.TypeLits
20import Data.Text as T
21import Data.Union
22import Data.Vector as V
23import Data.Vinyl hiding (Dict)
24import qualified Data.Vinyl.TypeLevel as V
25import GHC.Generics (Generic)
26import GHC.TypeLits (SomeNat(..), SomeSymbol(..), someSymbolVal, someNatVal)
27import Prelude as P
28import Test.SmallCheck.Series
31type family CRepr (s :: Schema) :: Type where
32 CRepr ('SchemaText cs) = TextConstraint
33 CRepr ('SchemaNumber cs) = NumberConstraint
34 CRepr ('SchemaObject fs) = (String, Schema)
35 CRepr ('SchemaArray ar s) = ArrayConstraint
37data TextConstraint
38 = TEq Nat
39 | TLt Nat
40 | TLe Nat
41 | TGt Nat
42 | TGe Nat
43 | TRegex Symbol
44 | TEnum [Symbol]
45 deriving (Generic)
47instance SingKind TextConstraint where
48 type Demote TextConstraint = DemotedTextConstraint
49 fromSing = \case
50 STEq n -> withKnownNat n (DTEq $ natVal n)
51 STLt n -> withKnownNat n (DTLt $ natVal n)
52 STLe n -> withKnownNat n (DTLe $ natVal n)
53 STGt n -> withKnownNat n (DTGt $ natVal n)
54 STGe n -> withKnownNat n (DTGe $ natVal n)
55 STRegex s -> withKnownSymbol s (DTRegex $ T.pack $ symbolVal s)
56 STEnum s -> let
57 d :: Sing (s :: [Symbol]) -> [Text]
58 d SNil = []
59 d (SCons ss@SSym fs) = T.pack (symbolVal ss) : d fs
60 in DTEnum $ d s
61 toSing = \case
62 DTEq n -> case someNatVal n of
63 Just (SomeNat (_ :: Proxy n)) -> SomeSing (STEq (SNat :: Sing n))
64 Nothing -> error "Negative singleton nat"
65 DTLt n -> case someNatVal n of
66 Just (SomeNat (_ :: Proxy n)) -> SomeSing (STLt (SNat :: Sing n))
67 Nothing -> error "Negative singleton nat"
68 DTLe n -> case someNatVal n of
69 Just (SomeNat (_ :: Proxy n)) -> SomeSing (STLe (SNat :: Sing n))
70 Nothing -> error "Negative singleton nat"
71 DTGt n -> case someNatVal n of
72 Just (SomeNat (_ :: Proxy n)) -> SomeSing (STGt (SNat :: Sing n))
73 Nothing -> error "Negative singleton nat"
74 DTGe n -> case someNatVal n of
75 Just (SomeNat (_ :: Proxy n)) -> SomeSing (STGe (SNat :: Sing n))
76 Nothing -> error "Negative singleton nat"
77 DTRegex s -> case someSymbolVal (T.unpack s) of
78 SomeSymbol (_ :: Proxy n) -> SomeSing (STRegex (SSym :: Sing n))
79 DTEnum ss -> case toSing ss of
80 SomeSing l -> SomeSing (STEnum l)
82data DemotedTextConstraint
83 = DTEq Integer
84 | DTLt Integer
85 | DTLe Integer
86 | DTGt Integer
87 | DTGe Integer
88 | DTRegex Text
89 | DTEnum [Text]
90 deriving (Generic)
92data instance Sing (tc :: TextConstraint) where
93 STEq :: Sing n -> Sing ('TEq n)
94 STLt :: Sing n -> Sing ('TLt n)
95 STLe :: Sing n -> Sing ('TLe n)
96 STGt :: Sing n -> Sing ('TGt n)
97 STGe :: Sing n -> Sing ('TGe n)
98 STRegex :: Sing s -> Sing ('TRegex s)
99 STEnum :: Sing ss -> Sing ('TEnum ss)
101instance (KnownNat n) => SingI ('TEq n) where sing = STEq sing
102instance (KnownNat n) => SingI ('TGt n) where sing = STGt sing
103instance (KnownNat n) => SingI ('TGe n) where sing = STGe sing
104instance (KnownNat n) => SingI ('TLt n) where sing = STLt sing
105instance (KnownNat n) => SingI ('TLe n) where sing = STLe sing
106instance (KnownSymbol s, SingI s) => SingI ('TRegex s) where sing = STRegex sing
107instance (SingI ss) => SingI ('TEnum ss) where sing = STEnum sing
109instance Eq (Sing ('TEq n)) where _ == _ = True
110instance Eq (Sing ('TLt n)) where _ == _ = True
111instance Eq (Sing ('TLe n)) where _ == _ = True
112instance Eq (Sing ('TGt n)) where _ == _ = True
113instance Eq (Sing ('TGe n)) where _ == _ = True
114instance Eq (Sing ('TRegex t)) where _ == _ = True
115instance Eq (Sing ('TEnum ss)) where _ == _ = True
117data NumberConstraint
118 = NLe Nat
119 | NLt Nat
120 | NGt Nat
121 | NGe Nat
122 | NEq Nat
123 deriving (Generic)
125data DemotedNumberConstraint
126 = DNLe Integer
127 | DNLt Integer
128 | DNGt Integer
129 | DNGe Integer
130 | DNEq Integer
131 deriving (Generic)
133data instance Sing (nc :: NumberConstraint) where
134 SNEq :: Sing n -> Sing ('NEq n)
135 SNGt :: Sing n -> Sing ('NGt n)
136 SNGe :: Sing n -> Sing ('NGe n)
137 SNLt :: Sing n -> Sing ('NLt n)
138 SNLe :: Sing n -> Sing ('NLe n)
140instance KnownNat n => SingI ('NEq n) where sing = SNEq sing
141instance KnownNat n => SingI ('NGt n) where sing = SNGt sing
142instance KnownNat n => SingI ('NGe n) where sing = SNGe sing
143instance KnownNat n => SingI ('NLt n) where sing = SNLt sing
144instance KnownNat n => SingI ('NLe n) where sing = SNLe sing
146instance Eq (Sing ('NEq n)) where _ == _ = True
147instance Eq (Sing ('NLt n)) where _ == _ = True
148instance Eq (Sing ('NLe n)) where _ == _ = True
149instance Eq (Sing ('NGt n)) where _ == _ = True
150instance Eq (Sing ('NGe n)) where _ == _ = True
152instance SingKind NumberConstraint where
153 type Demote NumberConstraint = DemotedNumberConstraint
154 fromSing = \case
155 SNEq n -> withKnownNat n (DNEq $ natVal n)
156 SNGt n -> withKnownNat n (DNGt $ natVal n)
157 SNGe n -> withKnownNat n (DNGe $ natVal n)
158 SNLt n -> withKnownNat n (DNLt $ natVal n)
159 SNLe n -> withKnownNat n (DNLe $ natVal n)
160 toSing = \case
161 DNEq n -> case someNatVal n of
162 Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNEq (SNat :: Sing n))
163 Nothing -> error "Negative singleton nat"
164 DNGt n -> case someNatVal n of
165 Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNGt (SNat :: Sing n))
166 Nothing -> error "Negative singleton nat"
167 DNGe n -> case someNatVal n of
168 Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNGe (SNat :: Sing n))
169 Nothing -> error "Negative singleton nat"
170 DNLt n -> case someNatVal n of
171 Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNLt (SNat :: Sing n))
172 Nothing -> error "Negative singleton nat"
173 DNLe n -> case someNatVal n of
174 Just (SomeNat (_ :: Proxy n)) -> SomeSing (SNLe (SNat :: Sing n))
175 Nothing -> error "Negative singleton nat"
177data ArrayConstraint
178 = AEq Nat
179 deriving (Generic)
181data DemotedArrayConstraint
182 = DAEq Integer
183 deriving (Generic)
185data instance Sing (ac :: ArrayConstraint) where
186 SAEq :: Sing n -> Sing ('AEq n)
188instance KnownNat n => SingI ('AEq n) where sing = SAEq sing
190instance Eq (Sing ('AEq n)) where _ == _ = True
192instance SingKind ArrayConstraint where
193 type Demote ArrayConstraint = DemotedArrayConstraint
194 fromSing = \case
195 SAEq n -> withKnownNat n (DAEq $ natVal n)
196 toSing = \case
197 DAEq n -> case someNatVal n of
198 Just (SomeNat (_ :: Proxy n)) -> SomeSing (SAEq (SNat :: Sing n))
199 Nothing -> error "Negative singleton nat"
201data Schema
202 = SchemaText [TextConstraint]
203 | SchemaBoolean
204 | SchemaNumber [NumberConstraint]
205 | SchemaObject [(Symbol, Schema)]
206 | SchemaArray [ArrayConstraint] Schema
207 | SchemaNull
208 | SchemaOptional Schema
209 | SchemaUnion [Schema]
210 deriving (Generic)
212data DemotedSchema
213 = DSchemaText [DemotedTextConstraint]
214 | DSchemaNumber [DemotedNumberConstraint]
215 | DSchemaBoolean
216 | DSchemaObject [(Text, DemotedSchema)]
217 | DSchemaArray [DemotedArrayConstraint] DemotedSchema
218 | DSchemaNull
219 | DSchemaOptional DemotedSchema
220 | DSchemaUnion [DemotedSchema]
221 deriving (Generic)
223data instance Sing (schema :: Schema) where
224 SSchemaText :: Sing tcs -> Sing ('SchemaText tcs)
225 SSchemaNumber :: Sing ncs -> Sing ('SchemaNumber ncs)
226 SSchemaBoolean :: Sing 'SchemaBoolean
227 SSchemaArray :: Sing acs -> Sing schema -> Sing ('SchemaArray acs schema)
228 SSchemaObject :: Sing fields -> Sing ('SchemaObject fields)
229 SSchemaOptional :: Sing s -> Sing ('SchemaOptional s)
230 SSchemaNull :: Sing 'SchemaNull
231 SSchemaUnion :: Sing ss -> Sing ('SchemaUnion ss)
233instance SingI sl => SingI ('SchemaText sl) where
234 sing = SSchemaText sing
235instance SingI sl => SingI ('SchemaNumber sl) where
236 sing = SSchemaNumber sing
237instance SingI 'SchemaNull where
238 sing = SSchemaNull
239instance SingI 'SchemaBoolean where
240 sing = SSchemaBoolean
241instance (SingI ac, SingI s) => SingI ('SchemaArray ac s) where
242 sing = SSchemaArray sing sing
243instance SingI stl => SingI ('SchemaObject stl) where
244 sing = SSchemaObject sing
245instance SingI s => SingI ('SchemaOptional s) where
246 sing = SSchemaOptional sing
247instance SingI s => SingI ('SchemaUnion s) where
248 sing = SSchemaUnion sing
250instance Eq (Sing ('SchemaText cs)) where _ == _ = True
251instance Eq (Sing ('SchemaNumber cs)) where _ == _ = True
252instance Eq (Sing 'SchemaNull) where _ == _ = True
253instance Eq (Sing 'SchemaBoolean) where _ == _ = True
254instance Eq (Sing ('SchemaArray as s)) where _ == _ = True
255instance Eq (Sing ('SchemaObject cs)) where _ == _ = True
256instance Eq (Sing ('SchemaOptional s)) where _ == _ = True
257instance Eq (Sing ('SchemaUnion s)) where _ == _ = True
259instance SingKind Schema where
260 type Demote Schema = DemotedSchema
261 fromSing = \case
262 SSchemaText cs -> DSchemaText $ fromSing cs
263 SSchemaNumber cs -> DSchemaNumber $ fromSing cs
264 SSchemaBoolean -> DSchemaBoolean
265 SSchemaArray cs s -> DSchemaArray (fromSing cs) (fromSing s)
266 SSchemaOptional s -> DSchemaOptional $ fromSing s
267 SSchemaNull -> DSchemaNull
268 SSchemaObject cs -> DSchemaObject $ fromSing cs
269 SSchemaUnion ss -> DSchemaUnion $ fromSing ss
270 toSing = \case
271 DSchemaText cs -> case toSing cs of
272 SomeSing scs -> SomeSing $ SSchemaText scs
273 DSchemaNumber cs -> case toSing cs of
274 SomeSing scs -> SomeSing $ SSchemaNumber scs
275 DSchemaBoolean -> SomeSing $ SSchemaBoolean
276 DSchemaArray cs sch -> case (toSing cs, toSing sch) of
277 (SomeSing scs, SomeSing ssch) -> SomeSing $ SSchemaArray scs ssch
278 DSchemaOptional sch -> case toSing sch of
279 SomeSing ssch -> SomeSing $ SSchemaOptional ssch
280 DSchemaNull -> SomeSing SSchemaNull
281 DSchemaObject cs -> case toSing cs of
282 SomeSing scs -> SomeSing $ SSchemaObject scs
283 DSchemaUnion ss -> case toSing ss of
284 SomeSing sss -> SomeSing $ SSchemaUnion sss
286data FieldRepr :: (Symbol, Schema) -> Type where
287 FieldRepr
288 :: (SingI schema, KnownSymbol name)
289 => JsonRepr schema
290 -> FieldRepr '(name, schema)
292-- | Forgetful Functor Ufr
293toJsonRepr :: FieldRepr '(fn, sch) -> JsonRepr sch
294toJsonRepr (FieldRepr x) = x
296knownFieldName
297 :: forall proxy (fieldName :: Symbol) schema
298 . KnownSymbol fieldName
299 => proxy '(fieldName, schema)
300 -> Text
301knownFieldName _ = T.pack $ symbolVal (Proxy @fieldName)
303knownFieldSchema
304 :: forall proxy fieldName schema
305 . SingI schema
306 => proxy '(fieldName, schema)
307 -> Sing schema
308knownFieldSchema _ = sing
310deriving instance Show (JsonRepr schema) => Show (FieldRepr '(name, schema))
312instance Eq (JsonRepr schema) => Eq (FieldRepr '(name, schema)) where
313 FieldRepr a == FieldRepr b = a == b
315instance
316 ( KnownSymbol name
317 , SingI schema
318 , Serial m (JsonRepr schema) )
319 => Serial m (FieldRepr '(name, schema)) where
320 series = FieldRepr <$> series
322type family USubsets (u :: [k]) :: Constraint where
323 USubsets '[] = ()
324 USubsets (h ': tl) = (USubset tl (h ': tl) (V.RImage tl (h ': tl)), USubsets tl)
326data JsonRepr :: Schema -> Type where
327 ReprText :: Text -> JsonRepr ('SchemaText cs)
328 ReprNumber :: Scientific -> JsonRepr ('SchemaNumber cs)
329 ReprBoolean :: Bool -> JsonRepr 'SchemaBoolean
330 ReprNull :: JsonRepr 'SchemaNull
331 ReprArray :: V.Vector (JsonRepr s) -> JsonRepr ('SchemaArray cs s)
332 ReprObject :: Rec FieldRepr fs -> JsonRepr ('SchemaObject fs)
333 ReprOptional :: Maybe (JsonRepr s) -> JsonRepr ('SchemaOptional s)
334 ReprUnion
335 -- :: USubsets (h ': tl)
336 :: Union JsonRepr (h ': tl)
337 -> JsonRepr ('SchemaUnion (h ': tl))
339-- | Move to the union package
340type family UnionAll (f :: u -> *) (rs :: [u]) (c :: * -> Constraint) :: Constraint where
341 UnionAll f '[] c = ()
342 UnionAll f (r ': rs) c = (c (f r), UnionAll f rs c)
344-- instance (UnionAll f as Show) => Show (Union f as) where
345-- show (This fa) = "This " P.++ show fa
346-- show (That u) = "That " P.++ show u
348instance Show (JsonRepr ('SchemaText cs)) where
349 show (ReprText t) = "ReprText " P.++ show t
351instance Show (JsonRepr ('SchemaNumber cs)) where
352 show (ReprNumber n) = "ReprNumber " P.++ show n
354instance Show (JsonRepr 'SchemaNull) where show _ = "ReprNull"
356instance Show (JsonRepr s) => Show (JsonRepr ('SchemaArray acs s)) where
357 show (ReprArray v) = "ReprArray " P.++ show v
359instance V.RecAll FieldRepr fs Show => Show (JsonRepr ('SchemaObject fs)) where
360 show (ReprObject fs) = "ReprObject " P.++ show fs
362instance Show (JsonRepr s) => Show (JsonRepr ('SchemaOptional s)) where
363 show (ReprOptional s) = "ReprOptional " P.++ show s
365deriving instance UnionAll f as Show => Show (Union f as)
367instance (Monad m, Serial m Text)
368 => Serial m (JsonRepr ('SchemaText cs)) where
369 series = cons1 ReprText
371instance (Monad m, Serial m Scientific)
372 => Serial m (JsonRepr ('SchemaNumber cs)) where
373 series = cons1 ReprNumber
375instance Monad m => Serial m (JsonRepr 'SchemaNull) where
376 series = cons0 ReprNull
378instance (Serial m (V.Vector (JsonRepr s)))
379 => Serial m (JsonRepr ('SchemaArray cs s)) where
380 series = cons1 ReprArray
382instance (Serial m (JsonRepr s))
383 => Serial m (JsonRepr ('SchemaOptional s)) where
384 series = cons1 ReprOptional
386instance (Monad m, Serial m (Rec FieldRepr fs))
387 => Serial m (JsonRepr ('SchemaObject fs)) where
388 series = cons1 ReprObject
390instance Eq (Rec FieldRepr fs) => Eq (JsonRepr ('SchemaObject fs)) where
391 ReprObject a == ReprObject b = a == b
393instance Eq (JsonRepr ('SchemaText cs)) where
394 ReprText a == ReprText b = a == b
396instance Eq (JsonRepr ('SchemaNumber cs)) where
397 ReprNumber a == ReprNumber b = a == b
399instance Eq (JsonRepr 'SchemaNull) where
400 ReprNull == ReprNull = True
402instance Eq (JsonRepr s) => Eq (JsonRepr ('SchemaArray as s)) where
403 ReprArray a == ReprArray b = a == b
405instance Eq (JsonRepr s) => Eq (JsonRepr ('SchemaOptional s)) where
406 ReprOptional a == ReprOptional b = a == b
408fromOptional
409 :: SingI s
410 => Sing ('SchemaOptional s)
411 -> J.Value
412 -> Parser (Maybe (JsonRepr s))
413fromOptional _ = parseJSON
415parseUnion
416 :: FromJSON (JsonRepr ('SchemaUnion ss))
417 => sing (ss :: [Schema])
418 -> Value
419 -> Parser (JsonRepr ('SchemaUnion ss))
420parseUnion _ val = parseJSON val
422instance FromJSON (Union JsonRepr '[]) where
423 parseJSON = fail "empty union"
425instance (SingI a, FromJSON (Union JsonRepr as)) => FromJSON (Union JsonRepr (a ': as)) where
426 parseJSON val = (This <$> parseJSON val)
427 <|> (That <$> (parseJSON val :: Parser (Union JsonRepr as)))
429instance ToJSON (Union JsonRepr as) where
430 toJSON (This fa) = toJSON fa
431 toJSON (That u) = toJSON u
433instance SingI schema => J.FromJSON (JsonRepr schema) where
434 parseJSON value = case sing :: Sing schema of
435 SSchemaText _ -> withText "String" (pure . ReprText) value
436 SSchemaNumber _ -> withScientific "Number" (pure . ReprNumber) value
437 SSchemaBoolean -> ReprBoolean <$> parseJSON value
438 SSchemaNull -> case value of
439 J.Null -> pure ReprNull
440 _ -> typeMismatch "Null" value
441 so@(SSchemaOptional s) -> withSingI s $ ReprOptional <$> fromOptional so value
442 SSchemaArray sa sb -> withSingI sa $ withSingI sb
443 $ withArray "Array" (fmap ReprArray . traverse parseJSON) value
444 SSchemaObject fs -> do
445 let
446 demoteFields :: SList s -> H.HashMap Text J.Value -> Parser (Rec FieldRepr s)
447 demoteFields SNil _ = pure RNil
448 demoteFields (SCons (STuple2 (n :: Sing fn) s) tl) h = withKnownSymbol n $ do
449 let fieldName = T.pack $ symbolVal (Proxy @fn)
450 fieldRepr <- case s of
451 SSchemaText so -> case H.lookup fieldName h of
452 Just v -> withSingI so $ FieldRepr <$> parseJSON v
453 Nothing -> fail "schematext"
454 SSchemaNumber so -> case H.lookup fieldName h of
455 Just v -> withSingI so $ FieldRepr <$> parseJSON v
456 Nothing -> fail "schemanumber"
457 SSchemaBoolean -> case H.lookup fieldName h of
458 Just v -> FieldRepr <$> parseJSON v
459 Nothing -> fail "schemaboolean"
460 SSchemaNull -> case H.lookup fieldName h of
461 Just v -> FieldRepr <$> parseJSON v
462 Nothing -> fail "schemanull"
463 SSchemaArray sa sb -> case H.lookup fieldName h of
464 Just v -> withSingI sa $ withSingI sb $ FieldRepr <$> parseJSON v
465 Nothing -> fail "schemaarray"
466 SSchemaObject so -> case H.lookup fieldName h of
467 Just v -> withSingI so $ FieldRepr <$> parseJSON v
468 Nothing -> fail "schemaobject"
469 SSchemaOptional so -> case H.lookup fieldName h of
470 Just v -> withSingI so $ FieldRepr <$> parseJSON v
471 Nothing -> fail "schemaoptional"
472 SSchemaUnion ss -> withSingI ss $ FieldRepr <$> parseUnion ss value
473 (fieldRepr :&) <$> demoteFields tl h
474 ReprObject <$> withObject "Object" (demoteFields fs) value
475 SSchemaUnion ss -> parseUnion ss value
477instance J.ToJSON (JsonRepr a) where
478 toJSON ReprNull = J.Null
479 toJSON (ReprBoolean b) = J.Bool b
480 toJSON (ReprText t) = J.String t
481 toJSON (ReprNumber n) = J.Number n
482 toJSON (ReprOptional s) = case s of
483 Just v -> toJSON v
484 Nothing -> J.Null
485 toJSON (ReprArray v) = J.Array $ toJSON <$> v
486 toJSON (ReprObject r) = J.Object . H.fromList . fold $ r
487 where
488 extract :: forall name s . (KnownSymbol name)
489 => FieldRepr '(name, s)
490 -> (Text, Value)
491 extract (FieldRepr s) = (T.pack $ symbolVal $ Proxy @name, toJSON s)
492 fold :: Rec FieldRepr fs -> [(Text, J.Value)]
493 fold = \case
494 RNil -> []
495 fr@(FieldRepr _) :& tl -> (extract fr) : fold tl
496 toJSON (ReprUnion u) = toJSON u
498class FalseConstraint a
500type family TopLevel (schema :: Schema) :: Constraint where
501 TopLevel ('SchemaArray acs s) = ()
502 TopLevel ('SchemaObject o) = ()
503 TopLevel spec = 'True ~ 'False