main.bend

mlbend-select@0.1.0.0 · 79 lines · 9 definitions

1# mlbend-select: k-fold cross-validation on top of the split.
2#
3#   import mlbend-select@0.1.0.0/main.bend as Select
4#
5# The folds are the ones `mlbend-split` makes, so the two agree by
6# construction: the same seed and the same labels give the same folds.
7# The package adds the walk over the folds — the rows of each fold, the
8# training rows of each fold, and the sizes — so a model can be fitted
9# and scored fold by fold without writing the loop again.
10#
11# What is proved: every row of the dataset is in exactly one fold
12# (`select_covers`) — the fold list holds one entry per row, so the
13# folds cover the dataset exactly once each. What is tested: that the
14# fold sizes and the class counts agree with scikit-learn's
15# `StratifiedKFold` (reference/test_select.py).
16
17import Base
18import mlbend-split@0.1.1.0/main.bend as Split
19
20# The rows of one fold: the ones that test and the ones that train.
21
22type Fold is Data:
23  Fold{test: List<&2, Nat>, train: List<&2, Nat>}
24
25# LAW (select_covers): every row of the dataset is in exactly one fold —
26# the fold list holds one entry per row, so the folds cover the dataset
27# exactly once each.
28law select_covers:
29  for labels: List<&2, Nat>
30  for +orders: List<&2, List<&2, Nat>>
31  for +k: Nat
32  for +i: Nat
33  {Split.count_rows(Split.folds_from(labels, orders, k, i)) == List.length(&2, Nat, labels) : Nat}
34
35# The rows of the fold f: the ones that test and the ones that train.
36def fold_of(+fs: List<&2, Nat>, +f: Nat) -> Fold:
37  Fold{Split.test_of(fs, f), Split.train_of(fs, f)}
38
39# The number of rows of the fold f.
40def fold_size(fs: List<&2, Nat>, f: Nat) -> Nat:
41  List.length(&2, Nat, Split.test_of(fs, f))
42
43# The number of rows of each fold.
44def fold_sizes_go(+fs: List<&2, Nat>, k: Nat, +acc: List<&2, Nat>) -> List<&2, Nat>:
45  match k:
46    case 0n:
47      acc
48    case 1n++rest:
49      fold_sizes_go(fs, rest, Con{fold_size(fs, rest), acc})
50
51# The number of rows of each fold.
52def fold_sizes(fs: List<&2, Nat>, k: Nat) -> List<&2, Nat>:
53  fold_sizes_go(fs, k, Nil{})
54
55# The fold of every row of the dataset, in the order of the rows.
56def folds(labels: List<&2, Nat>, seed: U32, k: Nat) -> List<&2, Nat>:
57  Split.folds(labels, seed, k)
58
59# The rows of every fold.
60def folds_go(+fs: List<&2, Nat>, k: Nat, +acc: List<&2, Fold>) -> List<&2, Fold>:
61  match k:
62    case 0n:
63      acc
64    case 1n++rest:
65      folds_go(fs, rest, Con{fold_of(fs, rest), acc})
66
67# The rows of every fold: the test rows of each fold, and the training
68# rows of each fold.
69def folds_of(labels: List<&2, Nat>, seed: U32, +k: Nat) -> List<&2, Fold>:
70  folds_go(Split.folds(labels, seed, k), k, Nil{})
71
72# every row of the dataset is in exactly one fold
73def select_covers(labels, orders, k, i):
74  match labels:
75    case Nil{}:
76      {==}
77    case Con{h, +t}:
78      %select_covers(t, orders, k, Nat.add(i, 1n)) : {1n+Split.count_rows(Split.folds_from(t, orders, k, Nat.add(i, 1n))) == 1n+_ : Nat}
79      {==}