main.bend

mlbend-report@0.1.0.0 · 254 lines · 27 definitions

1# mlbend-report: the confusion matrix and the per-class report, natively in Bend 2.
2#
3#   import mlbend-report@0.1.0.0/main.bend as R
4#
5# What an estimator's predictions look like: the confusion matrix of a
6# classification, and the per-class report scikit-learn's
7# classification_report prints — the precision, the recall, the F1 and
8# the support of every class, with the macro and the weighted averages.
9# The labels are Nat: the class 0, the class 1, and so on up to k-1.
10#
11# The per-class numbers rest on mlbend-metrics' counts and on its
12# zero-division convention: a class nobody predicted scores 0.0, the
13# way scikit-learn's zero_division=0 does.
14#
15# What is proved: the shape of the matrix. The matrix of k classes has
16# k rows (matrix_rows) and every row k cells (row_length). What is
17# tested: the F32 numbers, against scikit-learn's confusion_matrix and
18# classification_report (reference/test_report.py). F32 is not a real
19# number, so a report's value is never proved, only its shape.
20
21import Base
22import mlbend-metrics@0.1.0.0/main.bend as M
23
24# The report of one class: its scores, and how many samples it has.
25
26type Cls is Data:
27  Cls{precision: F32, recall: F32, f1: F32, support: Nat}
28
29# The whole report: one Cls per class, the averages over them, and the
30# accuracy.
31
32type Report is Data:
33  Report{classes: List<&2, Cls>, macro_avg: Cls, weighted_avg: Cls, accuracy: F32}
34
35# The matrix
36# ----------
37#
38# The confusion matrix, cell by cell. The row is the true label, the
39# column the predicted one, the way scikit-learn's confusion_matrix
40# lays it out.
41
42# The cell of the true label i and the predicted label j: how many
43# samples have both.
44def cell.go(ys: List<&2, Nat>, ps: List<&2, Nat>, +i: Nat, +j: Nat, n: Nat) -> Nat:
45  match ys ps:
46    case Con{y, yt} Con{p, pt}:
47      cell.go(yt, pt, i, j, (n + M.same(y, i) * M.same(p, j) : Nat))
48    case _ _:
49      n
50
51def cell(ys: List<&2, Nat>, ps: List<&2, Nat>, +i: Nat, +j: Nat) -> Nat:
52  cell.go(ys, ps, i, j, 0n)
53
54# How many rows a matrix has.
55def rows_of(m: List<&2, List<&2, Nat>>) -> Nat:
56  match m:
57    case Nil{}:
58      0n
59    case Con{h, t}:
60      (1n + rows_of(t) : Nat)
61
62# How many cells a row has.
63def cells_of(row: List<&2, Nat>) -> Nat:
64  match row:
65    case Nil{}:
66      0n
67    case Con{h, t}:
68      (1n + cells_of(t) : Nat)
69
70# The row of the class i, from the column j on: n cells, the cell of
71# every class from j to j+n-1, ascending. The counted form is the
72# public one, because the law walks it: the counter of the cells left
73# is the argument that shrinks.
74def row_from(+ys: List<&2, Nat>, +ps: List<&2, Nat>, +k: Nat, +i: Nat, n: Nat, +j: Nat) ->
75  List<&2, Nat>:
76  match n:
77    case 0n:
78      Nil{}
79    case 1n+rest:
80      Con{cell(ys, ps, i, j), row_from(ys, ps, k, i, rest, (1n + j : Nat))}
81
82# The row of the class i: k cells, ascending.
83def row(ys: List<&2, Nat>, ps: List<&2, Nat>, +k: Nat, +i: Nat) -> List<&2, Nat>:
84  row_from(ys, ps, k, i, k, 0n)
85
86# The rows of the classes i to i+n-1: n rows, each of k cells, ascending.
87def matrix_from(+ys: List<&2, Nat>, +ps: List<&2, Nat>, +k: Nat, n: Nat, +i: Nat) ->
88  List<&2, List<&2, Nat>>:
89  match n:
90    case 0n:
91      Nil{}
92    case 1n+rest:
93      Con{row(ys, ps, k, i), matrix_from(ys, ps, k, rest, (1n + i : Nat))}
94
95# The confusion matrix of k classes: k rows of k cells, the row of the
96# class 0 first.
97def matrix(ys: List<&2, Nat>, ps: List<&2, Nat>, +k: Nat) ->
98  List<&2, List<&2, Nat>>:
99  matrix_from(ys, ps, k, k, 0n)
100
101# LAW 1 (matrix_rows): n rows of the matrix are n rows.
102law matrix_rows:
103  for +ys: List<&2, Nat>
104  for +ps: List<&2, Nat>
105  for +k: Nat
106  for +n: Nat
107  for +i: Nat
108  {rows_of(matrix_from(ys, ps, k, n, i)) == n : Nat}
109
110# n rows of the matrix are n rows
111def matrix_rows(ys, ps, k, n, i):
112  match n:
113    case 0n:
114      {==}
115    case 1n+rest:
116      %matrix_rows(ys, ps, k, rest, (1n + i : Nat)) :
117        {1n+rows_of(matrix_from(ys, ps, k, rest, (1n + i : Nat))) == 1n+_ : Nat}
118      {==}
119
120# LAW 2 (row_length): n cells of a row are n cells.
121law row_length:
122  for +ys: List<&2, Nat>
123  for +ps: List<&2, Nat>
124  for +k: Nat
125  for +i: Nat
126  for +n: Nat
127  for +j: Nat
128  {cells_of(row_from(ys, ps, k, i, n, j)) == n : Nat}
129
130# n cells of a row are n cells
131def row_length(ys, ps, k, i, n, j):
132  match n:
133    case 0n:
134      {==}
135    case 1n+rest:
136      %row_length(ys, ps, k, i, rest, (1n + j : Nat)) :
137        {1n+cells_of(row_from(ys, ps, k, i, rest, (1n + j : Nat))) == 1n+_ : Nat}
138      {==}
139
140# The classes
141# -----------
142#
143# The per-class scores, on the counts of mlbend-metrics. The caller has
144# checked that the labels and the predictions agree in length and that
145# there is at least one sample; the gated entry is `report`.
146
147# The report of one class: its precision, its recall, its F1 and its
148# support.
149def cls_of(+ys: List<&2, Nat>, +ps: List<&2, Nat>, +i: Nat) -> Cls:
150  +hits = M.count_both(ys, ps, i)
151  +support = M.count_true(ys, i)
152  +p = M.ratio(hits, M.count_pred(ps, i))
153  +r = M.ratio(hits, support)
154  Cls{p, r, M.f1_num(p, r), support}
155
156# The report of every class, from the class i on: n of them, ascending.
157def classes_of.go(+ys: List<&2, Nat>, +ps: List<&2, Nat>, n: Nat, +i: Nat) ->
158  List<&2, Cls>:
159  match n:
160    case 0n:
161      Nil{}
162    case 1n+rest:
163      Con{cls_of(ys, ps, i), classes_of.go(ys, ps, rest, (1n + i : Nat))}
164
165# The report of every class: k of them, the class 0 first.
166def classes_of(ys: List<&2, Nat>, ps: List<&2, Nat>, +k: Nat) -> List<&2, Cls>:
167  classes_of.go(ys, ps, k, 0n)
168
169# The averages
170# ------------
171
172# The sums the averages rest on: the per-class scores added up, and the
173# support beside them.
174type Tot is Data:
175  Tot{p: F32, r: F32, f: F32, support: Nat}
176
177# One class more, added into the sums.
178def tot_add(t: Tot, c: Cls) -> Tot:
179  match t:
180    case Tot{p, r, f, support}:
181      match c:
182        case Cls{p2, r2, f2, support2}:
183          Tot{(p + p2 : F32), (r + r2 : F32), (f + f2 : F32), (support + support2 : Nat)}
184
185# The sums over the classes.
186def tot_of.go(classes: List<&2, Cls>, acc: Tot) -> Tot:
187  match classes:
188    case Nil{}:
189      acc
190    case Con{c, t}:
191      tot_of.go(t, tot_add(acc, c))
192
193def tot_of(classes: List<&2, Cls>) -> Tot:
194  tot_of.go(classes, Tot{0.0, 0.0, 0.0, 0n})
195
196# a divided by b, or 0.0 when b is zero — the zero_division convention
197def divide(+a: F32, +b: F32) -> F32:
198  Bool.pick(F32, F32.is_eq(b, 0.0), 0.0, (a / b : F32))
199
200def macro_of.go(t: Tot, +k: Nat) -> Cls:
201  match t:
202    case Tot{p, r, f, support}:
203      +n = F32.from_nat(k)
204      Cls{divide(p, n), divide(r, n), divide(f, n), support}
205
206# The macro average: the mean of the per-class scores, every class
207# weighing the same, the way scikit-learn's macro average does.
208def macro_of(classes: List<&2, Cls>, +k: Nat) -> Cls:
209  macro_of.go(tot_of(classes), k)
210
211# The weighted sums: every per-class score multiplied by its support.
212def weighted_sums(classes: List<&2, Cls>, +p: F32, +r: F32, +f: F32) -> Tot:
213  match classes:
214    case Nil{}:
215      Tot{p, r, f, 0n}
216    case Con{c, t}:
217      match c:
218        case Cls{p2, r2, f2, s2}:
219          +w = F32.from_nat(s2)
220          weighted_sums(t, (p + p2 * w : F32), (r + r2 * w : F32), (f + f2 * w : F32))
221
222def weighted_of.go(t: Tot, +total: Nat) -> Cls:
223  match t:
224    case Tot{p, r, f, support}:
225      +n = F32.from_nat(total)
226      Cls{divide(p, n), divide(r, n), divide(f, n), total}
227
228# The weighted average: the per-class scores, each weighed by its
229# support, over the total support, the way scikit-learn's weighted
230# average does.
231def weighted_of(classes: List<&2, Cls>, +total: Nat) -> Cls:
232  weighted_of.go(weighted_sums(classes, 0.0, 0.0, 0.0), total)
233
234# The report
235# ----------
236
237# The whole report, or why there is none: the labels and the
238# predictions must agree in length, and there must be at least one
239# sample.
240def report.go(r: Result<&1, &1, M.Bad, Nat>, +ys: List<&2, Nat>, +ps: List<&2, Nat>, +k: Nat) ->
241  Result<&1, &1, M.Bad, Report>:
242  match r:
243    case Done{+n}:
244      +classes = classes_of(ys, ps, k)
245      Done{Report{classes, macro_of(classes, k), weighted_of(classes, n),
246        M.ratio(M.count_right(ys, ps), n)}}
247    case Fail{M.Mismatch{expected, got}}:
248      Fail{M.Mismatch{expected, got}}
249    case Fail{M.Empty{}}:
250      Fail{M.Empty{}}
251
252def report(+ys: List<&2, Nat>, +ps: List<&2, Nat>, +k: Nat) ->
253  Result<&1, &1, M.Bad, Report>:
254  report.go(M.pairs(&2, Nat, ys, ps), ys, ps, k)