structure Network.Wai.ResponseReceived : Type

Opaque token proving a response was sent.

private mk ensures that application code cannot fabricate this token. Only server implementations (via ResponseReceived.done) and the AppM.respond combinator produce it. Combined with the AppM indexed monad, this means: an application that type-checks has necessarily invoked the response callback exactly once.

def Network.Wai.ResponseReceived.done : ResponseReceived

Construct a ResponseReceived token. Intended for use by server implementations (e.g., Warp) that provide the response callback. Application code should not call this directly.

Equations

• Network.Wai.ResponseReceived.done = { }

@[reducible, inline]

abbrev Network.Wai.StreamingBody : Type

Body streaming callback type. $$\text{StreamingBody} = (\text{ByteArray} \to \text{IO}()) \to \text{IO}() \to \text{IO}()$$

Equations

• Network.Wai.StreamingBody = ((ByteArray → IO Unit) → IO Unit → IO Unit)

inductive Network.Wai.RequestBodyLength : Type

The size of the request body. In the case of chunked transfer encoding, the size is unknown. $$\text{RequestBodyLength} = \text{ChunkedBody} \mid \text{KnownLength}\ \mathbb{N}$$ @since 1.4.0

• chunkedBody : RequestBodyLength

  Chunked transfer encoding — size unknown.

• knownLength (bytes : Nat) : RequestBodyLength

  Content-Length header present — size known. $$\text{KnownLength}\ n,\; n : \mathbb{N}$$

def Network.Wai.instBEqRequestBodyLength.beq : RequestBodyLength → RequestBodyLength → Bool

Equations

• Network.Wai.instBEqRequestBodyLength.beq Network.Wai.RequestBodyLength.chunkedBody Network.Wai.RequestBodyLength.chunkedBody = true
• Network.Wai.instBEqRequestBodyLength.beq (Network.Wai.RequestBodyLength.knownLength a) (Network.Wai.RequestBodyLength.knownLength b) = (a == b)
• Network.Wai.instBEqRequestBodyLength.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Network.Wai.instBEqRequestBodyLength : BEq RequestBodyLength

Equations

• Network.Wai.instBEqRequestBodyLength = { beq := Network.Wai.instBEqRequestBodyLength.beq }

@[implicit_reducible]

instance Network.Wai.instReprRequestBodyLength : Repr RequestBodyLength

Equations

• Network.Wai.instReprRequestBodyLength = { reprPrec := Network.Wai.instReprRequestBodyLength.repr }

def Network.Wai.instReprRequestBodyLength.repr : RequestBodyLength → Nat → Std.Format

Equations

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

structure Network.Wai.Request : Type

An HTTP request with all parsed information. $$\text{Request} = \{ \text{method}, \text{version}, \text{path}, \text{query}, \text{headers}, \ldots \}$$

• requestMethod : HTTP.Types.Method

  The HTTP method (GET, POST, etc.).

• httpVersion : HTTP.Types.HttpVersion

  The HTTP version.

• rawPathInfo : String

  The raw path info (e.g., "/foo/bar"). Middlewares should not modify this — modify pathInfo instead.

• rawQueryString : String

  The raw query string (e.g., "?key=val"), including leading '?'. Do not modify this raw value — modify queryString instead.

• requestHeaders : HTTP.Types.RequestHeaders

  The request headers.

• isSecure : Bool

  Whether the current connection is secure (HTTPS/TLS). Note: does not reflect whether the original client connection was secure (e.g., behind a reverse proxy). Use Network.Wai.Request.appearsSecure for a more complete check.

• remoteHost : Socket.SockAddr

  The remote client address.

• pathInfo : List String

  Parsed path segments (e.g., ["foo", "bar"]).

• queryString : HTTP.Types.Query

  Parsed query string.

• requestBody : IO ByteArray

  IO action to read the next chunk of the request body. Returns empty ByteArray when body is exhausted. Each call consumes a chunk — this is not idempotent.

• vault : Data.Vault

  Per-request extensible storage.

• requestBodyLength : RequestBodyLength

  The size of the request body — chunked or known length. @since 1.4.0

