main.bend

mlbend-metrics@0.1.0.0 · 325 lines · 42 definitions

1# mlbend-metrics: the evaluation surface of machine learning, natively in Bend 2.
2#
3#   import mlbend-metrics@0.1.0.0/main.bend as M
4#
5# A metric compares two sequences of the same length. The length is not
6# trusted: every metric answers a Result, and a mismatch of lengths (or
7# an empty input) is a value, never a crash.
8#
9# What is proved: the counts. What is tested: the F32 numbers, against
10# NumPy and scikit-learn (reference/test_metrics.py). F32 is not a real
11# number, so a metric's value is never proved, only its shape.
12
13import Base
14import bend-ml-nat-lemmas@0.1.1.0/main.bend as NL
15
16# Bad
17# ---
18#
19# Why a metric could not answer.
20
21type Bad is Data:
22  Mismatch{expected: Nat, got: Nat}
23  Empty{}
24
25# Counts
26# ------
27#
28# The counting core, over Nat, so that it can be proved. A count walks
29# the labels; the walks over two sequences stop at the shorter one (the
30# metrics check the lengths first).
31
32# 1 when a and b are the same label, 0 otherwise
33def same_of(s: Bool) -> Nat:
34  match s:
35    case True{}:
36      1n
37    case False{}:
38      0n
39
40def same(a: Nat, b: Nat) -> Nat:
41  same_of(Nat.is_eq(a, b))
42
43# the number of samples
44def count(ys: List<&2, Nat>) -> Nat:
45  match ys:
46    case Nil{}:
47      0n
48    case Con{h, t}:
49      (1n + count(t) : Nat)
50
51# the number of samples whose true label is k
52def count_true.go(ys: List<&2, Nat>, +k: Nat, n: Nat) -> Nat:
53  match ys:
54    case Nil{}:
55      n
56    case Con{y, yt}:
57      count_true.go(yt, k, (n + same(y, k) : Nat))
58
59def count_true(ys: List<&2, Nat>, k: Nat) -> Nat:
60  count_true.go(ys, k, 0n)
61
62# the number of samples whose predicted label is k
63def count_pred.go(ps: List<&2, Nat>, +k: Nat, n: Nat) -> Nat:
64  match ps:
65    case Nil{}:
66      n
67    case Con{p, pt}:
68      count_pred.go(pt, k, (n + same(p, k) : Nat))
69
70def count_pred(ps: List<&2, Nat>, k: Nat) -> Nat:
71  count_pred.go(ps, k, 0n)
72
73# the number of samples whose true label is k and whose predicted label
74# is k too: the true positives of the class k
75def count_both.go(ys: List<&2, Nat>, ps: List<&2, Nat>, +k: Nat, n: Nat) -> Nat:
76  match ys ps:
77    case Con{y, yt} Con{p, pt}:
78      count_both.go(yt, pt, k, (n + same(y, k) * same(p, k) : Nat))
79    case _ _:
80      n
81
82def count_both(ys: List<&2, Nat>, ps: List<&2, Nat>, k: Nat) -> Nat:
83  count_both.go(ys, ps, k, 0n)
84
85# the number of samples predicted right
86def count_right.go(ys: List<&2, Nat>, ps: List<&2, Nat>, n: Nat) -> Nat:
87  match ys ps:
88    case Con{y, yt} Con{p, pt}:
89      count_right.go(yt, pt, (n + same(y, p) : Nat))
90    case _ _:
91      n
92
93def count_right(ys: List<&2, Nat>, ps: List<&2, Nat>) -> Nat:
94  count_right.go(ys, ps, 0n)
95
96# LAW 1 (count_length): the number of samples is the length of the list
97# of labels. (The count is this package's own walk, so the law pins it
98# to the length Base counts.)
99law count_length:
100  for ys: List<&2, Nat>
101  {count(ys) == List.length(&2, Nat, ys) : Nat}
102
103# the number of samples is the length of the list of labels
104def count_length(ys):
105  match ys:
106    case Nil{}:
107      {==}
108    case Con{h, t}:
109      %count_length(t) : {1n+count(t) == 1n+_ : Nat}
110      {==}
111
112# Sums
113# -----
114#
115# The sums the error metrics need: the walk over the two sequences, with
116# the number of pairs walked beside the sum.
117
118type Sum is Data:
119  Sum{n: Nat, s: F32}
120
121def sum_add(a: Sum, x: F32) -> Sum:
122  match a:
123    case Sum{n, s}:
124      Sum{(1n + n : Nat), (s + x : F32)}
125
126# the sum of the squared differences of the pairs walked
127def sq_sum.go(ys: List<&2, F32>, ps: List<&2, F32>, acc: Sum) -> Sum:
128  match ys ps:
129    case Con{y, yt} Con{p, pt}:
130      +d = (y - p : F32);
131      sum_add(sq_sum.go(yt, pt, acc), (d * d : F32))
132    case _ _:
133      acc
134
135# the sum of the absolute differences of the pairs walked
136def abs_sum.go(ys: List<&2, F32>, ps: List<&2, F32>, acc: Sum) -> Sum:
137  match ys ps:
138    case Con{y, yt} Con{p, pt}:
139      d = F32.abs((y - p : F32));
140      sum_add(abs_sum.go(yt, pt, acc), d)
141    case _ _:
142      acc
143
144# Ratios
145# ------
146#
147# A metric that divides: the ratio of two counts, and the mean of a sum
148# over a number of pairs. A zero denominator answers 0.0, the
149# convention scikit-learn uses (zero_division=0).
150
151# the ratio a over b, or 0.0 when b is zero
152def ratio_of(z: Bool, +a: Nat, +b: Nat) -> F32:
153  match z:
154    case True{}:
155      0.0
156    case False{}:
157      (F32.from_nat(a) / F32.from_nat(b) : F32)
158
159def ratio(+a: Nat, +b: Nat) -> F32:
160  ratio_of(Nat.is_eq(b, 0n), a, b)
161
162# the mean of a sum over n pairs
163def mean(s: Sum, n: Nat) -> F32:
164  match s:
165    case Sum{n0, s0}:
166      (s0 / F32.from_nat(n) : F32)
167
168# Metrics
169# -------
170#
171# Every metric answers a Result: the value, or why it could not answer.
172
173# the number of pairs to walk, or why the two sequences do not agree
174def same_len_of(s: Bool, +n: Nat, +m: Nat) -> Result<&1, &1, Bad, Nat>:
175  match s:
176    case True{}:
177      Done{n}
178    case False{}:
179      Fail{Mismatch{n, m}}
180
181def same_len(+n: Nat, +m: Nat) -> Result<&1, &1, Bad, Nat>:
182  same_len_of(Nat.is_eq(n, m), n, m)
183
184# the number of pairs to walk, or why there are none
185def not_empty_of(z: Bool, n: Nat) -> Result<&1, &1, Bad, Nat>:
186  match z:
187    case True{}:
188      Fail{Empty{}}
189    case False{}:
190      Done{n}
191
192# the number of pairs, or why there is no answer
193def not_empty(r: Result<&1, &1, Bad, Nat>) -> Result<&1, &1, Bad, Nat>:
194  match r:
195    case Done{+n}:
196      not_empty_of(Nat.is_eq(n, 0n), n)
197    case Fail{Mismatch{expected, got}}:
198      Fail{Mismatch{expected, got}}
199    case Fail{Empty{}}:
200      Fail{Empty{}}
201
202# the number of pairs the two sequences hold, or why there is no answer
203def pairs(a, -A: Kind(a), ys: List<a, A>, ps: List<a, A>) -> Result<&1, &1, Bad, Nat>:
204  not_empty(same_len(List.length(a, A, ys), List.length(a, A, ps)))
205
206# the mean squared error between the targets and the predictions
207def mse.go(r: Result<&1, &1, Bad, Nat>, +ys: List<&2, F32>, +ps: List<&2, F32>) -> Result<&1, &1, Bad, F32>:
208  match r:
209    case Done{n}:
210      Done{mean(sq_sum.go(ys, ps, Sum{0n, 0.0}), n)}
211    case Fail{Mismatch{expected, got}}:
212      Fail{Mismatch{expected, got}}
213    case Fail{Empty{}}:
214      Fail{Empty{}}
215
216def mse(+ys: List<&2, F32>, +ps: List<&2, F32>) -> Result<&1, &1, Bad, F32>:
217  mse.go(pairs(&2, F32, ys, ps), ys, ps)
218
219# the mean absolute error between the targets and the predictions
220def mae.go(r: Result<&1, &1, Bad, Nat>, +ys: List<&2, F32>, +ps: List<&2, F32>) -> Result<&1, &1, Bad, F32>:
221  match r:
222    case Done{n}:
223      Done{mean(abs_sum.go(ys, ps, Sum{0n, 0.0}), n)}
224    case Fail{Mismatch{expected, got}}:
225      Fail{Mismatch{expected, got}}
226    case Fail{Empty{}}:
227      Fail{Empty{}}
228
229def mae(+ys: List<&2, F32>, +ps: List<&2, F32>) -> Result<&1, &1, Bad, F32>:
230  mae.go(pairs(&2, F32, ys, ps), ys, ps)
231
232# the root mean squared error between the targets and the predictions
233def rmse.go(r: Result<&1, &1, Bad, Nat>, +ys: List<&2, F32>, +ps: List<&2, F32>) -> Result<&1, &1, Bad, F32>:
234  match r:
235    case Done{n}:
236      Done{F32.sqrt(mean(sq_sum.go(ys, ps, Sum{0n, 0.0}), n))}
237    case Fail{Mismatch{expected, got}}:
238      Fail{Mismatch{expected, got}}
239    case Fail{Empty{}}:
240      Fail{Empty{}}
241
242def rmse(+ys: List<&2, F32>, +ps: List<&2, F32>) -> Result<&1, &1, Bad, F32>:
243  rmse.go(pairs(&2, F32, ys, ps), ys, ps)
244
245# the fraction of the samples predicted right
246def accuracy.go(r: Result<&1, &1, Bad, Nat>, +ys: List<&2, Nat>, +ps: List<&2, Nat>) -> Result<&1, &1, Bad, F32>:
247  match r:
248    case Done{n}:
249      Done{ratio(count_right(ys, ps), n)}
250    case Fail{Mismatch{expected, got}}:
251      Fail{Mismatch{expected, got}}
252    case Fail{Empty{}}:
253      Fail{Empty{}}
254
255def accuracy(+ys: List<&2, Nat>, +ps: List<&2, Nat>) -> Result<&1, &1, Bad, F32>:
256  accuracy.go(pairs(&2, Nat, ys, ps), ys, ps)
257
258# the fraction of the samples predicted as k that are really k: the
259# precision of the class k
260def precision.go(r: Result<&1, &1, Bad, Nat>, +ys: List<&2, Nat>, +ps: List<&2, Nat>, +k: Nat) -> Result<&1, &1, Bad, F32>:
261  match r:
262    case Done{n}:
263      Done{ratio(count_both(ys, ps, k), count_pred(ps, k))}
264    case Fail{Mismatch{expected, got}}:
265      Fail{Mismatch{expected, got}}
266    case Fail{Empty{}}:
267      Fail{Empty{}}
268
269def precision(+ys: List<&2, Nat>, +ps: List<&2, Nat>, +k: Nat) -> Result<&1, &1, Bad, F32>:
270  precision.go(pairs(&2, Nat, ys, ps), ys, ps, k)
271
272# the fraction of the samples really k that are predicted as k: the
273# recall of the class k
274def recall.go(r: Result<&1, &1, Bad, Nat>, +ys: List<&2, Nat>, +ps: List<&2, Nat>, +k: Nat) -> Result<&1, &1, Bad, F32>:
275  match r:
276    case Done{n}:
277      Done{ratio(count_both(ys, ps, k), count_true(ys, k))}
278    case Fail{Mismatch{expected, got}}:
279      Fail{Mismatch{expected, got}}
280    case Fail{Empty{}}:
281      Fail{Empty{}}
282
283def recall(+ys: List<&2, Nat>, +ps: List<&2, Nat>, +k: Nat) -> Result<&1, &1, Bad, F32>:
284  recall.go(pairs(&2, Nat, ys, ps), ys, ps, k)
285
286# the harmonic mean of two scores
287def f1_num_of(z: Bool, +p: F32, +r: F32) -> F32:
288  match z:
289    case True{}:
290      0.0
291    case False{}:
292      ((2.0 * p * r / (p + r) : F32))
293
294def f1_num(+p: F32, +r: F32) -> F32:
295  f1_num_of(F32.is_eq((p + r : F32), 0.0), p, r)
296
297# the harmonic mean of a precision and a recall
298def f1_of(p: Result<&1, &1, Bad, F32>, r: Result<&1, &1, Bad, F32>) -> Result<&1, &1, Bad, F32>:
299  match p:
300    case Done{pv}:
301      match r:
302        case Done{rv}:
303          Done{f1_num(pv, rv)}
304        case Fail{Mismatch{expected, got}}:
305          Fail{Mismatch{expected, got}}
306        case Fail{Empty{}}:
307          Fail{Empty{}}
308    case Fail{Mismatch{expected, got}}:
309      Fail{Mismatch{expected, got}}
310    case Fail{Empty{}}:
311      Fail{Empty{}}
312
313# the harmonic mean of the precision and the recall of the class k
314def f1.go(r: Result<&1, &1, Bad, Nat>, +ys: List<&2, Nat>, +ps: List<&2, Nat>, +k: Nat) -> Result<&1, &1, Bad, F32>:
315  match r:
316    case Done{+n}:
317      f1_of(precision.go(Done{n}, ys, ps, k), recall.go(Done{n}, ys, ps, k))
318    case Fail{Mismatch{expected, got}}:
319      Fail{Mismatch{expected, got}}
320    case Fail{Empty{}}:
321      Fail{Empty{}}
322
323def f1(+ys: List<&2, Nat>, +ps: List<&2, Nat>, +k: Nat) -> Result<&1, &1, Bad, F32>:
324  f1.go(pairs(&2, Nat, ys, ps), ys, ps, k)
325