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.