Hale Documentation

Hale ports Haskell’s web ecosystem to Lean 4 with maximalist typing – encoding correctness, invariants, and protocol guarantees directly in the type system.

Mantra: Extensive typing/proving with no compromise on performance.

Architecture Overview

+-----------------------------------------------------------+
|                    User Application                        |
|              (Application : WAI type)                      |
+-----------------------------------------------------------+
|                    Middleware Stack                         |
|    AddHeaders . ForceSSL . Gzip . RequestLogger . ...      |
+-----------------------------------------------------------+
|                    WAI Interface                            |
|  Request -> (Response -> IO Received) -> AppM .pending .sent|
+----------+----------+-----------+-------------------------+
|   Warp   | WarpTLS  | WarpQUIC  |  Static File Server     |
| HTTP/1.x |  HTTPS   |  HTTP/3   |  (wai-app-static)       |
+----------+----------+-----------+-------------------------+
|              Transport Layer                                |
|  Socket(.listening) -> Socket(.connected) -> Connection    |
|     TCP (plain)    |   TLS (OpenSSL)    |  QUIC            |
+-----------------------------------------------------------+
|              Operating System (via FFI)                     |
|         POSIX sockets | OpenSSL | kqueue/epoll             |
+-----------------------------------------------------------+

Leveraging Lean 4’s Dependent Type System

Lean 4 is not Haskell with nicer syntax – it is a full dependently-typed proof assistant that also happens to compile to efficient native code. Hale exploits this to turn protocol specifications, resource lifecycles, and algebraic contracts into compile-time obligations that are verified by the kernel and then erased at runtime (zero cost). Below are the four core techniques.

1. Phantom Type Parameters – Zero-Cost State Machines

A phantom parameter encodes the resource’s lifecycle state in the type. Functions that require a particular state accept only that constructor; transitions return the new state. The parameter is fully erased at runtime (same machine code as an untyped handle), yet the compiler rejects every protocol violation.

structure Socket (state : SocketState) where    -- phantom parameter, erased at runtime
  raw : RawSocket

def bind   (s : Socket .fresh)     : IO (Socket .bound)     -- fresh  --> bound
def listen (s : Socket .bound)     : IO (Socket .listening)  -- bound  --> listening
def accept (s : Socket .listening) : IO (Socket .connected)  -- listen --> connected
def send   (s : Socket .connected) : IO Nat                  -- only connected
def close  (s : Socket state)                                -- any non-closed state
           (h : state ≠ .closed := by decide)                -- PROOF: not already closed
           : IO (Socket .closed)                             -- returns closed token

-- Compile-time errors (no runtime check needed):
-- send freshSocket       -- type error: .fresh ≠ .connected
-- accept boundSocket     -- type error: .bound ≠ .listening
-- close closedSocket     -- type error: cannot prove .closed ≠ .closed

2. Proof-Carrying Structures – Invariants by Construction

Lean 4 erases proof terms at compile time, so proof fields in structures are literally free – same sizeof, same codegen. The invariant is guaranteed the moment the value exists; no runtime validation is ever needed.

structure Ratio where
  num : Int
  den : Nat
  den_pos : den > 0          -- erased: denominator always positive
  coprime : Nat.Coprime num.natAbs den  -- erased: always in lowest terms

structure Settings where
  settingsTimeout : Nat := 30
  settingsTimeoutPos : settingsTimeout > 0 := by omega  -- erased: never zero

3. Indexed Monads – Exactly-Once Protocol Enforcement

Where Haskell’s WAI relies on a gentleman’s agreement (“call respond exactly once”), Lean 4 enforces it at the type level via an indexed monad whose pre/post state parameters track the response lifecycle. The constructor is private, so the only way to produce AppM .pending .sent ResponseReceived is through the provided combinators – fabrication is a type error.

structure AppM (pre post : ResponseState) (α : Type) where
  private mk ::          -- can't fabricate: constructor is private
  run : IO α

def AppM.respond         -- the ONLY transition from .pending to .sent
  (callback : Response → IO ResponseReceived)
  (resp : Response)
  : AppM .pending .sent ResponseReceived

-- Double-respond is a compile-time error:
-- After the first respond, state is .sent.
-- A second respond would need AppM .sent .sent, which does not exist.

4. Inductive Types – Protocol Semantics as Data

Sum types encode every valid protocol state or message shape. Pattern matching is exhaustive, so the compiler verifies that every case is handled.

inductive Response where
  | responseFile    ...   -- sendfile(2)
  | responseBuilder ...   -- in-memory ByteArray
  | responseStream  ...   -- chunked streaming
  | responseRaw     ...   -- raw socket (WebSocket upgrade)

inductive RequestBodyLength where
  | chunkedBody           -- Transfer-Encoding: chunked
  | knownLength (n : Nat) -- Content-Length: n

Design Principle: Proofs on Objects, Not Wrapper Types

Invariants belong inside the original type, not in a separate wrapper. Proof fields are zero-cost (erased), so there is never a reason to create ValidSettings alongside Settings – just put the proof in Settings.

Package Index

Links marked API point to the auto-generated doc-gen4 API reference. Links marked Guide point to hand-written documentation.

Core Infrastructure

Web Application Interface

Protocol Implementations

Utilities

Proven Properties (257 theorems)

See Proofs.md for a complete catalog of all theorems.

Hale.Base — Haskell base for Lean 4

API Reference: Hale.Base

Re-exports all Base sub-modules.

Design Philosophy (Concurrency)

All concurrency primitives are promise-based, not OS-thread-based. Blocking operations return BaseIO (Task a) rather than suspending an OS thread. This enables scaling to millions of concurrent “threads” on Lean’s task-pool scheduler.

Cancellation is cooperative: killThread sets a CancellationToken rather than throwing an asynchronous exception. CPU-bound threads that never check the token will not be interrupted.

Foundational

• Void — Data.Void
• Function — Data.Function
• Newtype — Data.Monoid / Data.Semigroup

Core Abstractions

• Bifunctor — Data.Bifunctor
• Contravariant — Data.Functor.Contravariant
• Const — Data.Functor.Const
• Identity — Data.Functor.Identity
• Compose — Data.Functor.Compose
• Category — Control.Category

Data Structures

• NonEmpty — Data.List.NonEmpty
• Either — Data.Either
• Ord — Data.Ord
• Tuple — Data.Tuple + Prelude

Traversals

• Foldable — Data.Foldable
• Traversable — Data.Traversable

Numeric Types

• Ratio — Data.Ratio
• Complex — Data.Complex
• Fixed — Data.Fixed

Advanced Abstractions

• Arrow — Control.Arrow

Concurrency

• Concurrent — Control.Concurrent
• MVar — Control.Concurrent.MVar
• Chan — Control.Concurrent.Chan
• QSem — Control.Concurrent.QSem
• QSemN — Control.Concurrent.QSemN

Void

Lean: Hale.Base.Void | Haskell: Data.Void

Overview

Uninhabited type (alias for Empty). Provides absurd for ex falso reasoning.

API Mapping

Instances

• BEq Void
• Ord Void
• ToString Void
• Repr Void
• Hashable Void
• Inhabited (Void -> a) — functions from Void are always inhabited

Proofs & Guarantees

• eq_absurd — uniqueness of void functions: any two functions from Void are equal

Example

-- A function from Void to any type is unique
def fromVoid : Void -> Nat := Void.absurd

Function

Lean: Hale.Base.Function | Haskell: Data.Function

Overview

Standard function combinators: on, applyTo (&), const (K combinator), flip (C combinator).

API Mapping

Instances

None (standalone functions).

Proofs & Guarantees

• on_apply — (f.on g) x y = f (g x) (g y)
• applyTo_apply — x.applyTo f = f x
• const_apply — Function.const a b = a
• flip_flip — flip (flip f) = f (involution)
• flip_apply — Function.flip f x y = f y x

Example

-- Compare strings by length
Function.on (· + ·) String.length "hi" "hello"
-- => 7

Newtype

Lean: Hale.Base.Newtype | Haskell: Data.Monoid / Data.Semigroup

Overview

Monoid/semigroup wrappers: Dual, Endo, First, Last, Sum, Product, All, Any. Each wraps a value and provides an Append instance with specific combining semantics.

API Mapping

Instances

All wrappers provide Append.

Proofs & Guarantees

• append_assoc — associativity of Append for each wrapper

Example

-- Sum combines via addition
Sum.mk 3 ++ Sum.mk 4
-- => Sum 7

Bifunctor

Lean: Hale.Base.Bifunctor | Haskell: Data.Bifunctor

Overview

Typeclass for types with two covariant type parameters. Provides bimap, mapFst, mapSnd.

API Mapping

Instances

• Bifunctor Prod
• Bifunctor Sum
• Bifunctor Except
• LawfulBifunctor Prod
• LawfulBifunctor Sum
• LawfulBifunctor Except

Proofs & Guarantees

• bimap_id — bimap id id = id (via LawfulBifunctor)
• bimap_comp — bimap (f1 . f2) (g1 . g2) = bimap f1 g1 . bimap f2 g2 (via LawfulBifunctor)

Example

-- Map over both components of a pair
Bifunctor.bimap (· * 10) (· ++ "!") (1, "hello")
-- => (10, "hello!")

Contravariant

Lean: Hale.Base.Contravariant | Haskell: Data.Functor.Contravariant

Overview

Contravariant functors — types that consume values rather than produce them. Where a covariant functor maps over outputs, a contravariant functor maps over inputs.

API Mapping

Instances

• Contravariant Predicate
• Contravariant Equivalence
• LawfulContravariant Predicate
• LawfulContravariant Equivalence

Proofs & Guarantees

• contramap_id — contramap id = id (via LawfulContravariant)
• contramap_comp — contramap (f . g) = contramap g . contramap f (via LawfulContravariant)

Example

-- Adapt a predicate on Nat to work on String via length
Contravariant.contramap String.length (Predicate.mk (· > 3))
-- Now accepts strings with length > 3

Const

Lean: Hale.Base.Const | Haskell: Data.Functor.Const

Overview

Constant functor — ignores its second type parameter. Useful for phantom types and accumulating effects during traversals.

API Mapping

Instances

