Hesper.Data.DataFrame — minimal CSV-backed data analysis primitives

This module is the Option A MVP for tutorial Ch11: just enough of a DataFrame API to port the Sabela CaliforniaHousing example to Lean.

Scope (intentionally small):

• Schema-on-read CSV loading with Float / String / Option Float.
• Row-level selection (take, randomSplit).
• Column-level projection (select, exclude, columnNames, dimensions).
• Missing-value imputation (impute).
• Derived columns (derive, deriveMany) computed from scalars per row.
• Min-max normalisation across all numeric columns (normalizeFeatures).
• Markdown pretty-printer for Jupyter (toMarkdown).
• GPU upload (toTensor) producing a Float32Array ready for matmul.

Out of scope (Option B will add it on top):

• Typed column references via Lean macros.
• Column algebra (+ - * / lifted to columns).
• GroupBy / Join / Arrow interop.

The API is shaped after DataHaskell's dataframe (the library Sabela wraps), so users coming from that world should find it familiar. Naming choices follow Sabela where they map cleanly to Lean.

Acknowledgements

The data-analysis surface (column-oriented design, impute / derive / randomSplit / normalizeFeatures helpers, min-max normalisation choice, walk-through structure of the California Housing example) follows DataHaskell's dataframe and Sabela's port to Hasktorch. Implementation is fresh Lean 4 code; semantics, normalisation policy and the example layout are adapted from those projects. Thanks to their authors.

inductive Hesper.Data.Value : Type

A cell in a DataFrame. missing represents NA / NaN.

• f64 : Float → Value
• text : String → Value
• missing : Value

def Hesper.Data.instInhabitedValue.default : Value

Equations

• Hesper.Data.instInhabitedValue.default = Hesper.Data.Value.f64 default

instance Hesper.Data.instInhabitedValue : Inhabited Value

Equations

• Hesper.Data.instInhabitedValue = { default := Hesper.Data.instInhabitedValue.default }

def Hesper.Data.instReprValue.repr : Value → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Hesper.Data.instReprValue.repr Hesper.Data.Value.missing prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hesper.Data.Value.missing")).group prec✝

instance Hesper.Data.instReprValue : Repr Value

Equations

• Hesper.Data.instReprValue = { reprPrec := Hesper.Data.instReprValue.repr }

def Hesper.Data.Value.toFloat? : Value → Option Float

Project to Float?. text is treated as missing.

Equations

• (Hesper.Data.Value.f64 x_1).toFloat? = some x_1
• x✝.toFloat? = none

def Hesper.Data.Value.toString? : Value → Option String

Project to String?. Numerics are stringified.

Equations

• (Hesper.Data.Value.text s).toString? = some s
• (Hesper.Data.Value.f64 x_1).toString? = some (toString x_1)
• Hesper.Data.Value.missing.toString? = none

def Hesper.Data.Value.render : Value → String

Pretty-print for toMarkdown.

Equations

• (Hesper.Data.Value.f64 a).render = toString a
• (Hesper.Data.Value.text a).render = a
• Hesper.Data.Value.missing.render = "?"

inductive Hesper.Data.ColumnType : Type

Inferred column type. optF64 means the column contains at least one NA — used to format header cells like the Haskell Maybe Double.

• f64 : ColumnType
• optF64 : ColumnType
• text : ColumnType

def Hesper.Data.instInhabitedColumnType.default : ColumnType

Equations

• Hesper.Data.instInhabitedColumnType.default = Hesper.Data.ColumnType.f64

instance Hesper.Data.instInhabitedColumnType : Inhabited ColumnType

Equations

• Hesper.Data.instInhabitedColumnType = { default := Hesper.Data.instInhabitedColumnType.default }

instance Hesper.Data.instReprColumnType : Repr ColumnType

Equations

• Hesper.Data.instReprColumnType = { reprPrec := Hesper.Data.instReprColumnType.repr }

def Hesper.Data.instReprColumnType.repr : ColumnType → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Hesper.Data.instBEqColumnType.beq : ColumnType → ColumnType → Bool

Equations

• Hesper.Data.instBEqColumnType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Hesper.Data.instBEqColumnType : BEq ColumnType

Equations