• requestHeaderHost : Option String

  The Host header value. @since 2.0.0

• requestHeaderRange : Option String

  The Range header value. @since 2.0.0

• requestHeaderReferer : Option String

  The Referer header value. @since 3.2.0

• requestHeaderUserAgent : Option String

  The User-Agent header value. @since 3.2.0

inductive Network.Wai.Response : Type

An HTTP response.

• responseFile (status : HTTP.Types.Status) (headers : HTTP.Types.ResponseHeaders) (path : String) (part : Option Sendfile.FilePart) : Response

  Respond with a file.

• responseBuilder (status : HTTP.Types.Status) (headers : HTTP.Types.ResponseHeaders) (body : ByteArray) : Response

  Respond with a ByteArray body (built in memory).

• responseStream (status : HTTP.Types.Status) (headers : HTTP.Types.ResponseHeaders) (body : StreamingBody) : Response

  Respond with a streaming body.

• responseRaw (rawAction : IO ByteArray → (ByteArray → IO Unit) → IO Unit) (fallback : Response) : Response

  Respond with raw data sent directly to the socket.

def Network.Wai.Response.status : Response → HTTP.Types.Status

Get the status from a response.

Equations

• (Network.Wai.Response.responseFile s headers path part).status = s
• (Network.Wai.Response.responseBuilder s headers body).status = s
• (Network.Wai.Response.responseStream s headers body).status = s
• (Network.Wai.Response.responseRaw rawAction fb).status = fb.status

def Network.Wai.Response.headers : Response → HTTP.Types.ResponseHeaders

Get the headers from a response.

Equations

• (Network.Wai.Response.responseFile s headers path part).headers = headers
• (Network.Wai.Response.responseBuilder s headers body).headers = headers
• (Network.Wai.Response.responseStream s headers body).headers = headers
• (Network.Wai.Response.responseRaw rawAction fb).headers = fb.headers

def Network.Wai.Response.mapResponseHeaders (f : HTTP.Types.ResponseHeaders → HTTP.Types.ResponseHeaders) : Response → Response

Map over the response headers.

Equations

• Network.Wai.Response.mapResponseHeaders f (Network.Wai.Response.responseFile s headers path part) = Network.Wai.Response.responseFile s (f headers) path part
• Network.Wai.Response.mapResponseHeaders f (Network.Wai.Response.responseBuilder s headers body) = Network.Wai.Response.responseBuilder s (f headers) body
• Network.Wai.Response.mapResponseHeaders f (Network.Wai.Response.responseStream s headers body) = Network.Wai.Response.responseStream s (f headers) body
• Network.Wai.Response.mapResponseHeaders f (Network.Wai.Response.responseRaw rawAction fb) = Network.Wai.Response.responseRaw rawAction (Network.Wai.Response.mapResponseHeaders f fb)

def Network.Wai.Response.mapResponseStatus (f : HTTP.Types.Status → HTTP.Types.Status) : Response → Response

Map over the response status.

Equations

• Network.Wai.Response.mapResponseStatus f (Network.Wai.Response.responseFile s headers path part) = Network.Wai.Response.responseFile (f s) headers path part
• Network.Wai.Response.mapResponseStatus f (Network.Wai.Response.responseBuilder s headers body) = Network.Wai.Response.responseBuilder (f s) headers body
• Network.Wai.Response.mapResponseStatus f (Network.Wai.Response.responseStream s headers body) = Network.Wai.Response.responseStream (f s) headers body
• Network.Wai.Response.mapResponseStatus f (Network.Wai.Response.responseRaw rawAction fb) = Network.Wai.Response.responseRaw rawAction (Network.Wai.Response.mapResponseStatus f fb)

def Network.Wai.Response.bodyIsEmpty : Response → Bool

Whether a response has an empty body. Used for RFC 9110 §6.4.1 compliance checks. Files and streams are conservatively assumed non-empty; raw responses are opaque.

Equations

