typednoteslinen0.18.0

Lean Standard Library

LINEN

A curated standard-library companion for Lean 4 — external concepts ported in, with everything Lean already provides stripped out.

CI GitHub Stars License Last Commit Lean 4

770 modules · 468 compile-time theorems · 10882 #guard checks

Overview

linen is a small, opinionated extension of the Lean 4 standard library. When a useful concept exists in another ecosystem (a Haskell package, another Lean project, a single module), it is ported in — but every concept that already has a Lean standard-library equivalent is replaced with that equivalent, and the result is reshaped to follow Lean's own module hierarchy and naming. What ships is only what core genuinely lacks, written as idiomatic Lean on top of the standard library.

Three rules hold across the whole library:

  • Stdlib-first — no bespoke re-implementation of anything core provides (e.g. Id over a hand-rolled identity functor, · >=> · over a custom Kleisli combinator, List.foldlM over foldM).
  • No partial, no sorry — all recursion is structural or has a proven termination argument, and proofs are complete.
  • Everything is tested — each module has a Tests/ counterpart whose #guard examples run on every build.

Features

linen covers the following areas — see docs/modules.md for the full per-module feature list and module table.

  • Data.Functor / Control — functor, applicative & monad constructions missing from core (Compose/Product/FunctorSum, Bifunctor, Foldable/Traversable, mtl-style Reader/State/Except, STM, green-thread concurrency, …).

  • Control.Monad.Effect — extensible effects ported from freer-simple: an open union over an effect row (Data.OpenUnion), the Eff monad with send/interpret/interpose/reinterpret/run, and the Reader/State/Error/Writer/NonDet/Coroutine/Fresh/Trace effects — so a signature is an effect whitelist. Its FileSystem, HTTP and PostgreSQL effects go past what Haskell's rows can say, indexing the effect on a Capability value and so constraining an effect's arguments, not just which effects are named:

    • FileSystem — a read-only capability makes writeFile fail to elaborate, read/write/delete are separately grantable within one effect, and each path Scope carries its own operation list, so one capability says "read, write and delete under /srv/app/releases, read only under /etc/app, nothing anywhere else". Roots are matched component-wise, so /tmp/sandbox-evil is rejected where a string prefix would wrongly admit it. Scopes union — no deny rules, no precedence — so Capability.union provably takes nothing away (permits_union_left/_right).
    • HTTP — methods are separately grantable, and each URL scope carries its own method list, so one capability says "GET anywhere under u!"https://api.example.com/v1", POST only to /v1/events". Hosts are compared as DNS labels and paths component-wise, so api.example.com.evil.com, a scheme downgrade, a changed port and /v1-admin are all rejected.
    • PostgreSQL — the database, instance and role are capability fields the handler builds its connection from, so no computation can reach another; statement kinds and tables are separately grantable. Queries are a parameterised AST rather than strings, because a String of SQL cannot be checked by decide — and so the SQL sent cannot disagree with the SQL authorised.

  • Control.Lens — a lens-style profunctor-optics library (plus its profunctors/indexed-traversable prerequisites): Lens/Prism/Iso/ Traversal/Fold/Getter/Setter/Review and indexed variants, with Ixed/At/Each/Cons/Snoc/Wrapped instances over most existing containers; makeLenses-generated accessors are hand-written per field instead, since Lean has no Template Haskell.

  • Data.ByteString* / Data.String / Data.Word8 — byte strings (strict, lazy, short, builder), Base64, Base16 (Data.Hex), case-insensitive text, and ASCII byte classification.

  • Data.Json — a tiny JSON library with ToJSON/FromJSON and proven encode→decode round trips.

  • Data.Float — parseFloat? from text, shared by the JSON decoder, the YAML reader and the SQL decoders; Lean core has no String.toFloat?.

  • Data.Ini / Data.Yaml — configuration formats: INI sections and pairs, and YAML 1.2's core schema (block and flow collections, block scalars, multi-document streams). Anchors, aliases, merge keys and custom tags are rejected outright rather than silently mis-parsed.

  • Data.Map / Data.Set / Data.IntMap / Data.List' / Data.List.NonEmpty / … — Haskell-style container and list APIs over core Std/List types.

  • Time — a time-style calendar/clock layer over Lean's own Std.Time: Julian-calendar conversion, Gregorian/Orthodox Easter dates, absolute Month/Quarter counters, (months, days)/(months, Duration) calendar periods, UT1 mean-solar-time conversion, and TAI↔UTC leap-second conversion — the pieces Std.Time itself doesn't cover; Data.Time.*'s day/UTC-instant/time-of-day types are Std.Time.Date.PlainDate/ Std.Time.Duration/Std.Time.Zoned underneath.

  • Network.HTTP / HTTP2 / HTTP3 / Socket / TLS / QUIC / WebSockets — a full network stack: HTTP/1.1 client & wire types, HTTP/2 framing + HPACK, HTTP/3 over QUIC + QPACK, POSIX sockets with a green-thread event dispatcher, TLS 1.2/1.3 over OpenSSL, and WebSockets.

  • Network.WebApp / Network.WebApp.Server — a WAI-style application interface plus an HTTP server implementing it.

  • Web.Html / Web.Css — typed HTML5/CSS construction where illegal nesting and property/value mismatches are compile-time errors, with elem! and rule! macro sugar.

  • DataFrame — typed tabular data with a proven rectangular invariant, CSV I/O, joins, sorting, grouping/aggregation, and statistics.

  • Database.PostgreSQL / Database.SQL — libpq FFI bindings and a hasql-style typed client (encoders/decoders, sessions, pooling).

  • Database.SQLite3 — direct-sqlite-style FFI bindings to a vendored SQLite amalgamation (no pkg-config), with an Except Error-returning Direct layer and a public IO-throwing API.

  • Database.SQLite.Simple — a sqlite-simple-style mid-level client: Query/Only/row-cons types, the error-accumulating Ok applicative, SQLite date/time text parsing & rendering, Connection/Statement/Field connection plumbing, and the ToField/FromField/ToRow/FromRow parameter/row conversion classes (tuple instances up to arity 7); a public facade (withConnection, query/query_/execute/execute_, streaming fold/fold_, withTransaction/withSavepoint, lastInsertRowId/changes); the sql "…" syntax/macro_rules quasiquoter substitute; and user-defined scalar SQL function registration (createFunction0–createFunction3/deleteFunction) via a new Lean-closure-called-from-C sqlite3_create_function_v2 bridge.

  • Database.DuckDB.FFI — low-level duckdb-ffi-style FFI bindings to libduckdb: connection/query lifecycle, prepared statements & the appender, DataChunk/Vector/validity-mask access to result data, the logical-type system (primitive/LIST/ARRAY/MAP/STRUCT/UNION/ ENUM/DECIMAL), catalog/config/error/logging helpers, and user-defined scalar SQL function registration via a Lean-closure-called-from-C trampoline (mirroring the one built for Database.SQLite.Simple).

  • Database.DuckDB.Simple — a duckdb-simple-style mid-level client atop Database.DuckDB.FFI: the error-accumulating Ok applicative, Query/ Only/row-cons types, the ToField/FromField/ToRow/FromRow parameter/row conversion classes (tuple instances up to arity 7) including DuckDB's STRUCT/UNION/LIST/MAP/ENUM/DECIMAL logical-type decode support and hand-written STRUCT/UNION decode combinators standing in for GHC-generics-derived instances; catalog/config/file-system/logging helpers and user-defined scalar SQL function registration; and a public facade (withConnection, query/query_/execute/execute_, streaming fold/fold_, withTransaction) built on the appender-free prepared-statement/DataChunk fetch pipeline. Completes the sqlite-simple → duckdb-ffi → duckdb-simple import chain.

  • Database.Redis — a hedis-style Redis client: the RESP2 wire protocol (Reply encoder/parser over Std.Internal.Parsec.ByteArray) and request/response pipelining over Network.Socket/Network.TLS; the Redis monad with RedisCtx/MonadRedis; the full command surface (simple + irregular ManualCommands); ConnectInfo/redis://-URL parsing and an IO.Ref-guarded connection pool; MULTI/EXEC/WATCH transactions; Pub/Sub (publish, pubSub, pubSubForever); Redis Cluster (CRC16 hash slots, topology, MOVED/ASK redirects); and Sentinel-based master discovery with failover — no separate prerequisite Hackage package needed, every dependency resolving onto the Lean stdlib, an existing linen port, or a small inlined slice.

  • Data.Stream — a streamly-core-style stream-fusion library: the fused, direct-style Stream (a Yield/Skip/Stop Step-machine stepper) and the CPS-encoded StreamK, bridged both ways; Fold/Scanl terminating left folds and scans, Unfold/Producer generators, and a backtracking streaming Parser; plus an unboxed-array subsystem (MutByteArray/Unbox, MutArray, Array.Unboxed). A distinct streaming paradigm from the existing Conduit port — the fused data encoding is reproduced faithfully, without GHC's fusion-plugin optimizer that eager Lean has no analogue for; bounded to streamly-core, deferring the concurrent SVar scheduler.

  • Text.DocLayout — a Wadler/Leijen-style pretty-printer: the Doc document algebra (literal, <+>, $$, vcat, nest, hang, flush, side-by-side blocks, ANSI/OSC-8 styling) and its render/renderANSI line- wrapping engine, plus the HasChars/Attributed/ANSIFont layers beneath it. linen's first document-layout algebra, and a blocking prerequisite of pandoc — every pandoc writer renders through it.

  • Text.Pandoc — a pandoc-style universal document converter: the shared AST (Pandoc/Block/Inline, folded in from pandoc-types) with its Walk/Generic traversals and Builder combinator API; the shared reader/writer infrastructure (Extensions, Options, Parsing, Shared, Templates, Writers.Shared's gridTable) and the pure PandocMonad/PandocPure; and a working Markdown↔AST↔HTML round-trip (Readers/Writers.{Markdown,HTML}) plus the AST-native Native/JSON formats, dispatched through a top-level getReader/getWriter/convert facade. tagsoup (the HTML tokenizer) and a YAML front-matter parser had no other consumer, so each is folded in as a bounded slice directly inside its one reader module rather than imported as its own package; blaze-html substitutes onto the existing Web.Html. Scoped to the AST plus Markdown and HTML (both directions) — the long tail of exotic formats, binary/zip formats, the Lua-filter system, syntax highlighting, math typesetting, citations, and templating are all deferred.

  • Crypto.JOSE — JOSE/JWT signing and verification (HMAC/RSA/EC) over OpenSSL.

  • Crypto.SigV4 — AWS Signature Version 4 request signing, over the existing SHA-256/HMAC FFI and RFC 3986 escaping; checked against AWS's published test vectors, so it also serves S3-compatible clouds.

  • Text.XML — an XML reader (the counterpart to Text.Pandoc.XML's escaping): a character-at-a-time state machine feeding a stack-based tree builder, so nesting needs no partial and no fuel.

  • Network.HTTP.Client.Retry — capped exponential backoff with equal jitter over connection errors and 408/429/5xx, honouring Retry-After. Alongside it, socket read/write deadlines (SO_RCVTIMEO/SO_SNDTIMEO plus poll-based waiting) now bound every request: the blocking wrappers used to retry EAGAIN in a hot loop, so a stalled peer meant an indefinite hang at 100% CPU.

  • Network.OAuth2 — a hoauth2-style OAuth2 client: authorization-code, client-credentials, device-authorization, JWT-bearer, resource-owner-password and refresh-token grants; PKCE (S256) via two new OpenSSL-backed Crypto.SHA256/Crypto.SecureRandom FFI primitives; typed request-builder application config; and token/user-info/device-authorization HTTP flows over Network.HTTP.Client.Conduit.

  • Crypto.Zlib / Crypto.MD5 / Crypto.RC4 / Crypto.AES — zlib inflate, RFC 1321 MD5, the RC4 stream cipher, and AES-128 CBC decryption

    • PKCS5 unpadding — the primitives behind the PDF Standard Security Handler.

  • System.Keychain — OS credential-store access (macOS Keychain, Linux Secret Service, Windows Credential Manager).

  • Data.PDF.Stream / Data.PDF.Core / Data.PDF.Content / Data.PDF.Document — PDF parsing, rendering, and text extraction: a buffer-resident io-streams port, the low-level object model/parser/ xref/encryption layer, content-stream operators and font/text-encoding handling, and a document/page-tree API with text extraction.

  • Options.Applicative — optparse-applicative-style command-line argument parsing.

  • PostgREST — a Lean port of PostgREST's request/response pipeline: API request parsing, config, schema cache introspection, query planning, auth, and OpenAPI generation.

  • CDP — a Chrome DevTools Protocol client: typed commands/events/types for every protocol domain, plus a WebSocket-based runtime to connect to a browser, send commands, and subscribe to events.

  • Data.Colour — a colour-style colour library: Colour/AlphaColour blending, CIE chromaticity/illuminants, RGB colour spaces (HSL/HSV, sRGB), and named SVG colours.

  • Data.Array.Shaped — a repa-style rank-polymorphic, shape-indexed array library: Delayed/Manifest/Cursored/Partitioned/Undefined representations, index-space operators, and stencil-based convolution.

  • System.Console.Ansi / System.Exit / System.Log.FastLogger — terminal styling, process exit codes, and buffered logging.

  • Graphics.Netpbm — a netpbm-style parser for the PBM/PGM/PPM "portable anymap" image formats (ASCII and binary variants, magic numbers P1–P6) over ByteArray.

  • Codec.Picture — a JuicyPixels-style image codec suite: pixel/image types and colorspace conversions, plus PNG, JPEG (baseline + progressive), GIF (including animation), BMP, TGA, TIFF, and Radiance HDR encoders/ decoders, Exif/TIFF/JFIF metadata, and median-cut colour quantization.

  • Graphics.Image — a hip-style image-processing library: Y/RGB/ HSI/CMYK/YCbCr/complex/binary colour spaces over a shape-indexed pixel array; geometric transforms (rotate/scale/translate/crop) with nearest-neighbour/bilinear interpolation; kernel convolution and named filters (Sobel, Gaussian, Laplacian, …); binary morphology (erode/dilate/ open/close); FFT-based complex-image processing; adaptive histogram equalization; Hough-transform line detection; salt-and-pepper noise generation; and PNG/JPEG/GIF/BMP/TGA/TIFF/HDR and PNM/PGM/PPM file I/O via Codec.Picture/Graphics.Netpbm.

  • Cloud — one way to use cloud services across AWS, GCP and Scaleway: object stores, message queues and secret managers behind three portable interfaces, each a record of closures with one implementation per cloud. Scaleway's Object Storage and Queues speak the S3 and SQS APIs, so a single client serves two clouds and differs only in the endpoint; Cloud Storage gets its own JSON client, and Pub/Sub — a topic-and-subscription system rather than a queue — splits into a Producer and a Consumer so nothing has to pretend otherwise. Underneath: the three-source credential chain (CLI config files, OS keychain, environment), RFC 7523 token minting for GCP, locality-to-region tables, request signing over Crypto.SigV4, the four wire dialects, a classified error taxonomy, and pagination that reports whether it finished. Every interface has an in-memory backend and the transport is swappable, so all of it is tested with no credentials and no network.

  • Control.Monad.Effect.{ObjectStore,Queue,SecretStore} — the same three services as capability-restricted effects, on the Effect.FileSystem pattern. A capability is a value indexing the effect, so it can confine a program to one bucket's key prefix, let a worker read one queue and write another without draining either, or grant a health check the right to see that a secret exists while making getValue fail to elaborate. The handler takes the backend as a parameter, so one program runs against S3, against Cloud Storage, or against an in-memory double.

Quick Start

Add to your lakefile.toml:

[[require]]
name = "linen"
git = "https://github.com/typednotes/linen"
rev = "main"

Then import what you need:

import Linen.Data.Functor
import Linen.Control.Monad

open Data.Functor Control.Monad

#eval join (some (some 3))            -- some 3
#eval replicateM 3 (some 7)           -- some [7, 7, 7]

Using the FFI-backed modules

Pure modules need nothing beyond the require above. The modules backed by native code — System.Keychain, Crypto.*, Network.TLS, Network.HTTP (over HTTPS), Database.* — need link flags in your lakefile.

Lake does not propagate a dependency's moreLinkArgs to a dependent's executable: liblinenffi.a lands on your link line, but the flags its members need do not, so you get undefined symbol: SecItemCopyMatching or similar. Because the flags are platform-conditional, this needs lakefile.lean rather than lakefile.toml. Take only the lines for the features you use:

import Lake
open System Lake DSL

def pkgConfigFlags (args : Array String) : IO (Array String) := do
  try
    let out ← IO.Process.output { cmd := "pkg-config", args }
    if out.exitCode != 0 then return #[]
    return (out.stdout.trimAscii.copy.splitOn " ").toArray.map (·.trimAscii.copy)
      |>.filter (· != "")
  catch _ => return #[]

def pkgLinkFlags (pkg : String) : IO (Array String) := do
  let libs ← pkgConfigFlags #["--libs", pkg]
  let libdir ← pkgConfigFlags #["--variable=libdir", pkg]
  return (libdir.filter (· != "")).map ("-L" ++ ·) ++ libs

/-- Lean ships its own `lld`, which has no default framework search path. -/
def macSdkArgs : IO (Array String) := do
  try
    let out ← IO.Process.output { cmd := "xcrun", args := #["--show-sdk-path"] }
    if out.exitCode != 0 then return #[]
    let sdk := out.stdout.trimAscii.copy
    if sdk.isEmpty then return #[]
    return #["-F", sdk ++ "/System/Library/Frameworks", "-L", sdk ++ "/usr/lib"]
  catch _ => return #[]

open Lean Elab Command in
run_cmd do
  let mkDef (n : Name) (flags : Array String) : CommandElabM Unit := do
    let lits : Array (TSyntax `term) := flags.map (fun s => quote s)
    elabCommand (← `(def $(mkIdent n) : Array String := #[$lits,*]))
  -- `System.Keychain`
  let keychain : Array String ←
    if System.Platform.isOSX then
      (macSdkArgs).map (· ++ #["-framework", "Security", "-framework", "CoreFoundation"])
    else if System.Platform.isWindows then pure #["-ladvapi32", "-lcredui"]
    else pkgLinkFlags "libsecret-1"
  -- `Crypto.*` and `Network.TLS`. The explicit `-L` matters on macOS: without
  -- it these can bind to the system's incompatible `libboringssl`, which links
  -- cleanly and then crashes on the first TLS call.
  let ssl ← pkgLinkFlags "openssl"
  mkDef `nativeLinkArgs (keychain ++ ssl)

package myapp where
  moreLinkArgs := nativeLinkArgs

Add pkgLinkFlags "libpq" for Database.PostgreSQL, pkgLinkFlags "zlib" for Crypto.Zlib, and DuckDB's lib directory for Database.DuckDB.

Setting precompileModules := true on this package would make all of the above automatic, since Lake then links the extern library's shared form, which carries these flags. It is deliberately not the default: the shared form links the whole archive, so every dependent would need libpq, SQLite and DuckDB installed even to use, say, Crypto.SigV4.

Modules

See docs/modules.md for the full module table (all 770 modules).

Build & Test

lake build          # build the library
lake build Tests    # run every #guard / #eval check

Examples

Example programs live under Examples/ and share one entrypoint, lake exe examples <name> [args...] (run with no name to list them):

lake exe examples                  # list the available examples
lake exe examples echo             # green-threaded echo server — self-checking demo (exits 0)
lake exe examples echo serve 9099  # run the echo server forever; then:  nc 127.0.0.1 9099
lake exe examples bench            # network round-trips w/ a few-ms server delay: Green vs blocking pool (same #cores threads)
lake exe examples postgrest        # in-memory PostgREST request handling + OpenAPI spec generation — self-checking demo
lake exe examples quic             # QUIC types/config + HTTP/3 QPACK/frame wire round trip — self-checking demo
lake exe examples recv             # Network.Socket.Blocking accept/connect/send/recv round trip — self-checking demo
lake exe examples resourcet        # Control.Monad.Trans.Resource LIFO cleanup over real scratch files — self-checking demo
lake exe examples conduit          # Data.Conduit / Data.Conduit.Combinators pipelines, incl. bracketP/runConduitRes — self-checking demo
lake exe examples stm              # Control.Monad.STM + Concurrent.STM.{TVar,TMVar,TQueue} — self-checking demo
lake exe examples streaming-commons        # Data.Streaming.Network bindPortTCP/getSocketTCP/acceptSafe/AppData round trip — self-checking demo
lake exe examples streaming-commons serve 9098  # run it forever; then:  nc 127.0.0.1 9098
lake exe examples tls              # Network.TLS.Context handshake over loopback against a self-signed cert — self-checking demo
lake exe examples httpclient       # Network.HTTP.Client connect/request/response + redirect-following, over loopback — self-checking demo
lake exe examples httpconduit      # Network.HTTP.Client.Conduit / Network.HTTP.Simple streaming HTTP, over loopback — self-checking demo
lake exe examples req              # Network.HTTP.Req type-safe req/runReq (HttpBodyAllowed-checked GET/POST), over loopback — self-checking demo
lake exe examples webapp           # Network.WebApp: Application/Middleware/AppM (composeMiddleware/ifRequest/modifyResponse), over loopback — self-checking demo
lake exe examples webappstatic     # Network.WebApp.Static: staticApp/static + defaultFileServerSettings over a real scratch directory — self-checking demo
lake exe examples vault            # Data.Vault type-safe heterogeneous map: typed keys, adjust/delete/union — self-checking demo
lake exe examples vector           # Data.Vector-derived Array combinators: generate/ifilter/folds/reductions/backpermute/slice — self-checking demo
lake exe examples effects          # Control.Monad.Effect.{FileSystem,HTTP,PostgreSQL,Trace} capabilities over real files/socket/Postgres — self-checking demo
lake exe examples effects no-db    # same, minus the Podman-started PostgreSQL section
lake exe examples todo             # Web.Html/Web.Css typed TODO list over Network.WebApp.Server — self-checks, then keeps serving; try:  curl localhost:<port>
lake exe examples todo check       # same self-check round trip, but exits instead of staying up (for scripting)

The echo example exercises the whole socket stack end-to-end — a green accept loop forks a green handler per connection, each suspending on recvGreen/sendAllGreen (via the kqueue/epoll EventDispatcher) instead of holding an OS thread, so one small worker pool serves many connections. Adding an example is a new module under Examples/ plus one line in the registry in Examples/Main.lean.

The quic example demonstrates the HTTP/3-over-QUIC wire format end-to-end — Network.HTTP3.QPACK.Encode/Frame.encode producing bytes that Frame.decode/Network.HTTP3.QPACK.Decode reproduce exactly — without needing a live connection, since Network.QUIC.Client/Server are stubbed pending TLS 1.3 FFI. It also calls Client.connect/Server.run/Server.accept directly and checks that each fails with exactly its documented "not yet implemented" error, so the demo stays honest about what is and isn't wired up yet.

The stm example puts ten green tasks through a thousand atomically increments each of a shared TVar, hands values between a producer and consumer through an empty TMVar, checks TQueue's FIFO order survives its two-list representation, and shows orElse falling through to its alternative on retry.

The streaming-commons example drives Data.Streaming.Network's AppData abstraction over a real loopback connection; streaming-commons serve <port> runs runTCPServer forever for manual testing with nc.

The tls example runs a full TLS 1.2/1.3 handshake over loopback against a self-signed CN=localhost certificate, trusting it directly as its own CA via createClientContextWithCA so the demo stays fully offline. It also documents a real API limitation: getAlpn always reports none, because setAlpn only registers the server's selection callback — nothing in the current client API calls SSL_set_alpn_protos to advertise a protocol list for it to select from.

The httpclient and httpconduit examples each stand up a tiny hand-rolled HTTP/1.1 server over a real loopback socket and drive it with a different layer of the client stack: httpclient uses Client.connectPlain + Client.performRequest directly, then Client.execute to show a 302 Found → /final redirect followed automatically; httpconduit uses Simple.parseUrl!/httpBS, the callback-scoped Client.Conduit.withResponse, and Client.Conduit.httpSource streamed through a .| sinkList conduit pipeline.

The req example exercises Network.HTTP.Req's type-safe client — a GET with NoReqBody and a POST with a ReqBodyBs payload, both against a loopback server, both admitted by the HttpBodyAllowed typeclass at compile time (swapping a body onto the GET would instead fail to compile, since there is no HttpBodyAllowed .NoBody .YesBody instance).

The webapp example drives a Network.WebApp.Application through the same kind of hand-rolled loopback HTTP/1.1 server as httpclient/req, but this time the request handler itself is the thing under test: raw bytes are parsed into a Request, run through the application via Green.block, and the resulting Response serialized back. The demo application composes an echo handler with a /health route and a Server header, entirely from Middleware combinators — composeMiddleware, ifRequest, modifyResponse, addHeader — the same combinators the algebraic-law theorems in Network.WebApp (idMiddleware_comp_left/_right, modifyResponse_id, ifRequest_false) prove associative/identity laws for.

The webappstatic example serves a real scratch directory through Network.WebApp.Static.static (defaultFileServerSettings + staticApp), reusing webapp's loopback harness — including its Sendfile.sendFile path for .responseFile, since defaultFileServerSettings serves files that way rather than buffering them into a .responseBuilder. It checks a direct file hit (with its Cache-Control: max-age=3600 default), a directory request redirected to index.html, a 404 for a missing path, and a 403 for a dotfile-shaped path segment (rejected by Piece's no_dot invariant before any filesystem lookup runs).

The vault example mints distinctly-typed keys with Key.new and stores unrelated payloads under each in the same Vault, showing that a key only ever yields back the type it was minted for, plus adjust/delete/union.

The vector example runs through every combinator Linen.Data.Vector adds to Array (generate, ifilter, foldl1'/foldr1, ifoldl'/ifoldr, and/or/product, notElem, backpermute, slice) — everything else Haskell's Data.Vector offers already exists verbatim on Array.

The todo example is a small in-memory TODO list whose every page is built from Web.Html/Web.Css typed constructors — the <ul>/<li> nesting, each item's <form>s, and its inline style all go through the same illegal-construct-is-a-compile-error discipline as Tests.Linen.Web.HtmlTest/ CssTest (e.g. a <div> inside a <p>, or a color declaration given a Display value, simply fails to compile). Routing and state reuse Network.WebApp's Application/AppM, driven by the real Network.WebApp.Server engine via withApplication, exactly as the server example drives webapp's demoApplication. Unlike the other examples, todo doesn't exit after checking itself — it self-checks against its own live server and then keeps that same server (with its accumulated state) running on the printed OS-assigned port, so you can immediately curl it by hand; todo check runs the identical round trip but exits instead, for scripting.

The effects example is the capability-restricted effect modules (Control.Monad.Effect.{FileSystem,HTTP,PostgreSQL,Trace}) run against real resources, so that "authorised" and "actually happened" can be checked against each other: a capability rooted at a scratch directory reads and writes real files through IO.FS (and a second capability, same root plus the delete bit, removes them); a capability that may GET anything under /v1 but POST only to /v1/events drives a hand-rolled loopback HTTP/1.1 server; and a capability scoped to one table of one database, as one role, runs real INSERT/UPDATE/SELECT statements against a disposable postgres container the example starts with Podman itself. A second table exists in that same database and is provably unreachable through the capability, and CREATE TABLE is done with psql because the query AST has no DDL constructor and no rawSql escape hatch — so schema changes are outside the effect by construction. Every rejection the demo mentions is stated in the module as a theorem (webCap.permits .POST healthUrl ≠ true := by decide) rather than a comment, since a program that fails to compile cannot be run. The last two sections cover the runtime side: ScopedPath/ScopedUrl/ScopedQuery.check? for arguments only known at run time, and one Eff computation over a four-effect row — no IO in it — run by a single handler that dispatches each request to that effect's own interpreter. effects no-db skips the container sections; without a reachable podman they are reported as skipped rather than failed.

Running postgrest against a real database

lake exe examples postgrest (no args) and ... postgrest spec are fully self-contained — they run against a hand-built, in-memory SchemaCache and need no external services. postgrest live instead connects to a real PostgreSQL instance, introspects its public schema with the same catalog queries (SchemaCache.tablesSql/columnsSql) PostgREST itself runs at startup, and serves a couple of requests against the real tables.

Start a disposable local Postgres with Docker:

docker run --rm -e POSTGRES_PASSWORD=postgres -p 5432:5432 postgres

Then, in another terminal:

lake exe examples postgrest live

This connects with host=localhost port=5432 user=postgres password=postgres dbname=postgres — matching the container above — prints every table found in public, serves GET / and GET /<first table> through the same App.handleRequest code path as the in-memory demo, and prints the live schema's OpenAPI spec. Pass a different libpq connection string as the next argument to point at another instance or database, e.g.:

lake exe examples postgrest live "host=localhost port=5432 user=postgres password=postgres dbname=mydb"

If nothing is listening, the example prints a short "could not connect" hint (with this same docker run command) and exits 1, rather than crashing.

Documentation

  • docs/modules.md — the full module feature list and module table.
  • docs/imports/index.md — Hackage-package import order, with a per-package module dependency list under docs/imports/<Package>/dependencies.md.
  • docs/linking.md — how native libraries are linked: static vs dynamic, PIC, and the C++ exception/unwinder hazard on Linux. Read before adding an FFI dependency.
  • docs/rfcs.md — the specifications linen implements, mapped to their modules; the foundational ones it rests on; and a few worth reading for their own sake.
  • CHANGELOG.md — notable changes per released version.
  • AGENTS.md — conventions for contributing to the library.

License

See LICENSE for details.