blob: bbaaa5712fcdcc9389d201a450e28e12d8ee14d1 (
plain)
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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
|
(.module:
[lux (#- type)
["%" data/text/format (#+ format)]
["r" math/random (#+ Random)]
["_" test (#+ Test)]
[abstract
["." monad (#+ do)]]
[control
[pipe (#+ case>)]]
[data
["." product]
["." maybe]
["." text ("#\." equivalence)]
[number
["n" nat]]
[collection
["." list ("#\." functor)]
["." set]]]
["." type ("#\." equivalence)]]
{1
["." /]})
## TODO: Remove the following 3 definitions ASAP. //.type already exists...
(def: short
(r.Random Text)
(r.unicode 10))
(def: name
(r.Random Name)
(r.and ..short ..short))
(def: (type' num-vars)
(-> Nat (r.Random Type))
(do r.monad
[_ (wrap [])]
(let [(^open "R\.") r.monad
pairG (r.and (type' num-vars)
(type' num-vars))
quantifiedG (r.and (R\wrap (list)) (type' (inc num-vars)))
random-pair (r.either (r.either (R\map (|>> #.Sum) pairG)
(R\map (|>> #.Product) pairG))
(r.either (R\map (|>> #.Function) pairG)
(R\map (|>> #.Apply) pairG)))
random-id (let [random-id (r.either (R\map (|>> #.Var) r.nat)
(R\map (|>> #.Ex) r.nat))]
(case num-vars
0 random-id
_ (r.either (R\map (|>> (n.% num-vars) (n.* 2) inc #.Parameter) r.nat)
random-id)))
random-quantified (r.either (R\map (|>> #.UnivQ) quantifiedG)
(R\map (|>> #.ExQ) quantifiedG))]
($_ r.either
(R\map (|>> #.Primitive) (r.and ..short (R\wrap (list))))
random-pair
random-id
random-quantified
(R\map (|>> #.Named) (r.and ..name (type' num-vars)))
))))
(def: type
(r.Random Type)
(..type' 0))
(def: (valid-type? type)
(-> Type Bit)
(case type
(#.Primitive name params)
(list.every? valid-type? params)
(#.Ex id)
#1
(^template [<tag>]
[(<tag> left right)
(and (valid-type? left) (valid-type? right))])
([#.Sum] [#.Product] [#.Function])
(#.Named name type')
(valid-type? type')
_
#0))
(def: (type-checks? input)
(-> (/.Check []) Bit)
(case (/.run /.fresh-context input)
(#.Right [])
#1
(#.Left error)
#0))
(def: (build-ring num-connections)
(-> Nat (/.Check [[Nat Type] (List [Nat Type]) [Nat Type]]))
(do {! /.monad}
[[head-id head-type] /.var
ids+types (monad.seq ! (list.repeat num-connections /.var))
[tail-id tail-type] (monad.fold ! (function (_ [tail-id tail-type] [_head-id _head-type])
(do !
[_ (/.check head-type tail-type)]
(wrap [tail-id tail-type])))
[head-id head-type]
ids+types)]
(wrap [[head-id head-type] ids+types [tail-id tail-type]])))
(def: #export test
Test
(<| (_.context (%.name (name-of /._)))
($_ _.and
(do r.monad
[sample (r.filter ..valid-type? ..type)]
($_ _.and
(_.test "Any is the super-type of everything."
(/.checks? Any sample))
(_.test "Nothing is the sub-type of everything."
(/.checks? sample Nothing))
))
($_ _.and
(_.test "Any and Nothing match themselves."
(and (/.checks? Nothing Nothing)
(/.checks? Any Any)))
(_.test "Existential types only match with themselves."
(and (type-checks? (do /.monad
[[_ exT] /.existential]
(/.check exT exT)))
(not (type-checks? (do /.monad
[[_ exTL] /.existential
[_ exTR] /.existential]
(/.check exTL exTR))))))
(_.test "Names do not affect type-checking."
(and (type-checks? (do /.monad
[[_ exT] /.existential]
(/.check (#.Named ["module" "name"] exT)
exT)))
(type-checks? (do /.monad
[[_ exT] /.existential]
(/.check exT
(#.Named ["module" "name"] exT))))
(type-checks? (do /.monad
[[_ exT] /.existential]
(/.check (#.Named ["module" "name"] exT)
(#.Named ["module" "name"] exT))))))
(_.test "Functions are covariant on inputs and contravariant on outputs."
(and (/.checks? (#.Function Nothing Any)
(#.Function Any Nothing))
(not (/.checks? (#.Function Any Nothing)
(#.Function Nothing Any)))))
)
(do r.monad
[meta ..type
data ..type]
(_.test "Can type-check type application."
(and (/.checks? (|> Ann (#.Apply meta) (#.Apply data))
(type.tuple (list meta data)))
(/.checks? (type.tuple (list meta data))
(|> Ann (#.Apply meta) (#.Apply data))))))
(do r.monad
[#let [gen-short (r.ascii 10)]
nameL gen-short
nameR (|> gen-short (r.filter (|>> (text\= nameL) not)))
paramL ..type
paramR (r.filter (|>> (/.checks? paramL) not) ..type)]
($_ _.and
(_.test "Primitive types match when they have the same name and the same parameters."
(/.checks? (#.Primitive nameL (list paramL))
(#.Primitive nameL (list paramL))))
(_.test "Names matter to primitive types."
(not (/.checks? (#.Primitive nameL (list paramL))
(#.Primitive nameR (list paramL)))))
(_.test "Parameters matter to primitive types."
(not (/.checks? (#.Primitive nameL (list paramL))
(#.Primitive nameL (list paramR)))))
))
($_ _.and
(_.test "Type-vars check against themselves."
(type-checks? (do /.monad
[[id var] /.var]
(/.check var var))))
(_.test "Can bind unbound type-vars by type-checking against them."
(and (type-checks? (do /.monad
[[id var] /.var]
(/.check var .Any)))
(type-checks? (do /.monad
[[id var] /.var]
(/.check .Any var)))))
(_.test "Cannot rebind already bound type-vars."
(not (type-checks? (do /.monad
[[id var] /.var
_ (/.check var .Bit)]
(/.check var .Nat)))))
(_.test "If the type bound to a var is a super-type to another, then the var is also a super-type."
(type-checks? (do /.monad
[[id var] /.var
_ (/.check var Any)]
(/.check var .Bit))))
(_.test "If the type bound to a var is a sub-type of another, then the var is also a sub-type."
(type-checks? (do /.monad
[[id var] /.var
_ (/.check var Nothing)]
(/.check .Bit var))))
)
(do {! r.monad}
[num-connections (|> r.nat (:: ! map (n.% 100)))
boundT (|> ..type (r.filter (|>> (case> (#.Var _) #0 _ #1))))
pick-pcg (r.and r.nat r.nat)]
($_ _.and
(_.test "Can create rings of variables."
(type-checks? (do /.monad
[[[head-id head-type] ids+types [tail-id tail-type]] (build-ring num-connections)
#let [ids (list\map product.left ids+types)]
headR (/.ring head-id)
tailR (/.ring tail-id)]
(/.assert ""
(let [same-rings? (:: set.equivalence = headR tailR)
expected-size? (n.= (inc num-connections) (set.size headR))
same-vars? (|> (set.to-list headR)
(list.sort n.<)
(:: (list.equivalence n.equivalence) = (list.sort n.< (#.Cons head-id ids))))]
(and same-rings?
expected-size?
same-vars?))))))
(_.test "When a var in a ring is bound, all the ring is bound."
(type-checks? (do {! /.monad}
[[[head-id headT] ids+types tailT] (build-ring num-connections)
#let [ids (list\map product.left ids+types)]
_ (/.check headT boundT)
head-bound (/.read head-id)
tail-bound (monad.map ! /.read ids)
headR (/.ring head-id)
tailR+ (monad.map ! /.ring ids)]
(let [rings-were-erased? (and (set.empty? headR)
(list.every? set.empty? tailR+))
same-types? (list.every? (type\= boundT) (list& (maybe.default headT head-bound)
(list\map (function (_ [tail-id ?tailT])
(maybe.default (#.Var tail-id) ?tailT))
(list.zip/2 ids tail-bound))))]
(/.assert ""
(and rings-were-erased?
same-types?))))))
(_.test "Can merge multiple rings of variables."
(type-checks? (do /.monad
[[[head-idL headTL] ids+typesL [tail-idL tailTL]] (build-ring num-connections)
[[head-idR headTR] ids+typesR [tail-idR tailTR]] (build-ring num-connections)
headRL-pre (/.ring head-idL)
headRR-pre (/.ring head-idR)
_ (/.check headTL headTR)
headRL-post (/.ring head-idL)
headRR-post (/.ring head-idR)]
(/.assert ""
(let [same-rings? (:: set.equivalence = headRL-post headRR-post)
expected-size? (n.= (n.* 2 (inc num-connections))
(set.size headRL-post))
union? (:: set.equivalence = headRL-post (set.union headRL-pre headRR-pre))]
(and same-rings?
expected-size?
union?))))))
))
)))
|
