4
4
module Functora.TagsFamily
5
5
( -- * Constructors
6
6
-- $constructors
7
- TagsKind ,
8
7
type Tags ,
8
+ type NoTags ,
9
9
type (|+| ),
10
10
type (|-| ),
11
11
type (|&| ),
12
- type NoTags ,
13
12
14
13
-- * Accessors
15
14
-- $accessors
16
- HasKey ,
17
- HasNotKey ,
18
- HasTag ,
19
- HasTags ,
20
15
GetTag ,
21
16
GetKey ,
22
- GetTagDef ,
23
17
24
- -- * Introspection
25
- -- $introspection
18
+ -- * Fingerprints
19
+ -- $fingerprints
26
20
Fgpt ,
27
21
mkFgpt ,
28
- inspectTags ,
29
22
30
23
-- * Reexport
31
24
module X ,
34
27
35
28
import Data.Data as X (Data )
36
29
import Data.Kind (Type )
37
- import Data.String (IsString , fromString )
38
30
import Data.Type.Bool as X (type Not , type (&& ))
39
31
import Data.Type.Equality as X (type (== ))
40
- import Data.Type.Map (AsMap , Cmp , IsMap , Lookup , Mapping ((:->) ), Member )
32
+ import Data.Type.Map (AsMap , Cmp , Mapping ((:->) ))
41
33
import Data.Typeable
42
34
import qualified Data.Typeable as Typeable
43
35
import GHC.Generics as X (Generic )
@@ -53,14 +45,15 @@ import qualified LiftType
53
45
import Singlethongs as X
54
46
import Prelude
55
47
56
- type TagsKind = [Mapping Type Type ]
57
-
58
- type NoTags = ('[] :: [Mapping Type Type ])
48
+ -- $constructors
49
+ -- Constructors
59
50
60
51
type family Tags v where
61
52
Tags (v :: k ) =
62
53
'[k ':-> Sing v ]
63
54
55
+ type NoTags = ('[] :: [Mapping Type Type ])
56
+
64
57
type family tags |+| v where
65
58
tags |+| v =
66
59
AsMap (AddTagFamily v tags tags '[] )
@@ -71,41 +64,20 @@ type family tags |-| v where
71
64
72
65
type family lhs |&| rhs where
73
66
'[] |&| rhs = AsMap rhs
74
- ((_ ':-> v ) ': lhs ) |&| rhs = ( lhs |&| (rhs |+| v ) )
67
+ ((_ ':-> v ) ': lhs ) |&| rhs = lhs |&| (rhs |+| v )
75
68
76
- type HasKey k tags =
77
- ( IsMap tags ,
78
- Typeable (GetVals tags ),
79
- Member k tags ~ 'True
80
- )
81
-
82
- type HasNotKey k tags =
83
- ( IsMap tags ,
84
- Typeable (GetVals tags ),
85
- Member k tags ~ 'False
86
- )
87
-
88
- type HasTag v tags =
89
- ( HasTags (Tags v ) tags
90
- )
91
-
92
- type HasTags sub sup =
93
- ( IsMap sub ,
94
- IsMap sup ,
95
- Typeable (GetVals sub ),
96
- Typeable (GetVals sup ),
97
- HasTagsFamily 'Nothing sub sup ~ 'True
98
- )
69
+ -- $accessors
70
+ -- Accessors
99
71
100
72
type GetTag (v :: k ) tags =
101
- ( v ~ GetTagFamily k tags tags ,
102
- SingI v ,
103
- HasTag v tags
73
+ ( v ~ GetTagFamily ('Nothing :: Maybe k ) k tags tags ,
74
+ SingI v
104
75
)
105
76
106
- type GetKey k tags = GetTagFamily k tags tags
77
+ type GetKey k tags = GetTagFamily ('Nothing :: Maybe k ) k tags tags
107
78
108
- type GetTagDef (def :: k ) tags = GetTagDefFamily def tags tags
79
+ -- $fingerprints
80
+ -- Fingerprints
109
81
110
82
type family Fgpt (a :: k ) :: Symbol
111
83
@@ -135,18 +107,6 @@ mkFgpt =
135
107
)
136
108
|]
137
109
138
- inspectTags ::
139
- forall tags text vals .
140
- ( HasVals vals tags ,
141
- IsString text
142
- ) =>
143
- text
144
- inspectTags =
145
- fromString
146
- . show
147
- . Typeable. typeRep
148
- $ Proxy @ vals
149
-
150
110
--
151
111
-- Private
152
112
--
@@ -189,58 +149,26 @@ type family UnTagFamily member v tags prev next where
189
149
UnTagFamily member v tags (kv ': prev ) next =
190
150
UnTagFamily member v tags prev (kv ': next )
191
151
192
- type family GetTagFamily k tags prev where
193
- GetTagFamily k _ ((k ':-> Sing v ) ': _ ) = v
194
- GetTagFamily k tags (_ ': next ) = GetTagFamily k tags next
195
- GetTagFamily k tags '[] =
152
+ type family GetTagFamily mv k tags prev where
153
+ GetTagFamily ('Just (v :: k )) k _ '[] = v
154
+ GetTagFamily 'Nothing k tags '[] =
196
155
TypeError
197
156
( 'ShowType k
198
157
':<>: 'Text " key is missing in "
199
158
':<>: 'ShowType tags
200
159
)
201
-
202
- type family GetTagDefFamily (def :: k ) tags prev where
203
- GetTagDefFamily (_ :: k ) _ ((k ':-> Sing v ) ': _ ) = v
204
- GetTagDefFamily def tags (_ ': next ) = GetTagDefFamily def tags next
205
- GetTagDefFamily def _ '[] = def
206
-
207
- type family HasTagsFamily hastag submap supmap where
208
- HasTagsFamily 'Nothing '[] _ = 'True
209
- HasTagsFamily has '[] sup =
210
- TypeError
211
- ( 'Text " Impossible HasTagsFamily "
212
- ':<>: 'ShowType has
213
- ':<>: 'Text " clause with "
214
- ':<>: 'ShowType sup
215
- )
216
- HasTagsFamily 'Nothing ((k ':-> v ) ': sub ) sup =
217
- HasTagsFamily
218
- ('Just (Lookup sup k == 'Just v ))
219
- ((k ':-> v ) ': sub )
220
- sup
221
- HasTagsFamily ('Just 'True) (_ ': sub ) sup =
222
- HasTagsFamily 'Nothing sub sup
223
- HasTagsFamily ('Just 'False) ((k ':-> v ) ': _ ) sup =
160
+ GetTagFamily ('Just v ) k tags ((k ':-> Sing v ) ': _ ) =
224
161
TypeError
225
162
( 'ShowType v
226
163
':<>: 'Text " :: "
227
164
':<>: 'ShowType k
228
- ':<>: 'Text " tag is missing in "
229
- ':<>: 'ShowType sup
165
+ ':<>: 'Text " tag conflicts with "
166
+ ':<>: 'ShowType tags
230
167
)
231
-
232
- type family ToValsFamily map lst where
233
- ToValsFamily '[] acc = acc
234
- ToValsFamily ((_ ':-> v ) ': tail ) acc =
235
- ToValsFamily tail (v ': acc )
236
-
237
- type GetVals tags = ToValsFamily tags '[]
238
-
239
- type HasVals vals tags =
240
- ( IsMap tags ,
241
- Typeable vals ,
242
- vals ~ GetVals tags
243
- )
168
+ GetTagFamily 'Nothing k tags ((k ':-> Sing v ) ': next ) =
169
+ GetTagFamily ('Just v ) k tags next
170
+ GetTagFamily mv k tags (_ ': next ) =
171
+ GetTagFamily mv k tags next
244
172
245
173
--
246
174
-- TODO : NEED A PROPER INSTANCE!
0 commit comments