• Hesper.Data.instBEqColumnType = { beq := Hesper.Data.instBEqColumnType.beq }

def Hesper.Data.ColumnType.isNumeric : ColumnType → Bool

Equations

• Hesper.Data.ColumnType.f64.isNumeric = true
• Hesper.Data.ColumnType.optF64.isNumeric = true
• Hesper.Data.ColumnType.text.isNumeric = false

def Hesper.Data.ColumnType.label : ColumnType → String

Equations

• Hesper.Data.ColumnType.f64.label = "Float"
• Hesper.Data.ColumnType.optF64.label = "Float?"
• Hesper.Data.ColumnType.text.label = "String"

structure Hesper.Data.DataFrame : Type

A row-oriented data frame. All rows have the same length as columns; cell (row, col) is rows[row]![col]!.

The row-oriented layout makes derive and impute cheap to express (one closure per row) at the cost of a strided access pattern for column reductions. At the scale Ch11 needs (≤ 20k rows × 11 cols) this is irrelevant; a column-oriented redesign is left for Option B.

• columns : Array String
• schema : Array ColumnType
• rows : Array (Array Value)

instance Hesper.Data.instInhabitedDataFrame : Inhabited DataFrame

Equations

• Hesper.Data.instInhabitedDataFrame = { default := Hesper.Data.instInhabitedDataFrame.default }

def Hesper.Data.instInhabitedDataFrame.default : DataFrame

Equations

• Hesper.Data.instInhabitedDataFrame.default = { columns := default, schema := default, rows := default }

def Hesper.Data.DataFrame.dimensions (df : DataFrame) : Nat × Nat

(numRows, numCols). Matches D.dimensions in Sabela.

Equations

• df.dimensions = (df.rows.size, df.columns.size)

def Hesper.Data.DataFrame.columnNames (df : DataFrame) : Array String

Equations

• df.columnNames = df.columns

def Hesper.Data.DataFrame.colIndex? (df : DataFrame) (name : String) : Option Nat

Look up a column index by name. none if absent.

Equations

• df.colIndex? name = Array.findIdx? (fun (x : String) => x == name) df.columns

def Hesper.Data.DataFrame.colIndex! (df : DataFrame) (name : String) : Nat

Equations

• One or more equations did not get rendered due to their size.

def Hesper.Data.DataFrame.column (df : DataFrame) (name : String) : Array Value

Project to a single column as Array Value.

Equations

• df.column name = Array.map (fun (x : Array Hesper.Data.Value) => x[df.colIndex! name]!) df.rows

def Hesper.Data.DataFrame.numericColumn (df : DataFrame) (name : String) : Array Float

All Float values in a column, skipping NAs / non-numeric.

Equations

• df.numericColumn name = Array.filterMap Hesper.Data.Value.toFloat? (df.column name)

def Hesper.Data.DataFrame.take (n : Nat) (df : DataFrame) : DataFrame

The first n rows. Like D.take.

Equations

• Hesper.Data.DataFrame.take n df = { columns := df.columns, schema := df.schema, rows := df.rows.extract 0 (min n df.rows.size) }

def Hesper.Data.DataFrame.select (cols : Array String) (df : DataFrame) : DataFrame

Keep only the named columns, in the given order.

Equations

• One or more equations did not get rendered due to their size.

def Hesper.Data.DataFrame.exclude (cols : Array String) (df : DataFrame) : DataFrame

Drop the named columns.

Equations

• Hesper.Data.DataFrame.exclude cols df = Hesper.Data.DataFrame.select (Array.filter (fun (x : String) => !cols.contains x) df.columns) df

def Hesper.Data.DataFrame.impute (colName : String) (value : Float) (df : DataFrame) : DataFrame

Replace every missing in colName with value. The column type is promoted from optF64 to f64.

Equations

• One or more equations did not get rendered due to their size.

def Hesper.Data.DataFrame.meanMaybe (colName : String) (df : DataFrame) : Float

