Haskell's web ecosystem, ported to Lean 4 with maximalist typing.

257 compile-time theorems · 45 ported libraries · 241 Lean modules

Overview

hale ports 45 Haskell libraries (241 Lean modules) covering everything from foundational types to a full HTTP/1-2-3 web server stack. Unlike a minimal port, types encode correctness proofs, invariants, and guarantees wherever feasible:

• Correctness: Lawful typeclasses (LawfulBifunctor, LawfulCategory, LawfulTraversable) with verified laws
• Invariants: Ratio enforces positive denominator and coprimality in its type; NonEmpty guarantees length >= 1
• Proofs: clamp returns {y : a // lo <= y && y <= hi}; Fixed.add_exact proves addition preserves precision
• 257 compile-time verified theorems across 52 files, checked by the Lean 4 kernel

Quick Start

Add to your lakefile.toml:

[[require]]
name = "hale"
git = "<repository-url>"
rev = "main"

Then import:

import Hale
open Hale

Ported Libraries

Core Infrastructure

Lean Package	Haskell Package	Description
Hale.Base	base	Foundational types, functors, monads, concurrency
Hale.ByteString	bytestring	Byte array operations (strict, lazy, builder)
Hale.Word8	word8	Word8 character classification
Hale.Time	time	Clock and time types
Hale.STM	stm	Software transactional memory
Hale.DataDefault	data-default	Default values
Hale.ResourceT	resourcet	Resource management monad
Hale.UnliftIO	unliftio-core	MonadUnliftIO
Hale.Conduit	conduit	Composable streaming data pipelines

Networking

Lean Package	Haskell Package	Description
Hale.Network	network	POSIX sockets with phantom state
Hale.IpRoute	iproute	IP address types
Hale.Recv	recv	Socket receive
Hale.StreamingCommons	streaming-commons	Streaming network utilities
Hale.SimpleSendfile	simple-sendfile	sendfile(2) wrapper
Hale.TLS	tls	TLS via OpenSSL FFI

HTTP

Lean Package	Haskell Package	Description
Hale.HttpTypes	http-types	HTTP methods, status, headers, URI
Hale.HttpDate	http-date	HTTP date parsing
Hale.Http2	http2	HTTP/2 framing, HPACK, server
Hale.Http3	http3	HTTP/3 framing, QPACK
Hale.QUIC	quic	QUIC transport
Hale.BsbHttpChunked	bsb-http-chunked	Chunked transfer encoding
Hale.HttpClient	http-client	HTTP client with pluggable transport
Hale.HttpConduit	http-conduit	HTTP + Conduit integration
Hale.Req	req	Type-safe HTTP client

Web Application Interface

Lean Package	Haskell Package	Description
Hale.WAI	wai	Request/Response/Application/Middleware
Hale.Warp	warp	HTTP/1.x server
Hale.WarpTLS	warp-tls	HTTPS via OpenSSL
Hale.WarpQUIC	warp-quic	HTTP/3 over QUIC
Hale.WaiExtra	wai-extra	36 middleware modules
Hale.WaiAppStatic	wai-app-static	Static file serving
Hale.WaiHttp2Extra	wai-http2-extra	HTTP/2 server push
Hale.WaiWebSockets	wai-websockets	WebSocket WAI handler
Hale.WebSockets	websockets	RFC 6455 WebSocket protocol

Utilities

Lean Package	Haskell Package	Description
Hale.CaseInsensitive	case-insensitive	Case-insensitive strings
Hale.Vault	vault	Type-safe heterogeneous storage
Hale.AutoUpdate	auto-update	Periodic cached values
Hale.TimeManager	time-manager	Connection timeout management
Hale.Cookie	cookie	HTTP cookie parsing
Hale.MimeTypes	mime-types	MIME type lookup
Hale.Base64	base64-bytestring	RFC 4648 codec
Hale.FastLogger	fast-logger	Buffered thread-safe logging
Hale.WaiLogger	wai-logger	WAI request logging
Hale.UnixCompat	unix-compat	POSIX compatibility
Hale.AnsiTerminal	ansi-terminal	Terminal ANSI codes
Hale.PSQueues	psqueues	Priority search queues

Data

Lean Package	Haskell Package	Description
Hale.DataFrame	dataframe (adapted)	Tabular data with typed columns, CSV I/O

Typing Philosophy

Lean 4 is a dependently-typed proof assistant that compiles to efficient native code. Hale leverages this to turn protocol specs, resource lifecycles, and algebraic laws into compile-time obligations -- verified by the kernel, then erased at runtime (zero overhead).

• Phantom state machines: Socket (state : SocketState) makes it a type error to send on an unconnected socket or close an already-closed one (proof obligation: state != .closed, discharged by decide)
• Indexed monads: AppM .pending .sent ResponseReceived enforces that a WAI application calls respond exactly once -- double-respond is a compile-time error, not a runtime crash
• Proof-carrying structures: Ratio carries den_pos and coprime proofs; Settings carries timeout_pos -- all erased at runtime (zero cost)
• Algebraic laws: 257 theorems (bimap_id, bind_assoc, map_id, connAction_http11_default, ...) verified by the Lean kernel

Documentation

• docs/ -- Per-module documentation with API mappings and examples
• docs/Proofs.md -- Complete catalog of all 257 theorems
• Tests/ -- 82 Lean test files
• Tests/cross-check/ -- 9 Haskell cross-verification scripts

Build & Test

nix-shell                               # Nix users: enter shell with OpenSSL + pkg-config
lake build                              # Build the library
lake exe hale                           # Run smoke tests
lake build hale-tests && lake exe hale-tests  # Run test suite
bash tests/cross-check/run-all.sh       # Cross-check with Haskell (requires GHC)

Requires OpenSSL headers for TLS support. On non-Nix systems, ensure pkg-config openssl works (e.g., brew install openssl pkg-config on macOS, apt install libssl-dev pkg-config on Debian/Ubuntu).

License

See LICENSE for details.