• (Network.Wai.Response.responseBuilder status headers body).bodyIsEmpty = body.isEmpty
• (Network.Wai.Response.responseFile status headers path part).bodyIsEmpty = false
• (Network.Wai.Response.responseStream status headers body).bodyIsEmpty = false
• (Network.Wai.Response.responseRaw rawAction fallback).bodyIsEmpty = false

theorem Network.Wai.Response.status_responseBuilder (s : HTTP.Types.Status) (h : HTTP.Types.ResponseHeaders) (b : ByteArray) : (responseBuilder s h b).status = s

Status accessor returns the status of a builder response.

theorem Network.Wai.Response.status_responseFile (s : HTTP.Types.Status) (h : HTTP.Types.ResponseHeaders) (p : String) (fp : Option Sendfile.FilePart) : (responseFile s h p fp).status = s

Status accessor returns the status of a file response.

theorem Network.Wai.Response.status_responseStream (s : HTTP.Types.Status) (h : HTTP.Types.ResponseHeaders) (b : StreamingBody) : (responseStream s h b).status = s

Status accessor returns the status of a stream response.

theorem Network.Wai.Response.headers_responseBuilder (s : HTTP.Types.Status) (h : HTTP.Types.ResponseHeaders) (b : ByteArray) : (responseBuilder s h b).headers = h

Headers accessor returns the headers of a builder response.

theorem Network.Wai.Response.headers_responseFile (s : HTTP.Types.Status) (h : HTTP.Types.ResponseHeaders) (p : String) (fp : Option Sendfile.FilePart) : (responseFile s h p fp).headers = h

Headers accessor returns the headers of a file response.

theorem Network.Wai.Response.mapResponseHeaders_id_responseBuilder (s : HTTP.Types.Status) (h : HTTP.Types.ResponseHeaders) (b : ByteArray) : mapResponseHeaders id (responseBuilder s h b) = responseBuilder s h b

mapResponseHeaders id is identity for builder responses.

theorem Network.Wai.Response.mapResponseHeaders_id_responseFile (s : HTTP.Types.Status) (h : HTTP.Types.ResponseHeaders) (p : String) (fp : Option Sendfile.FilePart) : mapResponseHeaders id (responseFile s h p fp) = responseFile s h p fp

mapResponseHeaders id is identity for file responses.

theorem Network.Wai.Response.mapResponseHeaders_id_responseStream (s : HTTP.Types.Status) (h : HTTP.Types.ResponseHeaders) (b : StreamingBody) : mapResponseHeaders id (responseStream s h b) = responseStream s h b

mapResponseHeaders id is identity for stream responses.

theorem Network.Wai.Response.mapResponseStatus_id_responseBuilder (s : HTTP.Types.Status) (h : HTTP.Types.ResponseHeaders) (b : ByteArray) : mapResponseStatus id (responseBuilder s h b) = responseBuilder s h b

mapResponseStatus id is identity for builder responses.

theorem Network.Wai.Response.mapResponseStatus_id_responseFile (s : HTTP.Types.Status) (h : HTTP.Types.ResponseHeaders) (p : String) (fp : Option Sendfile.FilePart) : mapResponseStatus id (responseFile s h p fp) = responseFile s h p fp

mapResponseStatus id is identity for file responses.

theorem Network.Wai.Response.mapResponseStatus_id_responseStream (s : HTTP.Types.Status) (h : HTTP.Types.ResponseHeaders) (b : StreamingBody) : mapResponseStatus id (responseStream s h b) = responseStream s h b

mapResponseStatus id is identity for stream responses.

inductive Network.Wai.ResponseState : Type

Response lifecycle state for the indexed AppM monad.

This two-element type is the key to compile-time exactly-once enforcement. The AppM monad is parameterised by a pre-state and a post-state drawn from ResponseState. Since .pending ≠ .sent (proven below), the compiler can distinguish "haven't responded yet" from "already responded" and reject any code path that would respond twice or not at all. $$\text{ResponseState} = \text{pending} \mid \text{sent}$$

• pending : ResponseState

  No response has been sent yet.

• sent : ResponseState

  A response has been sent.

def Network.Wai.instBEqResponseState.beq : ResponseState → ResponseState → Bool

