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	
21	import Base
22	import 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	
26	type 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	
32	type 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.
44	def 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	
51	def 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.
55	def 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.
63	def 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.
74	def 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.
83	def 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.
87	def 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.
97	def 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.
102	law 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
111	def 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.
121	law 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
131	def 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.
149	def 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.
157	def 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.
166	def 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.
174	type Tot is Data:
175	  Tot{p: F32, r: F32, f: F32, support: Nat}
176	
177	# One class more, added into the sums.
178	def 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.
186	def 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	
193	def 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
197	def divide(+a: F32, +b: F32) -> F32:
198	  Bool.pick(F32, F32.is_eq(b, 0.0), 0.0, (a / b : F32))
199	
200	def 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.
208	def 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.
212	def 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	
222	def 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.
231	def 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.
240	def 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	
252	def 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)