Chapter 01 — Lean 4 for ML Engineers

You don't need to be a Lean expert to use Hesper. This chapter teaches just enough to read the rest of the tutorial. If you've used Haskell, OCaml, or even just Python with type hints, most of it will feel familiar — Lean is a strict, ML-style functional language with a dependent type system on top.

Types and definitions

In [ ]:
def square (x : Float) : Float := x * x

#eval square 3.14                 -- 9.8596
#check @square                    -- @square : Float → Float

def name (args) : ReturnType := body. Type annotations on arguments and return type are usually optional — Lean infers them — but in tutorial code we'll write them out for clarity.

The Array, List, and String types

Lean's standard library gives you the usual collections:

In [ ]:
def xs : Array Nat := #[1, 2, 3, 4]
def ys : List Float := [1.0, 2.0, 3.0]

#eval xs.map (· + 1)              -- #[2, 3, 4, 5]
#eval ys.foldl (· + ·) 0.0        -- 6.0

(· + 1) is shorthand for fun x => x + 1. The dot-notation xs.map desugars to Array.map xs.

Structures and product types

In [ ]:
structure Shape where
  rows : Nat
  cols : Nat
deriving Repr

def s : Shape := { rows := 3, cols := 4 }

#eval s.rows * s.cols             -- 12

We'll use small structures a lot — Tensor, Config, Layer, etc.

The IO monad

GPU side-effects and FFI calls live inside IO. You write do-blocks just like Haskell or Rust:

In [ ]:
def hello : IO Unit := do
  IO.println "hello GPU"

#eval hello

← binds the result of an IO action; let x := ... is pure binding. The s!"..." syntax is string interpolation.

Dependent types (the part that's new)

Lean lets a type depend on a value. This is what makes the shader DSL type-safe:

In [ ]:
inductive Kind | f32 | i32 | u32

-- A type that depends on a value of Kind.  We use `abbrev` (not `def`)
-- so that `Carrier .f32` reduces to `Float` transparently — otherwise
-- the elaborator can't see through the alias when it needs to find a
-- `OfNat Float 1` instance below.
abbrev Carrier : Kind → Type
  | .f32 => Float
  | .i32 => Int
  | .u32 => UInt32

def oneOf : (k : Kind) → Carrier k
  | .f32 => 1.0
  | .i32 => 1
  | .u32 => 1

In Hesper, Exp (.scalar .f32) and Exp (.scalar .i32) are different types, so a stray i32 cannot sneak into an f32 shader expression.

Typeclasses

Typeclasses look like Haskell:

In [ ]:
class Approximable (α : Type) where
  approxEq : α → α → Bool

instance : Approximable Float where
  approxEq a b := (a - b).abs < 1e-6

#eval Approximable.approxEq (1.0 : Float) 1.0000001
-- true

Hesper uses typeclasses for GPUBackend (Ch05), Differentiable (Ch03), and for tensor element types.

Module imports

A real Lean file starts with all its imports up top, like Python or Haskell. In the rest of this tutorial each chapter's notebook places its imports in the first code cell:

import Hesper.WGSL.DSL          -- the type-safe shader DSL
import Hesper.Compute           -- high-level compute API
import Hesper.Models.BitNet     -- BitNet inference

What's next