Equations

• Network.Wai.instBEqResponseState.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Network.Wai.instBEqResponseState : BEq ResponseState

Equations

• Network.Wai.instBEqResponseState = { beq := Network.Wai.instBEqResponseState.beq }

@[implicit_reducible]

instance Network.Wai.instDecidableEqResponseState : DecidableEq ResponseState

Equations

• Network.Wai.instDecidableEqResponseState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Network.Wai.instReprResponseState : Repr ResponseState

Equations

• Network.Wai.instReprResponseState = { reprPrec := Network.Wai.instReprResponseState.repr }

def Network.Wai.instReprResponseState.repr : ResponseState → Nat → Std.Format

Equations

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

theorem Network.Wai.ResponseState.pending_ne_sent : pending ≠ sent

Response states are distinct.

structure Network.Wai.AppM (pre post : ResponseState) (α : Type) : Type

Indexed Green monad tracking response lifecycle state transitions.

This is the core dependent-type mechanism that enforces the WAI exactly-once-response contract at compile time.

AppM pre post α represents a Green computation that transitions the response lifecycle from state pre to state post. The state indices are checked by the Lean 4 kernel during type-checking and erased at runtime -- AppM compiles to exactly the same code as plain Green.

Why private mk? The constructor is private, so the only ways to build an AppM value are through the provided combinators: respond, respondIO, liftIO, ipure, ibind, ioThen. Application code cannot fabricate AppM .pending .sent without actually invoking the response callback -- the type system forces the real work.

Why double-respond is impossible:

• AppM.respond has type AppM .pending .sent ResponseReceived.
• After one call the state is .sent.
• AppM.ibind chains: AppM s₁ s₂ α → (α → AppM s₂ s₃ β) → AppM s₁ s₃ β.
• A second respond would require AppM .sent _ _ with pre-state .sent, but respond's pre-state is .pending -- type mismatch, compile-time error.

Trust boundary: Server code (Warp) extracts the Green via .run at the edge. Middleware that needs full control can use the protected escape hatch AppM.unsafeLift, which requires an explicit open.

$$\text{AppM}\ s_1\ s_2\ \alpha = \text{Green}(\alpha) \text{ (opaque, indexed by state)}$$

• run : Control.Concurrent.Green.Green α

  Extract the underlying Green computation. For server/framework code only.

@[inline]

def Network.Wai.AppM.ipure {α : Type} {s : ResponseState} (a : α) : AppM s s α

Lift a pure value without changing state. $$\text{ipure} : \alpha \to \text{AppM}\ s\ s\ \alpha$$

Equations

• Network.Wai.AppM.ipure a = { run := pure a }

@[inline]

def Network.Wai.AppM.liftIO {α : Type} {s : ResponseState} (action : IO α) : AppM s s α

Lift a plain IO action without changing state. IO is automatically lifted into Green via MonadLift IO Green. $$\text{liftIO} : \text{IO}(\alpha) \to \text{AppM}\ s\ s\ \alpha$$

Equations

• Network.Wai.AppM.liftIO action = { run := liftM action }

@[inline]

def Network.Wai.AppM.ibind {s₁ s₂ : ResponseState} {α : Type} {s₃ : ResponseState} {β : Type} (ma : AppM s₁ s₂ α) (f : α → AppM s₂ s₃ β) : AppM s₁ s₃ β

Indexed bind: chains state transitions. $$\text{ibind} : \text{AppM}\ s_1\ s_2\ \alpha \to (\alpha \to \text{AppM}\ s_2\ s_3\ \beta) \to \text{AppM}\ s_1\ s_3\ \beta$$

Equations

• ma.ibind f = { run := do let a ← ma.run (f a).run }

@[inline]

def Network.Wai.AppM.respond (callback : Response → Control.Concurrent.Green.Green ResponseReceived) (resp : Response) : AppM ResponseState.pending ResponseState.sent ResponseReceived