Mean of a numeric column, ignoring NAs. Returns 0 if there are no non-NA cells (so it's safe to call before impute).

Equations

• One or more equations did not get rendered due to their size.

def Hesper.Data.DataFrame.minColumn (colName : String) (df : DataFrame) : Float

Minimum of a numeric column, ignoring NAs.

Equations

• One or more equations did not get rendered due to their size.

def Hesper.Data.DataFrame.maxColumn (colName : String) (df : DataFrame) : Float

Maximum of a numeric column, ignoring NAs.

Equations

• One or more equations did not get rendered due to their size.

def Hesper.Data.DataFrame.derive (newCol : String) (f : Array Value → Value) (df : DataFrame) : DataFrame

Append a new column computed from each row. The whole Array Value is passed to the closure so it can reference any other column by index/name. The new column's type is inferred from the first non-missing cell.

Equations

• One or more equations did not get rendered due to their size.

def Hesper.Data.DataFrame.deriveMany (specs : Array (String × (Array Value → Value))) (df : DataFrame) : DataFrame

derive several columns in sequence. Each subsequent closure sees the columns added by earlier closures.

Equations

• One or more equations did not get rendered due to their size.

def Hesper.Data.DataFrame.deriveFloat (newCol : String) (deps : Array String) (f : Array Float → Float) (df : DataFrame) : DataFrame

Helper: derive a Float column from a function on the named columns of each row. Looks up the name once.

Equations

• One or more equations did not get rendered due to their size.

def Hesper.Data.DataFrame.normalizeFeatures (df : DataFrame) : DataFrame

Min-max normalise every numeric column into [0, 1]. Constant columns (max == min) are left at 0. Mirrors Sabela's normalizeFeatures helper.

Equations

• One or more equations did not get rendered due to their size.

Random split

def Hesper.Data.DataFrame.randomSplit (seed : UInt64) (frac : Float) (df : DataFrame) : DataFrame × DataFrame

Split into (train, test) with frac of rows going to train. Order is randomised with seed for reproducibility, matching Sabela's D.randomSplit (mkStdGen seed) frac.

Equations

• One or more equations did not get rendered due to their size.

Pretty-printing

def Hesper.Data.DataFrame.toMarkdown (df : DataFrame) : String

GFM-style markdown table with header type annotations like Sabela's total_rooms<br>Double. Suitable for displayMarkdown in a Jupyter cell.

Equations

• One or more equations did not get rendered due to their size.

def Hesper.Data.DataFrame.toMarkdownHead (n : Nat) (df : DataFrame) : String

Like toMarkdown but caps the row count. Handy in cells where a 20k-row dump would overwhelm Jupyter.

Equations

• Hesper.Data.DataFrame.toMarkdownHead n df = (Hesper.Data.DataFrame.take n df).toMarkdown

def Hesper.Data.DataFrame.toHtml (df : DataFrame) : String

HTML table renderer. Use this with xeus-lean's #html command to get a real <table> (markdown round-trip via IO.println only yields raw text in #eval cells). Column headers include the inferred type, matching toMarkdown.

Equations

• One or more equations did not get rendered due to their size.

def Hesper.Data.DataFrame.toHtmlHead (n : Nat) (df : DataFrame) : String

Like toHtml but caps the row count.

Equations

• Hesper.Data.DataFrame.toHtmlHead n df = (Hesper.Data.DataFrame.take n df).toHtml

CSV loader (minimal)

Local float parser

`Hesper.Training.ParseFloat.parseFloat` works on older Lean — its
`String.Pos.mk ⟨...⟩` and `String.trim` usages don't survive the
4.28 API churn.  Re-implement a small parser inline that handles
California-Housing-style decimals + scientific notation. 

def Hesper.Data.DataFrame.readCsv (path : System.FilePath) : IO DataFrame

Read a CSV file with a header row. Type inference: a column is text if any non-empty cell fails to parse as Float, optF64 if all non-empty cells are floats but at least one cell is missing, f64 otherwise. Lines are split on \n (also handles \r\n).

Equations

• One or more equations did not get rendered due to their size.

Tensor export

def Hesper.Data.DataFrame.toTensor (df : DataFrame) : Array Float × Nat × Nat

Flatten the numeric columns of df into a row-major Float32Array suitable for upload as a feature matrix. Non-numeric and missing cells are encoded as 0.0 — call impute first to control that behaviour. The returned shape is (numRows, numNumericCols).

Equations

• One or more equations did not get rendered due to their size.