• BEq (Const a b) (requires BEq a)
• Ord (Const a b) (requires Ord a)
• Repr (Const a b) (requires Repr a)
• ToString (Const a b) (requires ToString a)
• Functor (Const a)
• Pure (Const a) (requires Append a and Inhabited a)

Proofs & Guarantees

• map_val — mapping over Const preserves the wrapped value
• map_id — Functor.map id = id
• map_comp — Functor.map (f . g) = Functor.map f . Functor.map g

Example

-- Mapping over Const does nothing to the stored value
(Functor.map f (Const.mk 42) : Const Nat String).getConst == 42
-- => true

Identity

Lean: Hale.Base.Identity | Haskell: Data.Functor.Identity

Overview

Identity functor/monad — trivial wrapper. Useful as a base case for monad transformer stacks and as a witness that a computation is pure.

API Mapping

Instances

• Functor Identity
• Pure Identity
• Bind Identity
• Seq Identity
• Applicative Identity
• Monad Identity
• BEq (Identity a) (derived)
• Ord (Identity a) (derived)
• Repr (Identity a) (derived)
• Hashable (Identity a) (derived)
• Inhabited (Identity a) (derived)
• ToString (Identity a)

Proofs & Guarantees

• map_id — Functor.map id = id
• map_comp — Functor.map (f . g) = Functor.map f . Functor.map g
• pure_bind — left identity: pure a >>= f = f a
• bind_pure — right identity: m >>= pure = m
• bind_assoc — associativity: (m >>= f) >>= g = m >>= (fun x => f x >>= g)

Example

-- Identity monad is just a trivial wrapper
(Identity.mk 42 >>= fun n => Identity.mk (n + 1)).runIdentity
-- => 43

Compose

Lean: Hale.Base.Compose | Haskell: Data.Functor.Compose

Overview

Composition of functors/applicatives. Compose F G a wraps F (G a), allowing two functors to be composed into a single functor (or two applicatives into a single applicative).

API Mapping

Instances

• Functor (Compose F G) (requires Functor F, Functor G)
• Pure (Compose F G) (requires Applicative F, Applicative G)
• Seq (Compose F G) (requires Applicative F, Applicative G)
• Applicative (Compose F G) (requires Applicative F, Applicative G)

Proofs & Guarantees

• map_id — Functor.map id = id (with lawful functors)
• map_comp — Functor.map (f . g) = Functor.map f . Functor.map g (with lawful functors)

Example

-- Compose List and Option into a single functor
Compose.mk [some 1, none, some 3]
-- : Compose List Option Nat

Category

Lean: Hale.Base.Category | Haskell: Control.Category

Overview

Abstract category with identity and composition. Uses diagrammatic order (f >>> g = g . f), which reads left-to-right as a pipeline.

API Mapping

Instances

• Category Fun — the function arrow as a category
• LawfulCategory Fun — all three laws hold definitionally

Proofs & Guarantees

• id_comp — id >>> f = f (via LawfulCategory)
• comp_id — f >>> id = f (via LawfulCategory)
• comp_assoc — (f >>> g) >>> h = f >>> (g >>> h) (via LawfulCategory)

Example

-- Compose functions in diagrammatic (left-to-right) order
(Fun.mk (· + 1) >>> Fun.mk (· * 2)).apply 3
-- => 8  (first add 1, then multiply by 2)

NonEmpty

Lean: Hale.Base.NonEmpty | Haskell: Data.List.NonEmpty

Overview