Send a response, transitioning from .pending to .sent. This is the only way to produce AppM .pending .sent ResponseReceived. The callback returns Green ResponseReceived — all response sending happens on the non-blocking Green monad. $$\text{respond} : (\text{Response} \to \text{Green}\ \text{ResponseReceived}) \to \text{Response} \to \text{AppM}\ \texttt{.pending}\ \texttt{.sent}\ \text{ResponseReceived}$$

Equations

• Network.Wai.AppM.respond callback resp = { run := callback resp }

@[inline]

def Network.Wai.AppM.respondIO (callback : Response → Control.Concurrent.Green.Green ResponseReceived) (action : IO Response) : AppM ResponseState.pending ResponseState.sent ResponseReceived

Perform IO then respond with the computed Response. Convenient for the common pattern of "compute a response, then send it." Uses do notation naturally inside the IO Response block. $$\text{respondIO} : (\text{Response} \to \text{Green}\ \text{ResponseReceived}) \to \text{IO}(\text{Response}) \to \text{AppM}\ \texttt{.pending}\ \texttt{.sent}\ \text{ResponseReceived}$$

Equations

• Network.Wai.AppM.respondIO callback action = { run := liftM action >>= callback }

@[inline]

def Network.Wai.AppM.ioThen {α : Type} {s₁ s₂ : ResponseState} {β : Type} (action : IO α) (f : α → AppM s₁ s₂ β) : AppM s₁ s₂ β

Perform an IO action then continue with a state-changing computation. Useful for middleware that needs IO before deciding whether to delegate or respond. $$\text{ioThen} : \text{IO}(\alpha) \to (\alpha \to \text{AppM}\ s_1\ s_2\ \beta) \to \text{AppM}\ s_1\ s_2\ \beta$$

Equations

• Network.Wai.AppM.ioThen action f = { run := do let a ← liftM action (f a).run }

def Network.Wai.AppM.unsafeLift {α : Type} {pre post : ResponseState} (action : IO α) : AppM pre post α

Escape hatch for framework/middleware code that needs full IO control over state transitions. Not for application code. The caller is responsible for ensuring exactly-once response semantics. $$\text{unsafeLift} : \text{IO}(\alpha) \to \text{AppM}\ s_1\ s_2\ \alpha$$

Equations

• Network.Wai.AppM.unsafeLift action = { run := liftM action }

@[implicit_reducible]

instance Network.Wai.instMonadAppM {s : ResponseState} : Monad (AppM s s)

AppM s s is a standard Monad (for non-state-changing operations). Enables do notation inside AppM.respondIO or AppM.ioThen blocks.

Equations

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

@[implicit_reducible]

instance Network.Wai.instMonadLiftTIOAppM {s : ResponseState} : MonadLiftT IO (AppM s s)

IO actions lift into AppM s s automatically (via IO → Green → AppM).

Equations

• Network.Wai.instMonadLiftTIOAppM = { monadLift := fun {α : Type} => Network.Wai.AppM.liftIO }

@[reducible, inline]

abbrev Network.Wai.Application : Type

A WAI application. $$\text{Application} = \text{Request} \to (\text{Response} \to \text{Green}(\text{ResponseReceived})) \to \text{AppM}\ \texttt{.pending}\ \texttt{.sent}\ \text{ResponseReceived}$$

The return type AppM .pending .sent ResponseReceived is the key dependent-type innovation over Haskell's WAI. It encodes three compile-time guarantees simultaneously:

1. Response was sent (post-state is .sent, not .pending).
2. Response was sent exactly once (no path from .sent back to .pending; no second respond accepted after .sent).
3. Response was sent through the callback (private mk prevents fabricating the AppM value without calling respond).

Server implementations (Warp) extract the underlying Green via .run at the trust boundary. Application code never touches .run.

The callback takes Response → Green ResponseReceived — all response sending happens on the non-blocking Green monad, freeing pool threads while awaiting socket I/O.

Equations

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

@[reducible, inline]

abbrev Network.Wai.Middleware : Type

A WAI middleware transforms an application. $$\text{Middleware} = \text{Application} \to \text{Application}$$

Equations

• Network.Wai.Middleware = (Network.Wai.Application → Network.Wai.Application)