LearningCore

Pleasant machine-learning library inspired by ``requests``. Design goals: * The pandas / sklearn ``X``/``y`` split is hidden. Users work with two opaque types — ``DataFrame`` (all columns intact) and ``Dataset`` (features + a designated target column). * Classification and regression are distinguished at the type level (``SklearnClassifier`` vs ``SklearnRegressor``). Metrics are typed against the right kind of model — ``accuracy`` will not type-check against a regressor, ``mse`` will not type-check against a classifier. * A few dataset-consuming operations are linear (``(1 ds: Dataset)``) so callers who bind their source with ``let 1 df = ...`` get a type error if they keep using the pre-transformed dataset. * Refinements carry shape and class invariants. Common ML bugs are rejected at compile time. ─── Pipeline-defect detection (Silva 2024) ───────────────────────────── This library encodes the component contracts from Pedro Silva's MSc thesis *"Static Analysis for Detection of Defects in Machine Learning Pipelines"* (ULisboa 2024). The thesis specifies each component with first-order pre/post-conditions over per-line predicates (``lineInDs``, ``lineCausality``, ``synthesizedLine`` …). Aeon's liquid refinements are quantifier-free, so instead of quantifying over lines we lift those predicates to **dataset-level summary flags** whose values are *fully determined* by each component's post-condition (biconditionals, not implications). This keeps everything decidable and needs no global axioms — the propagation laws live entirely in the contracts below. Summary flags (all uninterpreted ``Dataset -> Bool``): * ``is_timeseries`` — instances are chronologically ordered. * ``has_missing`` — some feature has missing values. * ``coupled`` — a whole-dataset transform (scaling, imputation, resampling, SMOTE) has made rows statistically depend on one another. Splitting a *coupled* dataset leaks information across the partition. * ``clean_test`` — this dataset is a held-out test set produced by a *safe* split (source not coupled, and not a shuffled time series). Only ``split`` ever sets it true, so evaluating on anything else is a type error. * ``independent_target`` — the target does not depend on any feature (no proxy / leaky feature). Defects caught at compile time: - Pre-processing (scale / impute / resample / SMOTE) **before** the train/test split → ``coupled`` source → ``clean_test`` is false. - Temporal leakage: shuffling a time series before splitting → ``clean_test`` is false. - Evaluating on the training data / on a non-split dataset → ``clean_test`` cannot be proven true. - Feeding missing values to an estimator → ``has_missing`` precondition. - Too few instances (``ds_rows <= ds_features * 10``) → ``split`` precondition (decidable for ``create_dataset``; assert it on the CSV path with ``require_enough_data`` before splitting). - A balance-sensitive metric (``accuracy`` / ``precision`` / ``recall``) on an imbalanced test set → ``is_balanced`` precondition. Runtime witnesses (``is_multiclass``, ``is_splittable``, ``is_nonempty``, ``balanced``) refine their Bool return type so they can discharge the corresponding precondition inside an ``if ... then ... else ...`` guard. ─── Opaque types ───────────────────────────────────────────────────────