Non-empty list with a guaranteed minimum of one element. The length function returns a subtype {n : Nat // n >= 1}, encoding the non-emptiness invariant at the type level.

API Mapping

Instances

• Append (NonEmpty a)
• Functor NonEmpty
• Pure NonEmpty
• Bind NonEmpty
• Monad NonEmpty
• ToString (NonEmpty a) (requires ToString a)
• BEq (NonEmpty a) (derived)
• Ord (NonEmpty a) (derived)
• Repr (NonEmpty a) (derived)
• Hashable (NonEmpty a) (derived)

Proofs & Guarantees

• toList_ne_nil — toList ne != [] (the list is never empty)
• reverse_length — reversing preserves length
• toList_length — toList length agrees with NonEmpty.length
• map_length — mapping preserves length

Example

-- Construct a non-empty list
let ne := NonEmpty.mk 1 [2, 3]
ne.head    -- => 1
ne.last    -- => 3
ne.length  -- => ⟨3, by omega⟩

Either

Lean: Hale.Base.Either | Haskell: Data.Either

Overview

Sum type with Left and Right constructors. Right-biased for Functor/Monad instances. Includes partitioning of lists of Either values.

API Mapping

Instances

• Functor (Either a)
• Pure (Either a)
• Bind (Either a)
• Seq (Either a)
• Applicative (Either a)
• Monad (Either a)
• Bifunctor Either
• ToString (Either a b) (requires ToString a, ToString b)

Proofs & Guarantees

• swap_swap — swap (swap e) = e (involution)
• isLeft_not_isRight — isLeft e = !isRight e
• partitionEithers_length — total elements preserved after partitioning

Example

-- Partition a list of Either values
Either.partitionEithers [.left "a", .right 1, .left "b", .right 2]
-- => (["a", "b"], [1, 2])

Ord

Lean: Hale.Base.Ord | Haskell: Data.Ord

Overview

Ordering utilities. Down reverses the comparison order. comparing lifts comparisons through projections. clamp returns a proof-carrying bounded value.

API Mapping

Instances

• BEq (Down a) (requires BEq a)
• Ord (Down a) (requires Ord a, reversed)
• ToString (Down a) (requires ToString a)

Proofs & Guarantees

• get_mk — (Down.mk x).get = x
• compare_reverse — compare (Down.mk a) (Down.mk b) = compare b a

Example

-- Down reverses comparison order
compare (Down.mk 3) (Down.mk 7)
-- => Ordering.gt  (because 3 < 7, but Down reverses it)

Tuple

Lean: Hale.Base.Tuple | Haskell: Data.Tuple + Prelude

Overview

Pair operations: swap, map components, curry/uncurry. Provides bidirectional conversions between curried and uncurried function forms.

API Mapping

Instances

None (standalone functions on Prod).

Proofs & Guarantees

• swap_swap — swap (swap p) = p (involution)
• curry_uncurry — curry (uncurry f) = f
• uncurry_curry — uncurry (curry f) = f
• bimap_id — bimap id id = id
• bimap_comp — bimap (f1 . f2) (g1 . g2) = bimap f1 g1 . bimap f2 g2
• mapFst_eq_bimap — mapFst f = bimap f id
• mapSnd_eq_bimap — mapSnd f = bimap id f

Example

-- Curry converts a function on pairs to a curried function
Tuple.curry (fun p => p.1 + p.2) 2 3
-- => 5

Foldable

Lean: Hale.Base.Foldable | Haskell: Data.Foldable

Overview

Typeclass for structures that can be folded to a summary value. Provides a rich API with many derived operations built on top of foldr.

API Mapping

Instances

• Foldable List
• Foldable Option
• Foldable List.NonEmpty
• Foldable (Either a)

Proofs & Guarantees

None listed (correctness follows from typeclass laws).

Example

-- Sum all elements in a list
Foldable.sum [1, 2, 3]
-- => 6

Traversable

Lean: Hale.Base.Traversable | Haskell: Data.Traversable

Overview

Typeclass for structures that can be traversed with effects. Extends Functor by allowing each element to produce an applicative effect, then collecting those effects.

API Mapping

Instances

• Traversable List
• Traversable Option
• Traversable NonEmpty

Note: Either α cannot have a Traversable instance due to universe constraints in Lean 4.

Proofs & Guarantees

• traverse_identity — traversing with the identity applicative is just map (via LawfulTraversable)

Example

-- Sequence a list of Options: all must be Some to get Some
Traversable.sequence [some 1, some 2, some 3]
-- => some [1, 2, 3]

Traversable.sequence [some 1, none, some 3]
-- => none

Ratio

Lean: Hale.Base.Ratio | Haskell: Data.Ratio

Overview

Exact rational arithmetic. Invariants are enforced in the type: the denominator is always positive and the numerator and denominator are always coprime.

API Mapping

Instances

• OfNat Ratio 0 / OfNat Ratio 1
• Inhabited Ratio
• LE Ratio / LT Ratio
• BEq Ratio
• Ord Ratio
• Add Ratio / Sub Ratio / Mul Ratio / Neg Ratio
• ToString Ratio

Proofs & Guarantees

Invariants maintained by construction via the den_pos and coprime fields in the Ratio structure:

• Denominator is always positive
• Numerator and denominator are always coprime

Example

-- Exact rational arithmetic: 1/2 + 1/3 = 5/6
Ratio.mk' 1 2 (by omega) + Ratio.mk' 1 3 (by omega)
-- => 5/6

Complex

Lean: Hale.Base.Complex | Haskell: Data.Complex

Overview

Complex numbers parameterized by coefficient type. Supports arithmetic operations and conjugation.

API Mapping

Instances

• Inhabited (Complex a) (requires Inhabited a)
• ToString (Complex a) (requires ToString a)
• Add (Complex a) (requires Add a)
• Neg (Complex a) (requires Neg a)
• Sub (Complex a) (requires Sub a)
• Mul (Complex a) (requires Add a, Sub a, Mul a)
• BEq (Complex a) (derived)
• Ord (Complex a) (derived)
• Repr (Complex a) (derived)
• Hashable (Complex a) (derived)

Proofs & Guarantees

• conjugate_conjugate — conjugate (conjugate z) = z (involution)
• add_comm' — z1 + z2 = z2 + z1

Example

-- Compute magnitude squared of 3 + 4i
Complex.magnitudeSquared ⟨3, 4⟩
-- => 25  (since 3^2 + 4^2 = 25)

Fixed

Lean: Hale.Base.Fixed | Haskell: Data.Fixed

Overview

Fixed-point decimal arithmetic. Fixed p stores integers scaled by 10^p. Addition and subtraction are exact (no rounding).

API Mapping

Instances

• Add (Fixed p) / Sub (Fixed p) / Neg (Fixed p) / Mul (Fixed p)
• OfNat (Fixed p) 0 / OfNat (Fixed p) 1
• Inhabited (Fixed p)
• ToString (Fixed p)
• BEq (Fixed p) (derived)
• Ord (Fixed p) (derived)
• Repr (Fixed p) (derived)
• Hashable (Fixed p) (derived)

Proofs & Guarantees

• scale_pos — the scale factor 10^p is always positive
• add_exact — addition of fixed-point values is exact (no rounding)
• sub_exact — subtraction of fixed-point values is exact (no rounding)

Example

-- Fixed-point with 2 decimal places: 3.00 + 1.57 = 4.57
Fixed.fromInt (p := 2) 3 + ⟨157⟩
-- => 4.57  (internally stored as raw 457)

Arrow

Lean: Hale.Base.Arrow | Haskell: Control.Arrow

Overview

Arrow abstraction for generalized function-like computations. Extends Category with lifting and product/sum operations.

API Mapping

Instances

• Arrow Fun
• ArrowChoice Fun

Proofs & Guarantees

None listed (laws follow from LawfulCategory and the arrow laws).

Example

-- Lift a pure function into the Arrow
(Arrow.arr (Cat := Fun) (· * 2)).apply 3
-- => 6

Concurrent

Lean: Hale.Control.Concurrent | Haskell: Control.Concurrent

Overview

Thread management primitives: forking lightweight threads, cooperative cancellation, delays, and yielding. Threads run on Lean’s task pool via IO.asTask, not as 1:1 OS threads.

API Mapping

Differences from GHC

Instances

• BEq ThreadId — equality by id field
• Hashable ThreadId — hash of id field
• ToString ThreadId — "ThreadId(n)"
• Repr ThreadId — "ThreadId(n)"

ThreadId Structure

structure ThreadId where
  private mk ::
  id : PosNat                           -- unique, monotonic, >= 1
  private task : Task (Except IO.Error Unit)
  private cancelToken : Std.CancellationToken

Fields task and cancelToken are private; the only public field is id.

Proofs & Guarantees

• Unique IDs by construction: freshThreadId reads and increments a global monotonic counter. Within a single process, no two ThreadId values share the same id.
• forkFinally finaliser guarantee: The finally_ callback runs in both the success and error branches of a try/catch, so it executes regardless of outcome.
• Cooperative cancellation only: killThread sets a CancellationToken; it does not forcibly terminate the thread. A thread that never checks the token will continue running.

Example

import Hale.Control.Concurrent

open Hale

-- Fork a thread that prints a message
let tid <- forkIO do
  IO.println "hello from thread"

-- Fork with a finaliser
let tid2 <- forkFinally (do IO.println "working..."; pure 42) fun
  | .ok val   => IO.println s!"done: {val}"
  | .error e  => IO.println s!"failed: {e}"

-- Cooperative cancellation
killThread tid

-- Delay for 1 second (1_000_000 microseconds)
threadDelay 1000000

-- Yield to other threads
yield

-- Wait for a thread to complete
waitThread tid2

Performance Notes

• forkIO is lightweight: it schedules a task on the thread pool, not an OS thread.
• threadDelay has millisecond granularity due to IO.sleep. A request for 1 microsecond will sleep for 1 millisecond.
• yield is equivalent to IO.sleep 0, giving other tasks a chance to run.

MVar

Lean: Hale.Control.Concurrent.MVar | Haskell: Control.Concurrent.MVar

Overview

A synchronisation variable that is either empty or holds a value of type a. All blocking is promise-based: waiting tasks are dormant IO.Promise values, not blocked OS threads. This allows scaling to millions of concurrent tasks.

MVar is the fundamental building block for all other concurrency primitives in hale (Chan, QSem, QSemN).

Concurrent Type Alias

abbrev Concurrent (a : Type) := BaseIO (Task a)

Any function returning Concurrent a is non-blocking by construction. Compose with BaseIO.bindTask:

let task <- mv.take        -- Concurrent a = BaseIO (Task a)
BaseIO.bindTask task fun val => ...

API Mapping

Constraint: [Nonempty a]

Blocking operations (take, read, swap, withMVar, modify, modify_) require [Nonempty a] for IO.Promise construction. Non-blocking try* operations do not require this constraint.

Proofs & Guarantees

Structural Invariant

Maintained by all operations:

• If value.isSome, then takers is empty (no one waits when a value exists).
• If value.isNone, then putters is empty (no one waits to put when empty).

FIFO Fairness

Waiters are queued in Std.Queue and dequeued in insertion order. Both takers and putters are served FIFO.

No Lost Wakeups

• Every put on an empty MVar with a taker wakes exactly one taker.
• Every take on a full MVar with a putter wakes exactly one putter.
• Proof by case analysis on the match branches in take/put.

Axiom-Dependent Properties (documented, not machine-checked)

• Linearizability – depends on Std.Mutex providing mutual exclusion.
• Starvation-freedom – depends on Lean’s task scheduler being eventually fair and on complementary operations eventually occurring.
• Progress – follows from no-lost-wakeups + mutex correctness.

Example

import Hale.Control.Concurrent.MVar

open Hale

-- Create an MVar with an initial value
let mv <- MVar.new 42

-- Non-blocking try operations
let val <- mv.tryRead    -- some 42
let ok  <- mv.tryPut 99  -- false (MVar is full)

-- Async take (returns a Task)
let task <- mv.take
let val  <- IO.wait task  -- 42 (MVar is now empty)

-- Async put
let task <- mv.put 100
IO.wait task              -- MVar now holds 100

-- Modify with result
let task <- mv.modify fun x => pure (x + 1, x)
let old  <- IO.wait task  -- 100 (MVar now holds 101)

-- Sync wrappers (block OS thread -- prefer async versions)
let v <- mv.takeSync      -- 101
mv.putSync 200

Performance Notes

• Promise-based blocking: Waiters are dormant promises, not spinning or sleeping OS threads. A million waiting tasks consume memory for the promise objects but no OS thread resources.
• Mutex contention: All operations go through Std.Mutex.atomically. Under extreme contention, this is the bottleneck.
• Sync wrappers (takeSync, putSync, readSync) block an OS thread via IO.wait. Use them only at top-level or in non-scalable contexts; prefer the async versions for concurrent code.
• isEmpty is a snapshot: The result may be stale by the time you act on it. Do not use it for synchronisation.

Chan

Lean: Hale.Control.Concurrent.Chan | Haskell: Control.Concurrent.Chan

Overview

An unbounded FIFO channel with subscriber-based duplication. Internally uses a Std.Queue buffer protected by a Std.Mutex, with a queue of reader promises for when the buffer is empty. A shared write-side mutex holds the subscriber list, enabling dup.

All blocking uses promises: read returns BaseIO (Task a), never blocking an OS thread.

API Mapping

Constraint: [Nonempty a]

Chan.read requires [Nonempty a] for IO.Promise construction. Chan.tryRead and Chan.write do not require this constraint.

Subscriber-Based Dup Design

Unlike Haskell’s linked-list-of-MVars implementation, hale uses a subscriber array:

• Each Chan has a private readState (per-reader buffer + waiters) and a shared writeState (subscriber list).
• write delivers the value to all current subscribers.
• dup creates a new readState and registers it in the shared subscriber list. The new channel shares the write side but reads independently.
• Values written before dup that have not been read are not visible on the new channel (matching Haskell’s dupChan semantics).

Proofs & Guarantees

Structural Invariant

Maintained by write/read:

buffer.isEmpty = false  =>  waiters.isEmpty = true

If there are buffered values, no reader should be waiting. Enforced by read consuming from the buffer first, and write resolving a waiter before buffering.

FIFO Ordering

Values are read in the order they were written, guaranteed by Std.Queue.

Write Fan-Out

A single write delivers to all current subscribers atomically (the subscriber list is read under the write-side mutex).

Example

import Hale.Control.Concurrent.Chan

open Hale

-- Create a channel
let ch <- Chan.new Nat

-- Write values
ch.write 1
ch.write 2
ch.write 3

-- Read (async, returns Task)
let task <- ch.read
let val  <- IO.wait task  -- 1

-- Non-blocking read
let maybe <- ch.tryRead   -- some 2

-- Duplicate: new reader sees future writes only
let ch2 <- ch.dup
ch.write 10
let t1 <- ch.read
let t2 <- ch2.read
let v1 <- IO.wait t1  -- 3 (buffered before dup, still in ch's buffer)
                       -- actually 3 was already buffered, 10 goes after
let v2 <- IO.wait t2  -- 10 (ch2 only sees writes after dup)

Performance Notes

• Unbounded buffer: There is no backpressure. A fast writer with a slow reader will accumulate values in the Std.Queue buffer without bound.
• Write cost is O(subscribers): Each write iterates over all subscribers. For a single-reader channel this is O(1); for many dup’d readers it scales linearly.
• Reader contention: Each reader has its own Std.Mutex-protected state, so multiple readers do not contend with each other. Writers contend briefly on the shared write-side mutex to read the subscriber list.
• Promise-based blocking: A read on an empty channel creates a dormant promise – no OS thread is consumed while waiting.

QSem

Lean: Hale.Control.Concurrent.QSem | Haskell: Control.Concurrent.QSem

Overview

A simple quantity semaphore: at most n resources can be acquired concurrently. All blocking is promise-based. Waiters are served in FIFO order.

API Mapping

Proofs & Guarantees

Non-Negative Count

The count is Nat by construction – it cannot underflow below zero.

Structural Invariant

count > 0  =>  waiters = empty

If resources are available, no one should be waiting. Maintained by signal: it wakes a waiter before incrementing the count.

FIFO Fairness

Waiters are queued in Std.Queue and dequeued in insertion order.

No Lost Wakeups

signal either wakes exactly one waiter or increments the count. Both branches are mutually exclusive (case split on waiters.dequeue?).

Exception Safety

withSem uses try/finally to ensure signal is called even if the action throws.

Example

import Hale.Control.Concurrent.QSem

open Hale

-- Create a semaphore allowing 3 concurrent accesses
let sem <- QSem.new 3

-- Acquire one unit (async, non-blocking by type)
let task <- sem.wait
IO.wait task

-- Release one unit
sem.signal

-- Bracket pattern: acquire, run, release
let result <- sem.withSem do
  -- at most 3 threads run this section concurrently
  pure 42

Performance Notes

• Promise-based blocking: A wait on an exhausted semaphore creates a dormant promise. No OS thread is consumed while waiting.
• withSem blocks an OS thread via IO.wait for the initial acquire. For fully non-blocking usage, call wait directly and chain with BaseIO.bindTask.
• Mutex contention: Both wait and signal go through Std.Mutex.atomically. Under high contention this is the bottleneck.
• Single-unit granularity: For multi-unit acquire/release, use QSemN instead.

QSemN

Lean: Hale.Control.Concurrent.QSemN | Haskell: Control.Concurrent.QSemN

Overview

A generalised quantity semaphore that allows acquiring and releasing arbitrary amounts of a resource. Like QSem, but wait and signal take a Nat parameter for the number of units.

API Mapping

Proofs & Guarantees

Non-Negative Count

The count is Nat by construction – it cannot underflow below zero.

Structural Invariant

count >= n  =>  no waiter requesting <= n is queued

When signal adds resources, it greedily wakes FIFO-ordered waiters whose requested amount can be satisfied.

Greedy FIFO Wakeup

signal calls wakeWaiters, which iterates from the front of the queue and wakes each waiter whose needed amount is less than or equal to the current count. It stops at the first waiter that cannot be satisfied (head-of-line blocking, matching Haskell semantics).

No Lost Wakeups

signal always either wakes one or more waiters or leaves the increased count for future wait calls. The wakeWaiters loop is exhaustive up to the first unsatisfiable request.

Exception Safety

withSemN uses try/finally to ensure signal n is called even if the action throws.

Example

import Hale.Control.Concurrent.QSemN

open Hale

-- Create a semaphore with 100 units (e.g., bytes of bandwidth)
let sem <- QSemN.new 100

-- Acquire 30 units
let task <- sem.wait 30
IO.wait task

-- Release 30 units
sem.signal 30

-- Bracket pattern: acquire n, run, release n
let result <- sem.withSemN 50 do
  -- up to 100 units can be held concurrently
  pure "done"

Greedy Wakeup Detail

When signal n is called, the internal wakeWaiters function runs:

1. Peek at the front waiter (needed, promise).
2. If count >= needed, subtract needed from count, resolve promise, and repeat from step 1.
3. If count < needed, stop. The waiter remains queued (head-of-line blocking).
4. If the queue is empty, stop.

This means a large request at the front of the queue can block smaller requests behind it, even if enough resources are available for the smaller ones. This matches Haskell’s QSemN semantics.

Performance Notes

• Promise-based blocking: A wait on an exhausted semaphore creates a dormant promise. No OS thread is consumed while waiting.
• withSemN blocks an OS thread via IO.wait for the initial acquire. For fully non-blocking usage, call wait directly and chain with BaseIO.bindTask.
• Wakeup cost: signal may wake multiple waiters in a single call (greedy loop), all within a single Std.Mutex.atomically block.
• Head-of-line blocking: A large request at the front of the queue prevents smaller requests behind it from being satisfied. Consider whether this is acceptable for your workload.

ByteString

Lean: Hale.ByteString | Haskell: bytestring (https://hackage.haskell.org/package/bytestring)

API Reference: Hale.ByteString

Overview

Port of Haskell’s bytestring library to Lean 4 with maximalist typing. Provides:

• Strict ByteString (Data.ByteString.ByteString): Slice-based representation with O(1) take/drop/splitAt, bounds proofs in the type
• Short ByteString (Data.ByteString.ShortByteString): Thin newtype over ByteArray for API compatibility
• Lazy ByteString (Data.ByteString.Lazy.LazyByteString): Chunked, Thunk-based lazy evaluation with non-empty chunk invariant
• Builder (Data.ByteString.Builder): Continuation-based O(1) concatenation with proven Monoid laws
• Char8 (Data.ByteString.Char8): Latin-1 character-oriented wrappers

Lean Stdlib Reuse

Uses ByteArray, UInt8, IO.FS.readBinFile/writeBinFile from Lean’s standard library. The port adds the slice representation, lazy chunking, and typed invariants that Lean lacks.

Module Map

Data.ByteString

Lean: Hale.ByteString.Data.ByteString | Haskell: Data.ByteString

Overview

Strict byte strings with O(1) slicing. The core type is a slice into a ByteArray:

structure ByteString where
  data : ByteArray
  off : Nat
  len : Nat
  valid : off + len ≤ data.size

Key API Mapping

Instances

• BEq ByteString – byte-by-byte comparison
• Ord ByteString – lexicographic ordering
• Append ByteString – concatenation (O(m+n))
• ToString ByteString – [w1, w2, ...] format
• Hashable ByteString
• Inhabited ByteString – empty

Proofs

• take_valid / drop_valid – slice operations preserve bounds
• null_iff_length_zero – null <-> length = 0

Performance

Data.ByteString.Char8

Lean: Hale.ByteString.Data.ByteString.Char8 | Haskell: Data.ByteString.Char8

Overview

Character-oriented operations on strict ByteString using the Latin-1 (ISO 8859-1) encoding. Each Char is truncated to its low 8 bits via Char.toUInt8.

This module re-exports the core ByteString type and provides Char-based wrappers around the byte-level API.

Key API Mapping

Design Notes

• Latin-1 only: Characters above U+00FF are truncated. This matches Haskell’s Data.ByteString.Char8 semantics exactly.
• No Unicode support: For UTF-8 encoded byte strings, use a dedicated text library instead.
• Shared representation: Char8 functions operate on the same ByteString type – there is no separate Char8ByteString.

Instances

No additional instances beyond those on ByteString. The Char8 module provides functions, not a new type.

Data.ByteString.Short

Lean: Hale.ByteString.Data.ByteString.Short | Haskell: Data.ByteString.Short

Overview

Short byte strings: a thin newtype over ByteArray providing a ByteString-compatible API without the slice indirection. Useful when you need compact storage and do not benefit from O(1) slicing.

Core Type

structure ShortByteString where
  data : ByteArray

Unlike ByteString, there is no offset/length – the entire ByteArray is the content.

Key API Mapping

Instances

• BEq ShortByteString
• Ord ShortByteString
• Inhabited ShortByteString – empty
• ToString ShortByteString

When to Use

• Use ShortByteString for small, long-lived keys (e.g., hash map keys) where GC overhead of the slice representation matters.
• Use ByteString for I/O buffers and large data where O(1) slicing is valuable.

Performance

Data.ByteString.Lazy

Lean: Hale.ByteString.Data.ByteString.Lazy | Haskell: Data.ByteString.Lazy

Overview

Lazy byte strings built from a spine of strict ByteString chunks connected via Thunk. This emulates Haskell’s lazy evaluation in Lean’s strict runtime.

Core Type

inductive LazyByteString where
  | empty : LazyByteString
  | chunk : (c : ByteString) → (h : c.len > 0) → Thunk LazyByteString → LazyByteString

The h : c.len > 0 invariant guarantees that every chunk in the spine is non-empty. This rules out degenerate representations and ensures that operations like null and length behave correctly.

Key API Mapping

Instances

• BEq LazyByteString
• Append LazyByteString – O(1) via thunk linking
• Inhabited LazyByteString – empty

Design Notes

• Non-empty chunk invariant: The proof h : c.len > 0 on every chunk constructor prevents empty chunks from appearing in the spine. This simplifies reasoning about null, head, and uncons.
• Thunk-based laziness: Each tail is wrapped in Thunk so chunks are only forced on demand, matching Haskell’s lazy list spine.
• Chunk size: fromChunks silently drops empty byte strings. Consumers should use defaultChunkSize (typically 32 KiB) when building lazy byte strings incrementally.

Performance

Data.ByteString.Builder

Lean: Hale.ByteString.Data.ByteString.Builder | Haskell: Data.ByteString.Builder

Overview

Continuation-based builder for efficient incremental construction of byte strings. The builder type wraps a difference-list style function, achieving O(1) concatenation.

Core Type

structure Builder where
  run : LazyByteString → LazyByteString

A Builder is a function that prepends its content onto a continuation LazyByteString. Two builders compose by function composition, giving O(1) append.

Key API Mapping

Monoid Law Proofs

The module proves that Builder forms a lawful monoid:

• empty_append: Builder.empty ++ b = b
• append_empty: b ++ Builder.empty = b
• append_assoc: (a ++ b) ++ c = a ++ (b ++ c)

These follow directly from function composition laws.

Usage Pattern

let b := Builder.byteString header
     ++ Builder.word32BE payloadLen
     ++ Builder.byteString payload
let result := Builder.toLazyByteString b

Performance

Word8 – UInt8 Classification

Lean: Hale.Word8 | Haskell: word8

UInt8 classification predicates and byte constants. All predicates are @[inline] for zero overhead. Proofs via exhaustive native_decide over all 256 values.

API

Files

• Hale/Word8/Data/Word8.lean – Classification predicates and constants

Time – Clock and Time Types

Lean: Hale.Time | Haskell: time

UTC time and durations. Wraps Lean’s IO.monoNanosNow for high-resolution monotonic timing.

Key Types

structure NominalDiffTime where
  nanoseconds : Int

Files

• Hale/Time/Data/Time/Clock.lean – NominalDiffTime, UTCTime

STM – Software Transactional Memory

Lean: Hale.STM | Haskell: stm

Pessimistic STM with global mutex serialization. Provides TVar, TMVar, and TQueue for concurrent programming.

Key Types

API

Files

• Hale/STM/Control/Monad/STM.lean – STM monad, atomically, retry, orElse
• Hale/STM/Control/Concurrent/STM/TVar.lean – Transactional variables
• Hale/STM/Control/Concurrent/STM/TMVar.lean – Transactional MVars
• Hale/STM/Control/Concurrent/STM/TQueue.lean – Transactional queues

DataDefault – Default Values

Lean: Hale.DataDefault | Haskell: data-default

Default typeclass providing sensible starting values, distinct from Inhabited.

Key Types

class Default (α : Type) where
  default : α

Instances for: Bool, Nat, Int, String, List, Array, Option, Unit, products.

Files

• Hale/DataDefault/Data/Default.lean – Default class and instances

ResourceT – Resource Management Monad

Lean: Hale.ResourceT | Haskell: resourcet

API Reference: Hale.ResourceT | Resource

Ensures cleanup of resources (file handles, connections) even on exceptions.

Lifecycle

  runResourceT ---+
                  |
    allocate(acquire, release)
       | -> (ReleaseKey, resource)
       |
    ... use resource ...
       |
    release(key)  <-- optional early release
       |
  +---- finally: all remaining cleanups run (LIFO order)

Detailed Flow

  +---------------------------------------------+
  | runResourceT                                 |
  |                                              |
  |   ref <- IO.mkRef #[]   (cleanup registry)  |
  |                                              |
  |   try                                        |
  |     allocate(open, close)                    |
  |       |  push (key0, close) to registry      |
  |       v                                      |
  |     allocate(connect, disconnect)            |
  |       |  push (key1, disconnect) to registry |
  |       v                                      |
  |     ... user code ...                        |
  |       |                                      |
  |     release(key0)  -- early release          |
  |       |  remove key0 from registry           |
  |       |  run close action                    |
  |       v                                      |
  |     ... more user code ...                   |
  |                                              |
  |   finally                                    |
  |     for (_, cleanup) in registry.reverse:    |
  |       try cleanup catch _ => ()              |
  |       -- key1 (disconnect) runs here         |
  |       -- key0 already released, not in list  |
  +---------------------------------------------+

Core Types

ResourceT (Monad Transformer)

def ResourceT (m : Type -> Type) (a : Type) := IO.Ref CleanupMap -> m a

ReleaseKey (Opaque, Single-Use)

structure ReleaseKey where
  private mk ::
    id : Nat

The constructor is private – only allocate can create keys.

Guarantees

• LIFO cleanup: Last allocated = first released
• Exception-safe: try/finally ensures all cleanups run
• Single-use keys: Releasing twice is a no-op (idempotent)
• Cleanup isolation: If one cleanup throws, remaining cleanups still run

Proven Properties (1 theorem)

Axiom-Dependent Properties (documented, not machine-checked)

• Exception safety depends on IO.finally semantics
• LIFO ordering depends on Array preserving insertion order (which it does)

Instances

• Monad (ResourceT m) (for any Monad m)
• MonadLift IO (ResourceT m) (for any MonadLift IO m)

Files

• Hale/ResourceT/Control/Monad/Trans/Resource.lean – Full implementation + 1 proof

UnliftIO – MonadUnliftIO

Lean: Hale.UnliftIO | Haskell: unliftio-core

Allows running monadic actions in IO by “unlifting” them. CPS form avoids universe issues.

Key Types

class MonadUnliftIO (m : Type → Type) where
  withRunInIO : ((∀ α, m α → IO α) → IO β) → m β

Laws

• withRunInIO (fun run => run m) = m (identity)
• withRunInIO (fun run => run (liftIO io)) = liftIO io (lift-run roundtrip)

Files

• Hale/UnliftIO/Control/Monad/IO/Unlift.lean – MonadUnliftIO class

Conduit – Stream Processing

Lean: Hale.Conduit | Haskell: conduit

Composable streaming data pipelines. ConduitT i o m r is a CPS wrapper over Pipe with O(1) monadic bind.

Key Types

API

Files

• Hale/Conduit/Data/Conduit.lean – Re-exports
• Hale/Conduit/Data/Conduit/Internal/Pipe.lean – Pipe type
• Hale/Conduit/Data/Conduit/Internal/Conduit.lean – ConduitT, fusion
• Hale/Conduit/Data/Conduit/Combinators.lean – Standard combinators

Network – POSIX Sockets with Phantom State

Lean: Hale.Network | Haskell: network

POSIX socket API with phantom type parameters encoding lifecycle states. A Socket (state : SocketState) tracks state transitions (fresh → bound → listening → connected → closed) at compile time, making it a type error to send on an unconnected socket or close an already-closed one.

Socket State Machine

  Fresh ──bind──► Bound ──listen──► Listening ──accept──► Connected
    │                                                         │
    └──────────────────── close ◄─────────────────────────────┘

Key Types

API

Files

• Hale/Network/Network/Socket/Types.lean – SocketState, SockAddr, phantom socket type
• Hale/Network/Network/Socket/FFI.lean – C FFI declarations
• Hale/Network/Network/Socket.lean – High-level API with state transitions
• Hale/Network/Network/Socket/ByteString.lean – ByteArray send/recv
• Hale/Network/Network/Socket/Blocking.lean – Blocking wrappers
• Hale/Network/Network/Socket/EventDispatcher.lean – kqueue/epoll dispatcher

IpRoute – IP Address Types

Lean: Hale.IpRoute | Haskell: iproute

IP addresses (IPv4, IPv6) and CIDR ranges with decidable membership predicate.

Key Types

API

Files

• Hale/IpRoute/Data/IP.lean – IPv4, IPv6, CIDR ranges

Recv – Socket Receive

Lean: Hale.Recv | Haskell: recv

Thin wrapper for socket recv returning ByteArray. Empty result signals EOF.

API

Files

• Hale/Recv/Network/Socket/Recv.lean – recv, recvString

StreamingCommons – Streaming Network Utilities

Lean: Hale.StreamingCommons | Haskell: streaming-commons

Streaming network utilities: bind/connect helpers and application data abstraction.

Key Types

API

Files

• Hale/StreamingCommons/Data/Streaming/Network.lean – AppData, bind/connect helpers

SimpleSendfile – Zero-Copy File Sending

Lean: Hale.SimpleSendfile | Haskell: simple-sendfile

Efficient file sending using sendfile(2) syscall for zero-copy transfer, with read+send fallback.

Key Types

structure FilePart where
  offset : Nat
  count  : Nat

API

Files

• Hale/SimpleSendfile/Network/Sendfile.lean – sendFile, FilePart

TLS – OpenSSL FFI Wrapper

Lean: Hale.TLS | Haskell: tls (concept) / OpenSSL bindings

API Reference: Hale.TLS | Types | Context | WarpTLS

HTTPS support via OpenSSL/LibreSSL C FFI.

TLS Handshake Flow

  Client                          Server
    |                               |
    |     TCP connect               |
    |------------------------------>|
    |                               |
    |     ClientHello               |
    |------------------------------>|
    |                               | SSL_accept()
    |     ServerHello + Cert        | (OpenSSL FFI)
    |<------------------------------|
    |                               |
    |     Key Exchange + Finished   |
    |------------------------------>|
    |                               |
    |     === TLS Established ===   |
    |                               |
    |     HTTP/1.1 (encrypted)      |
    |------------------------------>|
    |     or HTTP/2 (via ALPN)      |
    |                               |

Opaque Handles (FFI Pattern)

opaque TLSContextHandle : NonemptyType    -- SSL_CTX*
opaque TLSSessionHandle : NonemptyType    -- SSL*
def TLSContext := TLSContextHandle.type
def TLSSession := TLSSessionHandle.type

Both handles use the lean_alloc_external / lean_register_external_class pattern (same as Socket). The GC finalizer calls SSL_free / SSL_CTX_free automatically when the Lean object is collected.

API

TLS Version Types

inductive TLSVersion where
  | tls10 | tls11 | tls12 | tls13

Security

• Minimum TLS 1.2 (enforced by SSL_CTX_set_min_proto_version)
• ALPN for HTTP/2 negotiation (“h2” / “http/1.1”)
• Certificate + key validated at context creation time (OpenSSL rejects invalid files)
• Hardware AES-NI acceleration (via OpenSSL)
• Session finalizer ensures SSL_shutdown + SSL_free on GC

Integration with WarpTLS

WarpTLS.runTLS creates a TLSContext once at startup, then for each accepted connection:

1. Socket.accept  -> Socket .connected
2. TLS.acceptSocket ctx sock -> TLSSession
3. parseRequest + app + sendResponse (via TLS read/write)
4. TLS.close session
5. Socket.close sock

Both TLS session and socket are cleaned up in try/finally blocks.

Files

• Hale/TLS/Network/TLS/Types.lean – TLSVersion, CipherID
• Hale/TLS/Network/TLS/Context.lean – Opaque handles + FFI declarations

HttpTypes – Core HTTP Types

Lean: Hale.HttpTypes | Haskell: http-types

Core HTTP/1.1 types: methods, status codes, headers, versions, and URI query parsing. Status codes carry a bounded proof (100 ≤ code ≤ 999).

Key Types

API

Files

• Hale/HttpTypes/Network/HTTP/Types/Method.lean – StdMethod, Method
• Hale/HttpTypes/Network/HTTP/Types/Status.lean – Status with bounded proof
• Hale/HttpTypes/Network/HTTP/Types/Header.lean – Header types
• Hale/HttpTypes/Network/HTTP/Types/Version.lean – HttpVersion
• Hale/HttpTypes/Network/HTTP/Types/URI.lean – Query parsing and URL encoding

HttpDate – HTTP Date Parsing

Lean: Hale.HttpDate | Haskell: http-date

HTTP date parsing and formatting per RFC 7231. Supports IMF-fixdate, RFC 850, and asctime formats. Fields carry bounded proofs (month 1-12, day 1-31, hour 0-23, etc.).

Key Types

structure HTTPDate where
  year   : Nat
  month  : Nat  -- 1-12
  day    : Nat  -- 1-31
  hour   : Nat  -- 0-23
  minute : Nat  -- 0-59
  second : Nat  -- 0-60 (leap second)

Files

• Hale/HttpDate/Network/HTTP/Date.lean – HTTPDate type, parser, formatter

Http2 – HTTP/2 Protocol

Lean: Hale.Http2 | Haskell: http2

HTTP/2 framing, HPACK header compression, flow control, and server implementation per RFC 9113. Stream IDs carry a 31-bit bound proof. Settings carry RFC 9113 value constraint proofs.

Key Types

Modules

Files

• Hale/Http2/Network/HTTP2/Types.lean – Core types
• Hale/Http2/Network/HTTP2/Frame/Types.lean – Frame definitions
• Hale/Http2/Network/HTTP2/Frame/Encode.lean – Frame encoding
• Hale/Http2/Network/HTTP2/Frame/Decode.lean – Frame decoding
• Hale/Http2/Network/HTTP2/HPACK/Table.lean – HPACK tables
• Hale/Http2/Network/HTTP2/HPACK/Huffman.lean – Huffman coding
• Hale/Http2/Network/HTTP2/HPACK/Encode.lean – HPACK encoding
• Hale/Http2/Network/HTTP2/HPACK/Decode.lean – HPACK decoding
• Hale/Http2/Network/HTTP2/FlowControl.lean – Flow control
• Hale/Http2/Network/HTTP2/Stream.lean – Stream management
• Hale/Http2/Network/HTTP2/Server.lean – Server

Http3 – HTTP/3 Protocol

Lean: Hale.Http3 | Haskell: http3

HTTP/3 framing and QPACK header compression per RFC 9114. Uses QUIC variable-length integer encoding (RFC 9000 Section 16) with proven roundtrip properties.

Key Types

Proven Properties

• decodeVarInt (encodeVarInt n) = some n (roundtrip)

Modules

Files

• Hale/Http3/Network/HTTP3/Frame.lean – Frame types, varint codec
• Hale/Http3/Network/HTTP3/Error.lean – Error codes
• Hale/Http3/Network/HTTP3/QPACK/Table.lean – QPACK tables
• Hale/Http3/Network/HTTP3/QPACK/Encode.lean – QPACK encoding
• Hale/Http3/Network/HTTP3/QPACK/Decode.lean – QPACK decoding
• Hale/Http3/Network/HTTP3/Server.lean – Server

QUIC – QUIC Transport Protocol

Lean: Hale.QUIC | Haskell: quic

QUIC transport protocol types per RFC 9000. Connection IDs carry a bounded-length proof (≤ 20 bytes). Stream IDs encode directionality (client/server, bidi/uni) in the type.

Key Types

Modules

Files

• Hale/QUIC/Network/QUIC/Types.lean – ConnectionId, StreamId, TransportParams
• Hale/QUIC/Network/QUIC/Config.lean – Configuration
• Hale/QUIC/Network/QUIC/Connection.lean – Connection management
• Hale/QUIC/Network/QUIC/Stream.lean – Stream management
• Hale/QUIC/Network/QUIC/Server.lean – Server
• Hale/QUIC/Network/QUIC/Client.lean – Client

BsbHttpChunked – Chunked Transfer Encoding

Lean: Hale.BsbHttpChunked | Haskell: bsb-http-chunked

HTTP/1.1 chunked transfer encoding framing. Each chunk: <hex-length>\r\n<data>\r\n. Terminator: 0\r\n\r\n.

API

Files

• Hale/BsbHttpChunked/Network/HTTP/Chunked.lean – Chunked encoding helpers

HttpClient – HTTP Client

Lean: Hale.HttpClient | Haskell: http-client

HTTP client with pluggable transport. Connection abstracts plain TCP and TLS uniformly.

Key Types

API

Modules

• Types – Core types
• Connection – Transport abstraction
• Request – Request building and serialization
• Response – Response parsing
• Redirect – Redirect following

Files

• Hale/HttpClient/Network/HTTP/Client/Types.lean – Connection, Request, Response
• Hale/HttpClient/Network/HTTP/Client/Connection.lean – Transport
• Hale/HttpClient/Network/HTTP/Client/Request.lean – Request
• Hale/HttpClient/Network/HTTP/Client/Response.lean – Response
• Hale/HttpClient/Network/HTTP/Client/Redirect.lean – Redirects

HttpConduit – HTTP + Conduit Integration

Lean: Hale.HttpConduit | Haskell: http-conduit

Conduit integration for HTTP client and simple high-level HTTP API.

API

Files

• Hale/HttpConduit/Network/HTTP/Client/Conduit.lean – Conduit bridge
• Hale/HttpConduit/Network/HTTP/Simple.lean – Simple one-shot API

Req – Type-Safe HTTP Client

Lean: Hale.Req | Haskell: req

Type-safe HTTP client with compile-time guarantees: method/body compatibility, HTTPS-only auth, non-empty hostnames, proven option monoid laws.

Compile-Time Guarantees

• HttpBodyAllowed prevents GET with body
• basicAuth returns Option .Https for type safety
• Hostname non-emptiness proven at construction

Files

• Hale/Req/Network/HTTP/Req.lean – Type-safe request builders

WAI – Web Application Interface

Lean: Hale.WAI | Haskell: wai

API Reference: Hale.WAI | Network.Wai.Internal | Network.Wai

The core abstraction for Hale’s HTTP ecosystem. Every web application, middleware, and server speaks WAI.

Request Lifecycle

   Client HTTP Request
         |
         v
  +--------------+     +------------------+
  | Socket.accept |---->| parseRequest     |
  |  (.listening) |     | (headers, body)  |
  +--------------+     +--------+---------+
                                |
                     WAI Request struct
                                |
         +----------------------+----------------------+
         |                      |                      |
         v                      v                      v
  +--------------+     +--------------+     +--------------+
  |  Middleware   |---->|  Middleware   |---->|  Application |
  |  (ForceSSL)  |     |  (Logger)    |     |  (user code) |
  +--------------+     +--------------+     +------+-------+
                                                    |
                                             Response (inductive)
                                                    |
                       +----------------------------+----------+
                       |              |              |          |
                       v              v              v          v
                  responseFile   responseBuilder  responseStream  responseRaw
                  (sendfile)    (in-memory)      (chunked)       (WebSocket)
                       |              |              |          |
                       +--------------+--------------+----------+
                                       |
                                sendResponse
                                       |
                                       v
                              Socket.connected

Core Types

Application (CPS + Indexed Monad)

abbrev Application :=
  Request -> (Response -> IO ResponseReceived) -> AppM .pending .sent ResponseReceived

The return type AppM .pending .sent ResponseReceived is an indexed monad that leverages Lean 4’s dependent types to enforce exactly-once response at compile time:

• .pending → .sent: The application must transition from “no response” to “response sent”. AppM.respond is the only combinator that performs this transition.
• No double-respond: After respond, the state is .sent. A second respond would need AppM .sent .sent, which does not exist – type error.
• No skip-respond: The return type demands .sent as post-state. Returning without calling respond would leave the state at .pending – type error.
• No fabrication: AppM.mk is private. Application code cannot construct the value without going through the real combinators.

This is strictly stronger than Haskell’s WAI, where the contract is a gentleman’s agreement. Here the Lean 4 kernel verifies it.

Middleware (Monoid under Composition)

abbrev Middleware := Application -> Application

Proven algebraic properties:

Response (4 Delivery Modes)

inductive Response where
  | responseFile    (status headers path part)   -- sendfile(2)
  | responseBuilder (status headers body)        -- in-memory ByteArray
  | responseStream  (status headers body)        -- chunked streaming
  | responseRaw     (rawAction fallback)         -- raw socket (WebSocket)

Proven accessor laws (12 theorems):

• status_responseBuilder s h b = s (and for File, Stream)
• headers_responseBuilder s h b = h (and for File)
• mapResponseHeaders id r = r (per constructor: builder, file, stream)
• mapResponseStatus id r = r (per constructor: builder, file, stream)

RequestBodyLength (Dependent Encoding)

inductive RequestBodyLength where
  | chunkedBody                    -- Transfer-Encoding: chunked
  | knownLength (bytes : Nat)      -- Content-Length: N

Full Theorem List (17)

Response Accessor Laws (11, in Internal.lean)

Middleware Algebra (5, in Wai.lean)

Response Linearity (Compile-Time Guarantee)

• Exactly-once response: The indexed AppM monad enforces at the type level that respond is invoked exactly once. AppM .pending .sent ResponseReceived can only be produced via AppM.respond (which transitions .pending → .sent). Double-respond is a compile-time error: no combinator transitions .sent → .sent. The private mk on AppM prevents circumventing the guarantee.

Files

• Hale/WAI/Network/Wai/Internal.lean – Core types + 11 accessor theorems
• Hale/WAI/Network/Wai.lean – Public API + 5 middleware algebra theorems

Warp – High-Performance HTTP Server

Lean: Hale.Warp | Haskell: warp

API Reference: Hale.Warp | Types | Settings | Request | Response | Run

A fast HTTP/1.x server achieving 156,000+ requests/sec with keep-alive.

Connection Lifecycle

  runSettings(port, app)
         |
         v
  +--------------------+
  | listenTCP(port)    |
  | Socket(.listening) |
  +--------+-----------+
           |
     acceptLoop <------------------------------------+
           |                                          |
           v                                          |
  +--------------------+                              |
  | Socket.accept      |                              |
  | -> (.connected)    |                              |
  +--------+-----------+                              |
           |                                          |
     forkIO (green thread)                            |
           |                                          |
           v                                          |
  +------------------------+                          |
  | runConnection          |                          |
  |  +------------------+  |                          |
  |  | parseRequest     |  |                          |
  |  | -> WAI.Request   |  |                          |
  |  +--------+---------+  |                          |
  |           |             |                          |
  |  +--------v---------+  |                          |
  |  | app(req, respond) |  |                          |
  |  | -> Response       |  |                          |
  |  +--------+---------+  |                          |
  |           |             |                          |
  |  +--------v---------+  |                          |
  |  | sendResponse     |  |                          |
  |  +--------+---------+  |                          |
  |           |             |                          |
  |  +--------v---------+  |                          |
  |  | connAction?      |  |                          |
  |  | keepAlive/close  |  |                          |
  |  +--------+---------+  |                          |
  |           |             |                          |
  |     +-----+-----+      |                          |
  |     | keepAlive  |      |                          |
  |     | -> loop ---+------+-- (back to parseRequest) |
  |     |            |      |                          |
  |     | close      |      |                          |
  |     | -> cleanup |      |                          |
  |     +------------+      |                          |
  +-------------------------+                          |
                                                       |
           <-------------------------------------------+

Transport Abstraction

inductive Transport where
  | tcp                                         -- plain channel
  | tls (major minor : Nat) (alpn : Option String) (cipher : UInt16)
  | quic (alpn : Option String) (cipher : UInt16)

Security proofs:

Keep-Alive State Machine

  +---------------+    Connection: close    +-----------+
  |   HTTP/1.1    | ----------------------> |   CLOSE   |
  | (keep-alive   |                         +-----------+
  |  by default)  |    no Connection hdr         ^
  |               | ----------------------> keepAlive
  +---------------+                              |
                                                 |
  +---------------+    Connection: keep-alive    |
  |   HTTP/1.0    | ----------------------> keepAlive
  | (close by     |
  |  default)     |    no Connection hdr    +-----------+
  |               | ----------------------> |   CLOSE   |
  +---------------+                         +-----------+

Proven semantics:

• connAction_http10_default: HTTP/1.0 without Connection header -> close
• connAction_http11_default: HTTP/1.1 without Connection header -> keep-alive

How Lean 4’s Dependent Types Secure the Warp Server

Warp is where every dependent-type technique in Hale converges: phantom state machines, proof-carrying structures, and indexed monads all cooperate to make entire classes of server bugs unrepresentable.

Socket State Machine (phantom type parameter)

structure Socket (state : SocketState) where   -- phantom parameter, erased at runtime
  raw : RawSocket

-- Every function declares its pre/post state:
listenTCP  : ... -> IO (Socket .listening)
accept     : Socket .listening -> IO (Socket .connected × SockAddr)
send       : Socket .connected -> ByteArray -> IO Nat
close      : Socket state -> (state ≠ .closed := by decide) -> IO (Socket .closed)

-- All of these are compile-time errors (not runtime, not asserts):
-- accept freshSocket       -- .fresh ≠ .listening
-- send listeningSocket     -- .listening ≠ .connected
-- close closedSocket       -- cannot prove .closed ≠ .closed

Exactly-Once Response (indexed monad)

The server provides a respond callback and calls (app req respond).run. The AppM .pending .sent return type guarantees that by the time .run executes, the application has called respond exactly once:

-- In runConnection (the trust boundary):
let _received ← (app req fun resp => sendResponse sock settings req resp).run

Settings with Proof Fields (zero-cost invariants)

structure Settings where
  settingsPort : UInt16
  settingsTimeout : Nat := 30
  settingsBacklog : Nat := 128
  settingsTimeoutPos : settingsTimeout > 0 := by omega   -- erased at runtime
  settingsBacklogPos : settingsBacklog > 0 := by omega   -- erased at runtime

The proof fields are erased at compile time (zero cost, same sizeof). It is impossible to construct a Settings with a zero timeout or zero backlog – the by omega obligation cannot be discharged for 0 > 0.

InvalidRequest (Exhaustive Error Model)

inductive InvalidRequest where
  | notEnoughLines | badFirstLine | nonHttp | incompleteHeaders
  | connectionClosedByPeer | overLargeHeader | badProxyHeader
  | payloadTooLarge | requestHeaderFieldsTooLarge

Full Theorem List (11)

Transport Security (3, in Types.lean)

Keep-Alive Semantics (2, in Run.lean)

HTTP Version Parsing (5, in Request.lean)

Settings Validity (1, in Settings.lean)

Performance

• 156k QPS (wrk, 4 threads, 50 connections, keep-alive)
• 30k QPS (ab, 100 connections, no keep-alive)
• Green threads via forkIO (scheduler-managed, not OS threads)
• RecvBuffer in C (CRLF scanning entirely in native code)

Files (17 modules)

WarpTLS – HTTPS for Warp

Lean: Hale.WarpTLS | Haskell: warp-tls

HTTPS support for Warp using OpenSSL FFI. TLS 1.2+ enforced. ALPN negotiation for HTTP/2. Uses EventDispatcher and Green monad for non-blocking I/O.

Key Types

Files

• Hale/WarpTLS/Network/Wai/Handler/WarpTLS.lean – runTLS, TLS settings
• Hale/WarpTLS/Network/Wai/Handler/WarpTLS/Internal.lean – Internal types

WarpQUIC – HTTP/3 over QUIC

Lean: Hale.WarpQUIC | Haskell: warp-quic

WAI handler over HTTP/3/QUIC transport. TLS 1.3 mandatory (QUIC requirement).

Key Types

structure Settings where
  port     : Nat
  certFile : String
  keyFile  : String

Files

• Hale/WarpQUIC/Network/Wai/Handler/WarpQUIC.lean – Settings, QUIC server entry point

WaiExtra – Middleware Collection

Lean: Hale.WaiExtra | Haskell: wai-extra

API Reference: Hale.WaiExtra | AddHeaders | ForceSSL | Gzip | HttpAuth | Test

36 middleware modules for request/response transformation.

Middleware Composition

         +----------------------------------------------+
         |         Middleware Composition                 |
         |                                               |
         |   m1 . m2 . m3 : Middleware                   |
         |                                               |
         |   Algebraic Laws:                             |
         |     id . m = m        (left identity)         |
         |     m . id = m        (right identity)        |
         |     (f.g).h = f.(g.h) (associativity)         |
         +----------------------------------------------+

  Request --> m1 --> m2 --> m3 --> App --> Response
              |       |       |              |
              | modify| check |              | modify
              | headers auth  |              | headers
              v       v       v              v

Available Middleware

Request Modification

Response Modification

Routing and Filtering

Security

Monitoring

Protocol

Proven Properties (11 theorems)

All proofs are in the source files, verified at compile time (no sorry):

AddHeaders Identity (3, in AddHeaders.lean)

StripHeaders Identity (3, in StripHeaders.lean)

Select (1, in Select.lean)

Routed (2, in Routed.lean)

ForceSSL (1, in ForceSSL.lean)

HealthCheck (1, in HealthCheckEndpoint.lean)

Files (36 modules)

WaiAppStatic – Static File Serving

Lean: Hale.WaiAppStatic | Haskell: wai-app-static

API Reference: Hale.WaiAppStatic | Types | Filesystem | Static

Serves static files from the filesystem with type-safe path validation.

Request Flow

  GET /css/style.css
         |
         v
  +---------------------+
  | toPieces(pathInfo)   |  Validate each path segment
  | "css"       -> Piece |  No dots, no slashes
  | "style.css" -> Piece |
  +--------+------------+
           |
  +--------v------------+
  | ssLookupFile         |  Filesystem stat + MIME lookup
  | -> LookupResult      |
  +--------+------------+
           |
     +-----+------+------------+------------+
     |            |            |            |
     v            v            v            v
  lrFile      lrFolder     lrNotFound   lrRedirect
  200 OK      try index    404          301
  + Cache     files
  + MIME

Dependent Type: Piece (Path Traversal Prevention)

structure Piece where
  val : String
  no_dot   : startsDot val = false        -- no dotfiles
  no_slash : containsSlash val = false     -- no path traversal

The no_dot and no_slash fields are proofs, erased at runtime. A Piece is just a String at runtime, but the type system guarantees it cannot contain a leading dot or an embedded slash.

Smart Constructor

def toPiece (t : String) : Option Piece  -- None if invalid!

Proven properties (4 theorems, in Types.lean):

Security guarantee: It is impossible to construct a Piece with a leading dot or embedded slash. The staticApp function only accepts Piece values, so dotfile serving and path traversal are prevented by the type system, not by runtime checks.

Other Types

LookupResult (File Lookup Outcome)

inductive LookupResult where
  | lrFile (file : File)       -- found a file
  | lrFolder                   -- found a directory
  | lrNotFound                 -- path does not exist
  | lrRedirect (pieces : Pieces)  -- client should be redirected

MaxAge (Cache Control)

inductive MaxAge where
  | noMaxAge                   -- no cache-control header
  | maxAgeSeconds (seconds : Nat)  -- max-age=N
  | maxAgeForever              -- ~1 year (31536000s)
  | noStore                    -- cache-control: no-store
  | noCache                    -- cache-control: no-cache

StaticSettings (Server Configuration)

structure StaticSettings where
  ssLookupFile    : Pieces -> IO LookupResult
  ssGetMimeType   : Piece -> String
  ssMaxAge        : MaxAge := .maxAgeSeconds 3600
  ssRedirectToIndex : Bool := true
  ssIndices       : List Piece := [unsafeToPiece "index.html"]
  ssListing       : Option (Pieces -> IO Response) := none

Files

• WaiAppStatic/Types.lean – Piece, LookupResult, StaticSettings + 4 proofs
• WaiAppStatic/Storage/Filesystem.lean – Filesystem backend
• Network/Wai/Application/Static.lean – WAI Application wrapper

WaiHttp2Extra – HTTP/2 Server Push

Lean: Hale.WaiHttp2Extra | Haskell: wai-http2-extra

HTTP/2 server push via referer prediction. Learns resource associations from Referer headers and proactively pushes on subsequent requests. LRU eviction for bounded memory.

Key Types

API

Modules

• Types – PushSettings, configuration
• LRU – LRU eviction cache
• Manager – Thread-safe push table
• ParseURL – URL parsing for same-origin checks
• Referer – Main middleware entry point

Files

• Hale/WaiHttp2Extra/Network/Wai/Middleware/Push/Referer.lean – Main middleware
• Hale/WaiHttp2Extra/Network/Wai/Middleware/Push/Referer/Types.lean – Configuration
• Hale/WaiHttp2Extra/Network/Wai/Middleware/Push/Referer/LRU.lean – LRU cache
• Hale/WaiHttp2Extra/Network/Wai/Middleware/Push/Referer/Manager.lean – Push manager
• Hale/WaiHttp2Extra/Network/Wai/Middleware/Push/Referer/ParseURL.lean – URL parsing

WaiWebSockets – WebSocket WAI Handler

Lean: Hale.WaiWebSockets | Haskell: wai-websockets

Upgrade WAI requests to WebSocket connections.

API

Files

• Hale/WaiWebSockets/Network/Wai/Handler/WebSockets.lean – WebSocket upgrade handler

WebSockets – RFC 6455 Protocol

Lean: Hale.WebSockets | Haskell: websockets

API Reference: Hale.WebSockets | Types | Frame | Handshake | Connection | WAI Bridge

Native WebSocket framing implementation with typed state machine.

WebSocket Upgrade Flow

  HTTP GET /chat
  Upgrade: websocket
  Connection: Upgrade
  Sec-WebSocket-Key: dGhlIHNhbXBsZQ==
  Sec-WebSocket-Version: 13
         |
         v
  +----------------------------+
  | isValidHandshake(headers)? |
  |   Check Upgrade header     |
  +------+-------+-------------+
         |yes    |no
         v       v
  +----------+  +--------------+
  | Handshake|  | Normal HTTP  |
  | SHA-1+B64|  | Application  |
  +----+-----+  +--------------+
       |
       v HTTP 101 Switching Protocols
  +----------------------------+
  |  PendingConnection         |
  |  state = .pending          |
  +------------+---------------+
               | acceptIO
               v
  +----------------------------+
  |  Connection                |
  |  state = .open_            |
  |                            |
  |  sendText / sendBinary     |
  |  receiveData / receiveText |
  |  sendPing (auto-pong)      |
  +------------+---------------+
               | sendClose
               v
  +----------------------------+
  |  state = .closing          |
  |  (awaiting close frame)    |
  +------------+---------------+
               | receive close
               v
  +----------------------------+
  |  state = .closed           |
  +----------------------------+

Frame Format (RFC 6455 section 5.2)

  0                   1                   2                   3
  0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1
 +-+-+-+-+-------+-+-------------+-------------------------------+
 |F|R|R|R| opcode|M| Payload len |   Extended payload length     |
 |I|S|S|S|  (4)  |A|     (7)     |          (16/64)              |
 |N|V|V|V|       |S|             |  (if payload len==126/127)    |
 | |1|2|3|       |K|             |                               |
 +-+-+-+-+-------+-+-------------+-------------------------------+
 | Masking-key (if MASK=1)       |         Payload Data          |
 +-------------------------------+-------------------------------+

Dependent Types

Opcode (Bounded to 4 bits)

inductive Opcode where
  | continuation | text | binary | close | ping | pong
  | reserved (val : Fin 16)   -- Fin 16 bounds to [0, 15]

The reserved constructor uses Fin 16 to statically guarantee all opcode values fit in 4 bits, matching the wire format.

Connection State Machine

inductive ConnectionState where
  | pending   -- handshake not completed
  | open_     -- data transfer active
  | closing   -- close frame sent
  | closed    -- terminated

CloseCode (Typed Status Codes)

structure CloseCode where
  code : UInt16

-- Named constants:
CloseCode.normal         -- 1000
CloseCode.goingAway      -- 1001
CloseCode.protocolError   -- 1002
CloseCode.unsupportedData -- 1003

ServerApp (Application Type)

abbrev ServerApp := PendingConnection -> IO Unit

Proven Properties (6 theorems)

All opcode encoding/decoding roundtrips, in Types.lean:

Implementation Notes

• XOR masking: applyMask applies the 4-byte masking key via XOR. XOR is its own inverse, so the same function masks and unmasks.
• Auto-pong: When a ping control frame is received during receiveData, the connection automatically replies with a pong frame (RFC 6455 section 5.5.3).
• SHA-1 placeholder: The handshake module contains a placeholder SHA-1 implementation. TODO: replace with full FIPS 180-4 implementation for production.

Files

• Types.lean – Core types (Opcode, ConnectionState, Connection, PendingConnection) + 6 roundtrip proofs
• Frame.lean – Frame encode/decode + XOR masking
• Handshake.lean – WebSocket upgrade (SHA-1 + Base64, magic GUID)
• Connection.lean – High-level send/receive API with auto-pong

CaseInsensitive – Case-Insensitive Comparison

Lean: Hale.CaseInsensitive | Haskell: case-insensitive

Wrapper type CI α that compares values case-insensitively while preserving the original. Stores both original and pre-computed foldedCase. Equality, ordering, and hashing use only foldedCase.

Key Types

Files

• Hale/CaseInsensitive/Data/CaseInsensitive.lean – FoldCase, CI

Vault – Type-Safe Heterogeneous Map

Lean: Hale.Vault | Haskell: vault

Type-safe heterogeneous container keyed by Key α tokens. Backed by Std.HashMap mapping unique Nat IDs to type-erased values.

Key Types

Axiom-Dependent Properties

• Type safety of lookup depends on axiom that unsafeCast is safe when the original value was of type α

Files

• Hale/Vault/Data/Vault.lean – Key, Vault, insert, lookup, delete

AutoUpdate – Periodic Cached Values

Lean: Hale.AutoUpdate | Haskell: auto-update

Periodically updated cached values. Runs an IO action in a background task and caches the result for consumers. Uses IO.asTask with .dedicated priority and Std.CancellationToken for lifecycle management.

Key Types

structure UpdateSettings (α : Type) where
  interval : Nat      -- update interval in microseconds
  action   : IO α     -- action to run periodically

Files

• Hale/AutoUpdate/Control/AutoUpdate.lean – UpdateSettings, mkAutoUpdate

TimeManager – Connection Timeout Management

Lean: Hale.TimeManager | Haskell: time-manager

Periodically sweeps registered handles and fires timeout callbacks for expired connections. Uses IO.asTask with .dedicated priority.

Guarantees

• tickle resets timeout – O(1)
• cancel prevents future firing
• Thread-safe via IO.Ref atomicity

Files

• Hale/TimeManager/System/TimeManager.lean – TimeManager, Handle, tickle, cancel

Cookie – HTTP Cookie Parsing

Lean: Hale.Cookie | Haskell: cookie

Parse Cookie and Set-Cookie headers per RFC 6265.

Key Types

API

Files

• Hale/Cookie/Web/Cookie.lean – CookiePair, parseCookies

MimeTypes – MIME Type Lookup

Lean: Hale.MimeTypes | Haskell: mime-types

Map file extensions to MIME types. Default fallback: application/octet-stream. Handles multi-part extensions (e.g., tar.gz).

Key Types

API

Files

• Hale/MimeTypes/Network/Mime.lean – MimeType, MimeMap, lookup

Base64 – RFC 4648 Codec

Lean: Hale.Base64 | Haskell: base64-bytestring

Base64 encoding and decoding per RFC 4648.

Guarantees

• decode (encode bs) = some bs (roundtrip)
• Output of encode contains only [A-Za-z0-9+/=]

API

Files

• Hale/Base64/Data/ByteString/Base64.lean – encode, decode

FastLogger – Buffered Thread-Safe Logging

Lean: Hale.FastLogger | Haskell: fast-logger

High-performance buffered logger with mutex synchronization and periodic flushing via AutoUpdate. Supports stdout, stderr, file, and callback destinations.

Key Types

Files

• Hale/FastLogger/System/Log/FastLogger.lean – LogType, LogStr, logger lifecycle

WaiLogger – WAI Request Logging

Lean: Hale.WaiLogger | Haskell: wai-logger

Formats HTTP request/response data in Apache Combined Log Format: host - - [date] "method path version" status size.

API

Files

• Hale/WaiLogger/Network/Wai/Logger.lean – apacheFormat

UnixCompat – POSIX Compatibility

Lean: Hale.UnixCompat | Haskell: unix-compat

Subset of POSIX operations needed by Warp: file descriptor operations and close-on-exec.

Key Types

API

Files

• Hale/UnixCompat/System/Posix/Compat.lean – Fd, FileStatus, closeFd

AnsiTerminal – Terminal ANSI Codes

Lean: Hale.AnsiTerminal | Haskell: ansi-terminal

ANSI terminal escape codes for colored output.

Key Types

API

Files

• Hale/AnsiTerminal/System/Console/ANSI.lean – Color, Intensity, escape code helpers

PSQueues – Priority Search Queues

Lean: Hale.PSQueues | Haskell: psqueues

Priority search queues (IntPSQ) for efficient priority-indexed operations.

Files

• Hale/PSQueues/Data/IntPSQ.lean – IntPSQ implementation

DataFrame – Tabular Data

Lean: Hale.DataFrame | Haskell: dataframe (adapted)

Tabular data structure with typed columns, supporting subset, sort, join, aggregation, statistics, and CSV I/O.

Modules

Files

• Hale/DataFrame/DataFrame.lean – Re-exports
• Hale/DataFrame/DataFrame/Internal/Types.lean – Core types
• Hale/DataFrame/DataFrame/Internal/Column.lean – Column operations
• Hale/DataFrame/DataFrame/Operations/*.lean – Operations
• Hale/DataFrame/DataFrame/IO/CSV.lean – CSV I/O
• Hale/DataFrame/DataFrame/Display.lean – Display

API Reference

The API reference is auto-generated by doc-gen4 from Lean docstrings. Every public definition, structure, class, and theorem is documented.

Browse the full API reference

Quick Links

Core Infrastructure

• Hale.Base — Foundational types, functors, monads
• Hale.ByteString — Byte array operations
• Hale.Network — POSIX sockets with phantom state
• Hale.HttpTypes — HTTP methods, status, headers, URI

Web Application Interface

• Hale.WAI — Request/Response/Application/Middleware
• Hale.Warp — HTTP/1.x server
• Hale.WarpTLS — HTTPS via OpenSSL
• Hale.WaiExtra — 36 middleware modules
• Hale.WaiAppStatic — Static file serving
• Hale.WebSockets — RFC 6455 WebSocket protocol

Protocol Implementations

• Hale.Http2 — HTTP/2 framing (RFC 9113)
• Hale.Http3 — HTTP/3 framing + QPACK
• Hale.QUIC — QUIC transport
• Hale.TLS — OpenSSL FFI wrapper

Proven Properties Catalog

All theorems link to their source modules in the API Reference.

Total: 257 compile-time verified theorems across 52 files

All theorems are checked by the Lean 4 kernel at compile time. The codebase is completely sorry-free — every proof obligation is fully discharged.

Algebraic Laws

Monoid/Semigroup Associativity (8, in Base/Data/Newtype.lean)

Functor Laws (14)

Monad Laws (9)

Monad Combinators (1)

Data Structure Properties

Either (3)

Maybe/Option (8)

Tuple (7)

List (4)

NonEmpty (4)

Ord/Down (2)

Bool (5)

Void (1)

Function (5)

Foldable (2)

String (1)

Char (3)

Ix (1)

ExitCode (2)

Numeric Type Properties

Complex (2)

Fixed-Point (5)

Time (2)

Protocol Correctness

HTTP Method Properties (21, in HttpTypes/Network/HTTP/Types/Method.lean)

HTTP Status Properties (13, in HttpTypes/Network/HTTP/Types/Status.lean)

HTTP Version Properties (4, in HttpTypes/Network/HTTP/Types/Version.lean)

Transport Security (3, in Warp/Types.lean)

Keep-Alive Semantics (2, in Warp/Run.lean)

HTTP Version Parsing (5, in Warp/Request.lean)

Warp Settings (1, in Warp/Settings.lean)

Encoding/Decoding Roundtrips

HTTP/2 Frame Types (10, in Http2/Network/HTTP2/Frame/Types.lean)