1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
|
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
import Data.Aeson (Value, object, (.=))
import Data.Constraint (Dict (Dict))
import Data.Kind (Type)
import Data.Maybe (mapMaybe)
import Data.Singletons (Sing, SingI, sing)
import Data.Singletons.Base.TH (genSingletons, singDecideInstance)
import Data.Singletons.Decide qualified as D
data Sigma (f :: k -> Type) where
Sigma :: Sing a -> f a -> Sigma f
withSigma :: (forall (a :: k). Sing a -> f a -> r) -> Sigma f -> r
withSigma c (Sigma s f) = c s f
toSigma :: SingI a => f a -> Sigma f
toSigma = Sigma sing
fromSigma
:: forall k (a :: k) (f :: k -> Type)
. (SingI a, D.SDecide k)
=> Sigma f
-> Maybe (f a)
fromSigma (Sigma s f) =
case s D.%~ sing @a of
D.Proved D.Refl -> Just f
D.Disproved _ -> Nothing
class Dict1 c (f :: k -> Type) where
dict1 :: Sing (a :: k) -> Dict (c (f a))
data LogType = JsonMsg | TextMsg deriving (Eq, Ord, Show)
$(genSingletons [''LogType])
$(singDecideInstance ''LogType)
data family LogMsg (msg :: LogType)
newtype instance LogMsg 'JsonMsg = Json Value deriving (Eq, Show)
newtype instance LogMsg 'TextMsg = Text String deriving (Eq, Show)
instance
( c (LogMsg 'JsonMsg)
, c (LogMsg 'TextMsg)
)
=> Dict1 c LogMsg
where
dict1 SJsonMsg = Dict
dict1 STextMsg = Dict
catSigmas
:: forall k (a :: k) f
. ( SingI a
, D.SDecide k
)
=> [Sigma f]
-> [f a]
catSigmas = mapMaybe fromSigma
logs :: [Sigma LogMsg]
logs =
[ toSigma $ Text "hello"
, toSigma $ Json $ object ["world" .= (5 :: Int)]
, toSigma $ Text "structured logging"
]
jsonLogs :: [LogMsg 'JsonMsg]
jsonLogs = catSigmas logs
textLogs :: [LogMsg 'TextMsg]
textLogs = catSigmas logs
|
