diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,7 @@ +# Revision history for acolyte-core + +## 0.1.0.0 -- 2026-04-27 + +* Initial release. Pure type-level machinery for describing HTTP APIs as + types: endpoints, paths, methods, effects, session types, versioning, + and content negotiation. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,27 @@ +Copyright (c) 2024-2026, Josh Burgess + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +1. Redistributions of source code must retain the above copyright notice, + this list of conditions and the following disclaimer. + +2. Redistributions in binary form must reproduce the above copyright notice, + this list of conditions and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +3. Neither the name of the copyright holder nor the names of its + contributors may be used to endorse or promote products derived from this + software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" +AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE +ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE +LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR +CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF +SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS +INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN +CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) +ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE +POSSIBILITY OF SUCH DAMAGE. diff --git a/acolyte-core.cabal b/acolyte-core.cabal new file mode 100644 --- /dev/null +++ b/acolyte-core.cabal @@ -0,0 +1,110 @@ +cabal-version: 3.0 +name: acolyte-core +version: 0.1.0.0 +synopsis: Type-level API specification for acolyte +category: Web +description: + Pure type-level machinery for describing HTTP APIs as types. + Endpoints, paths, methods, effects, session types, versioning, + and content negotiation. No IO, no runtime beyond base. + +license: BSD-3-Clause +license-file: LICENSE +author: Josh Burgess +maintainer: Josh Burgess +homepage: https://github.com/joshburgess/acolyte +bug-reports: https://github.com/joshburgess/acolyte/issues +build-type: Simple + +extra-doc-files: + CHANGELOG.md + +flag dev-tests + description: + Build dev-only test suites that shell out to @cabal exec ghc@. + These rely on the in-place package database from @cabal build@ + in the source workspace and cannot run from an installed + package, so they are off by default. + default: False + manual: True + +library + exposed-modules: + Acolyte.Core + Acolyte.Core.Method + Acolyte.Core.Path + Acolyte.Core.Endpoint + Acolyte.Core.API + Acolyte.Core.Effect + Acolyte.Core.Wrapper + Acolyte.Core.Session + Acolyte.Core.Versioning + Acolyte.Core.Negotiate + + build-depends: + base >= 4.20 && < 5, + text >= 2.0 && < 2.2 + + hs-source-dirs: src + default-language: GHC2024 + + default-extensions: + DataKinds + GADTs + PolyKinds + TypeFamilies + TypeOperators + UndecidableInstances + ConstraintKinds + StandaloneKindSignatures + NoStarIsType + RoleAnnotations + AllowAmbiguousTypes + StrictData + + ghc-options: -Wall -funbox-strict-fields + +test-suite spec + type: exitcode-stdio-1.0 + main-is: Main.hs + hs-source-dirs: test + default-language: GHC2024 + + default-extensions: + DataKinds + GADTs + PolyKinds + TypeFamilies + TypeOperators + UndecidableInstances + ConstraintKinds + StandaloneKindSignatures + NoStarIsType + AllowAmbiguousTypes + StrictData + + ghc-options: -Wall -rtsopts "-with-rtsopts=-K1K" + + build-depends: + base >= 4.20 && < 5, + acolyte-core, + text >= 2.0 && < 2.2 + +test-suite typeerrors + type: exitcode-stdio-1.0 + main-is: TypeErrors.hs + hs-source-dirs: test + default-language: GHC2024 + ghc-options: -Wall + + if !flag(dev-tests) + buildable: False + + build-depends: + base >= 4.20 && < 5, + process >= 1.6 && < 1.8, + directory >= 1.3 && < 1.4 + +source-repository head + type: git + location: https://github.com/joshburgess/acolyte.git diff --git a/src/Acolyte/Core.hs b/src/Acolyte/Core.hs new file mode 100644 --- /dev/null +++ b/src/Acolyte/Core.hs @@ -0,0 +1,106 @@ +-- | @acolyte-core@ — type-level API specification. +-- +-- This module re-exports all core types for defining HTTP APIs. +-- No IO, no runtime beyond base. +module Acolyte.Core + ( -- * Methods + Method (..) + , SMethod (..) + , KnownMethod (..) + , methodVal + + -- * Path segments + , PathSegment (..) + , Captures + , CapturesTuple + , CountCaptures + , At + , Param + , At2 + , Param2 + , ParamNamed + + -- * Endpoints + , Endpoint + , Get + , Post + , Put + , Delete + , Patch + , NoBody + , Json (..) + + -- * API specification + , type API + , Serves + , Length + , type (++) + + -- * Effects (Layer 1: generic middleware tracking) + , Auth + , Cors + , RateLimit + , Tracing + , Requires + , HasEffect + , RequiredEffects + , AllEffectsProvided + + -- * Endpoint wrappers (Layer 2: per-endpoint typed dispatch) + , Protected + , Validated + , Validate (..) + , Versioned + , ApiVersion (..) + , Describe + , Description + , Named + , AllNamed + , EndpointNames + , NoDuplicateNames + , LookupNamed + , WithParams + , QP + , WithHeaders + , HH + + -- * Streaming RPC markers + , ServerStream + , ClientStream + , BidiStream + + -- * Response status code annotations + , RespondsWith + , PostCreated + , DeleteNoContent + + -- * Session types (WebSocket protocols) + , SessionType (..) + , Dual + + -- * API versioning + , Change (..) + , VersionedApi + , ApplyChanges + , IsBackwardCompatible + , BackwardCompatible + + -- * Content negotiation + , Negotiate + , ContentFormat (..) + , JsonFormat + , XmlFormat + , TextFormat + , HtmlFormat + , CsvFormat + ) where + +import Acolyte.Core.Method +import Acolyte.Core.Path +import Acolyte.Core.Endpoint +import Acolyte.Core.API +import Acolyte.Core.Effect +import Acolyte.Core.Wrapper +import Acolyte.Core.Session +import Acolyte.Core.Versioning +import Acolyte.Core.Negotiate diff --git a/src/Acolyte/Core/API.hs b/src/Acolyte/Core/API.hs new file mode 100644 --- /dev/null +++ b/src/Acolyte/Core/API.hs @@ -0,0 +1,130 @@ +-- | API-level combinators: the completeness check and handler binding. +-- +-- The key design decision: APIs are type-level lists of endpoints. +-- The 'Serves' constraint is a type synonym that uses 'CheckArity' +-- to compare the API length against the handler tuple arity via +-- closed type families. No class, no instances, no recursive +-- constraint resolution — O(1) for the compiler. +module Acolyte.Core.API + ( -- * API specification + type API + -- * Completeness check + , Serves + -- * Length checking + , Length + , TupleArity + , type (==) + -- * Arity checking + , CheckArity + -- * Type-level list append + , type (++) + -- * Custom type errors + , HandlerMismatchMsg + ) where + +import Data.Kind (Type, Constraint) +import GHC.TypeLits (Nat, type (+), TypeError, ErrorMessage (..)) +import Data.Type.Equality (type (==)) +import Data.Type.Bool (If) + + +-- | An API is a type-level list of endpoint types. +-- +-- @ +-- type UsersAPI = +-- '[ Get '[ Lit "users" ] (Json [User]) +-- , Get '[ Lit "users", Capture Int ] (Json User) +-- , Post '[ Lit "users" ] (Json CreateUser) (Json User) +-- ] +-- @ +type API = [Type] + + +-- | Compute the length of a type-level list. +type Length :: [k] -> Nat +type family Length (xs :: [k]) :: Nat where + Length '[] = 0 + Length (_ ': xs) = 1 + Length xs + + +-- | Compute the arity of a handler tuple. +-- Covers arities 0–25 (matching 'BuildServer' coverage). +type TupleArity :: Type -> Nat +type family TupleArity h :: Nat where + TupleArity () = 0 + TupleArity (a, b) = 2 + TupleArity (a, b, c) = 3 + TupleArity (a, b, c, d) = 4 + TupleArity (a, b, c, d, e) = 5 + TupleArity (a, b, c, d, e, f) = 6 + TupleArity (a, b, c, d, e, f, g) = 7 + TupleArity (a, b, c, d, e, f, g, h) = 8 + TupleArity (a, b, c, d, e, f, g, h, i) = 9 + TupleArity (a, b, c, d, e, f, g, h, i, j) = 10 + TupleArity (a, b, c, d, e, f, g, h, i, j, k) = 11 + TupleArity (a, b, c, d, e, f, g, h, i, j, k, l) = 12 + TupleArity (a, b, c, d, e, f, g, h, i, j, k, l, m) = 13 + TupleArity (a, b, c, d, e, f, g, h, i, j, k, l, m, n) = 14 + TupleArity (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) = 15 + TupleArity (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) = 16 + TupleArity (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q) = 17 + TupleArity (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) = 18 + TupleArity (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s) = 19 + TupleArity (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t) = 20 + TupleArity (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u) = 21 + TupleArity (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) = 22 + TupleArity (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) = 23 + TupleArity (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) = 24 + TupleArity (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) = 25 + TupleArity _ = 1 -- bare value = single handler + + +-- | Type-level list append. +-- +-- Used to combine sub-APIs into a larger API: +-- +-- @ +-- type FullAPI = UsersAPI ++ ArticlesAPI ++ CommentsAPI +-- @ +type family (xs :: [k]) ++ (ys :: [k]) :: [k] where + '[] ++ ys = ys + (x ': xs) ++ ys = x ': (xs ++ ys) +infixr 5 ++ + + +-- | Custom error message for handler/endpoint count mismatch. +type HandlerMismatchMsg :: Nat -> Nat -> ErrorMessage +type family HandlerMismatchMsg (nEndpoints :: Nat) (nHandlers :: Nat) :: ErrorMessage where + HandlerMismatchMsg n m = + 'Text "API has " ':<>: 'ShowType n ':<>: 'Text " endpoint(s) but " + ':<>: 'ShowType m ':<>: 'Text " handler(s) were provided." + ':$$: 'Text "Every endpoint must have exactly one handler." + + +-- | Verify that the API endpoint count matches the handler count. +-- Produces a clear 'TypeError' on mismatch instead of a confusing +-- GHC constraint error. +type CheckArity :: Nat -> Nat -> Constraint +type family CheckArity (apiLen :: Nat) (handlerCount :: Nat) :: Constraint where + CheckArity n n = () + CheckArity n m = TypeError (HandlerMismatchMsg n m) + + +-- | The API completeness check. +-- +-- @Serves api handlers@ holds when the handler tuple arity matches +-- the number of endpoints in the API list. If they don't match, +-- produces a clear compile error: +-- +-- @ +-- API has 4 endpoint(s) but 3 handler(s) were provided. +-- Every endpoint must have exactly one handler. +-- @ +-- +-- This is a constraint synonym — no class, no instances, no +-- overlapping pragmas. 'CheckArity' does the work via a closed +-- type family that reduces to @()@ on match or 'TypeError' on +-- mismatch. +type Serves (api :: [Type]) (handlers :: Type) = + CheckArity (Length api) (TupleArity handlers) + diff --git a/src/Acolyte/Core/Effect.hs b/src/Acolyte/Core/Effect.hs new file mode 100644 --- /dev/null +++ b/src/Acolyte/Core/Effect.hs @@ -0,0 +1,149 @@ +-- | Type-level middleware effects. +-- +-- Effects are type-level tags that declare what middleware an endpoint +-- requires. The effect system has two parts: +-- +-- 1. 'Requires' wraps an endpoint in the API type to declare a requirement. +-- 2. 'AllEffectsProvided' checks at serve-time that every required effect +-- has been provided. +-- +-- Effects are user-extensible: any type of kind 'Type' can be an effect. +-- Built-in effects ('Auth', 'Cors', etc.) are provided for convenience. +-- +-- @ +-- type MyAPI = +-- '[ Requires Auth (Get '[ Lit "users" ] (Json [User])) +-- , Requires Cors (Get '[ Lit "public" ] (Json Data)) +-- , Get '[ Lit "health" ] String -- no requirements +-- ] +-- @ +module Acolyte.Core.Effect + ( -- * Built-in effect tags + Auth + , Cors + , RateLimit + , Tracing + -- * Declaring requirements + , Requires + -- * Checking requirements + , HasEffect + , RequiredEffects + , AllEffectsProvided + , Assert + ) where + +import Data.Kind (Type, Constraint) +import GHC.TypeLits (TypeError, ErrorMessage (..)) + +import Acolyte.Core.API (type (++)) + + +-- =================================================================== +-- Built-in effect tags (user-extensible: any Type can be an effect) +-- =================================================================== + +-- | Authentication middleware required. +data Auth + +-- | CORS middleware required. +data Cors + +-- | Rate limiting middleware required. +data RateLimit + +-- | Tracing/observability middleware required. +data Tracing + + +-- =================================================================== +-- Requires: declare that an endpoint needs a middleware effect +-- =================================================================== + +-- | Declare that an endpoint requires effect @e@. +-- +-- @Requires@ is a type-level wrapper — it marks the endpoint but does +-- not change its runtime behavior. At serve-time, 'AllEffectsProvided' +-- checks that every @Requires e _@ in the API has its @e@ in the +-- provided list. If not, compilation fails. +-- +-- Multiple effects can be nested: +-- +-- @ +-- Requires Auth (Requires RateLimit (Get path resp)) +-- @ +type Requires :: Type -> Type -> Type +data Requires (e :: Type) (endpoint :: Type) + + +-- =================================================================== +-- Type-level membership check +-- =================================================================== + +-- | Check whether effect @e@ is in the provided list @es@. +-- +-- Closed type family — O(n) in the length of the list, evaluated by +-- simple top-to-bottom matching with no backtracking. +type HasEffect :: Type -> [Type] -> Bool +type family HasEffect (e :: Type) (es :: [Type]) :: Bool where + HasEffect _ '[] = 'False + HasEffect e (e ': _) = 'True + HasEffect e (_ ': es) = HasEffect e es + + +-- =================================================================== +-- Collect all required effects from an API +-- =================================================================== + +-- | Collect all effects required by endpoints in an API. +-- +-- Walks the API list and extracts the @e@ from every @Requires e _@. +-- Nested @Requires@ are flattened. Non-@Requires@ endpoints contribute +-- nothing. +type RequiredEffects :: [Type] -> [Type] +type family RequiredEffects (api :: [Type]) :: [Type] where + RequiredEffects '[] = '[] + RequiredEffects (Requires e inner ': rest) = + e ': RequiredEffects ('[inner] ++ rest) + RequiredEffects (_ ': rest) = RequiredEffects rest + + +-- =================================================================== +-- AllEffectsProvided: the compile-time completeness check +-- =================================================================== + +-- | Assert with a custom error message. +type Assert :: Bool -> ErrorMessage -> Constraint +type family Assert (b :: Bool) (msg :: ErrorMessage) :: Constraint where + Assert 'True _ = () + Assert 'False msg = TypeError msg + +-- | Verify that every effect required by the API is in the provided list. +-- +-- Two-step design: 'RequiredEffects' collects all effect tags from +-- the API, then 'AllIn' checks each one against the provided list. +-- This separates collection from verification. +-- +-- @ +-- -- Compiles: Auth and Cors are both provided. +-- example :: AllEffectsProvided MyAPI '[Auth, Cors] => () +-- +-- -- Fails: Auth is missing. +-- bad :: AllEffectsProvided MyAPI '[Cors] => () +-- @ +type AllEffectsProvided (api :: [Type]) (provided :: [Type]) = + AllIn (RequiredEffects api) provided + +-- | Check that every effect in @required@ is present in @provided@. +-- Produces a clear compile error naming the first missing effect. +type AllIn :: [Type] -> [Type] -> Constraint +type family AllIn (required :: [Type]) (provided :: [Type]) :: Constraint where + AllIn '[] _ = () + AllIn (e ': es) provided = + ( Assert (HasEffect e provided) + ( 'Text "Missing middleware effect: " ':<>: 'ShowType e + ':$$: 'Text "This effect is required by an endpoint but was not provided." + ':$$: 'Text "Add .provide @" ':<>: 'ShowType e + ':<>: 'Text " to the server builder." + ) + , AllIn es provided + ) diff --git a/src/Acolyte/Core/Endpoint.hs b/src/Acolyte/Core/Endpoint.hs new file mode 100644 --- /dev/null +++ b/src/Acolyte/Core/Endpoint.hs @@ -0,0 +1,79 @@ +-- | Endpoint type: the specification of a single HTTP endpoint. +-- +-- An 'Endpoint' carries the method, path, request body type, and response +-- type as phantom parameters. It exists only at the type level — the runtime +-- representation is empty (just a proxy/phantom). +-- +-- The response type is the /declared/ happy-path type — what appears in +-- OpenAPI specs and client return types. Handlers are free to return +-- @Either AppError resp@ or any compatible response type. +module Acolyte.Core.Endpoint + ( -- * Core endpoint type + Endpoint + -- * Convenience aliases + , Get + , Post + , Put + , Delete + , Patch + -- * Request body marker + , NoBody + -- * JSON response/request marker + , Json (..) + ) where + +import Data.Kind (Type) +import Acolyte.Core.Method (Method (..)) +import Acolyte.Core.Path (PathSegment) + + +-- | A marker for endpoints with no request body (GET, DELETE, HEAD). +data NoBody + + +-- | A single HTTP endpoint descriptor. +-- +-- All parameters are phantom — this type has no runtime representation. +-- +-- * @m@ — HTTP method ('GET, 'POST, etc.) +-- * @path@ — URL path as a type-level list of 'PathSegment' +-- * @req@ — request body type ('NoBody' for bodyless methods) +-- * @resp@ — declared response type (the happy-path type for OpenAPI/clients) +type Endpoint :: Method -> [PathSegment] -> Type -> Type -> Type +data Endpoint (m :: Method) (path :: [PathSegment]) (req :: Type) (resp :: Type) + + +-- | @GET@ endpoint with no request body. +-- +-- @ +-- type ListUsers = Get '[ Lit "users" ] (Json [User]) +-- type GetUser = Get '[ Lit "users", Capture Int ] (Json User) +-- @ +type Get path resp = Endpoint 'GET path NoBody resp + +-- | @POST@ endpoint with a request body. +-- +-- @ +-- type CreateUser = Post '[ Lit "users" ] (Json CreateUserReq) (Json User) +-- @ +type Post path req resp = Endpoint 'POST path req resp + +-- | @PUT@ endpoint with a request body. +type Put path req resp = Endpoint 'PUT path req resp + +-- | @DELETE@ endpoint with no request body. +type Delete path resp = Endpoint 'DELETE path NoBody resp + +-- | @PATCH@ endpoint with a request body. +type Patch path req resp = Endpoint 'PATCH path req resp + + +-- | A JSON-encoded value, used as a request or response body marker. +-- +-- In API types: @Get path (Json User)@ declares a JSON response. +-- In handlers: @Json val@ wraps a value for JSON serialization. +-- +-- The core package defines only the newtype. The server package +-- provides @IntoResponse (Json a)@ for HTTP responses. +newtype Json a = Json { unJson :: a } + deriving (Show, Eq) diff --git a/src/Acolyte/Core/Method.hs b/src/Acolyte/Core/Method.hs new file mode 100644 --- /dev/null +++ b/src/Acolyte/Core/Method.hs @@ -0,0 +1,64 @@ +-- | HTTP method types, promoted to the kind level via DataKinds. +-- +-- Each constructor becomes a type-level tag used to parameterize 'Endpoint'. +-- The 'SMethod' singleton allows demoting back to a runtime value when needed +-- (e.g., for routing or OpenAPI generation). +module Acolyte.Core.Method + ( -- * Method kind + Method (..) + -- * Singleton for runtime access + , SMethod (..) + , KnownMethod (..) + , methodVal + ) where + +import Data.Kind (Constraint, Type) + +-- | HTTP methods, used at the type level via DataKinds. +data Method + = GET + | POST + | PUT + | DELETE + | PATCH + | HEAD + | OPTIONS + deriving stock (Eq, Ord, Show) + +-- | Singleton witness for a promoted 'Method'. +-- +-- Lets us recover the runtime method from a type-level tag +-- without carrying a dictionary everywhere. +type SMethod :: Method -> Type +data SMethod (m :: Method) where + SGET :: SMethod 'GET + SPOST :: SMethod 'POST + SPUT :: SMethod 'PUT + SDELETE :: SMethod 'DELETE + SPATCH :: SMethod 'PATCH + SHEAD :: SMethod 'HEAD + SOPTIONS :: SMethod 'OPTIONS + +-- | Class for recovering the singleton from a type-level method. +type KnownMethod :: Method -> Constraint +class KnownMethod (m :: Method) where + sMethod :: SMethod m + +instance KnownMethod 'GET where sMethod = SGET +instance KnownMethod 'POST where sMethod = SPOST +instance KnownMethod 'PUT where sMethod = SPUT +instance KnownMethod 'DELETE where sMethod = SDELETE +instance KnownMethod 'PATCH where sMethod = SPATCH +instance KnownMethod 'HEAD where sMethod = SHEAD +instance KnownMethod 'OPTIONS where sMethod = SOPTIONS + +-- | Demote a type-level method to its runtime representation. +methodVal :: forall m. KnownMethod m => Method +methodVal = case sMethod @m of + SGET -> GET + SPOST -> POST + SPUT -> PUT + SDELETE -> DELETE + SPATCH -> PATCH + SHEAD -> HEAD + SOPTIONS -> OPTIONS diff --git a/src/Acolyte/Core/Negotiate.hs b/src/Acolyte/Core/Negotiate.hs new file mode 100644 --- /dev/null +++ b/src/Acolyte/Core/Negotiate.hs @@ -0,0 +1,94 @@ +{-# LANGUAGE OverloadedStrings #-} +-- | Type-level content negotiation. +-- +-- A single endpoint can serve multiple content types. The handler +-- returns the domain value; the framework selects the serialization +-- format based on the @Accept@ header. +-- +-- @ +-- type GetArticle = Get '[ Lit "articles", Capture Int ] +-- (Negotiate '[JsonFormat, XmlFormat, TextFormat] Article) +-- @ +-- +-- All formats appear in the OpenAPI spec. The handler just returns +-- @Article@ — no format awareness needed. +module Acolyte.Core.Negotiate + ( -- * Negotiated response type + Negotiate + -- * Content format class + , ContentFormat (..) + -- * Built-in format tags + , JsonFormat + , XmlFormat + , TextFormat + , HtmlFormat + , CsvFormat + ) where + +import Data.Kind (Type) +import Data.Text (Text) + + +-- | A response that supports multiple content types via negotiation. +-- +-- @formats@ is a type-level list of format tags (e.g., @'[JsonFormat, XmlFormat]@). +-- @a@ is the domain type that can be rendered in each format. +-- +-- The server package implements the runtime negotiation: parse the +-- @Accept@ header, select the best format, and serialize @a@ using +-- the appropriate @RenderAs@ instance. +type Negotiate :: [Type] -> Type -> Type +data Negotiate (formats :: [Type]) (a :: Type) + + +-- | A content format tag. +-- +-- Each format declares its MIME type and quality. The server package +-- uses this to match against @Accept@ headers. +class ContentFormat (fmt :: Type) where + -- | The MIME type for this format (e.g., "application/json"). + contentType :: Text + + -- | Default quality weight for this format (0.0–1.0). + -- Used to break ties when the client has no preference. + defaultQuality :: Double + defaultQuality = 1.0 + + +-- =================================================================== +-- Built-in format tags +-- =================================================================== + +-- | JSON format (@application/json@). +data JsonFormat + +instance ContentFormat JsonFormat where + contentType = "application/json" + +-- | XML format (@application/xml@). +data XmlFormat + +instance ContentFormat XmlFormat where + contentType = "application/xml" + defaultQuality = 0.9 + +-- | Plain text format (@text/plain@). +data TextFormat + +instance ContentFormat TextFormat where + contentType = "text/plain" + defaultQuality = 0.5 + +-- | HTML format (@text/html@). +data HtmlFormat + +instance ContentFormat HtmlFormat where + contentType = "text/html" + defaultQuality = 0.8 + +-- | CSV format (@text/csv@). +data CsvFormat + +instance ContentFormat CsvFormat where + contentType = "text/csv" + defaultQuality = 0.3 diff --git a/src/Acolyte/Core/Path.hs b/src/Acolyte/Core/Path.hs new file mode 100644 --- /dev/null +++ b/src/Acolyte/Core/Path.hs @@ -0,0 +1,142 @@ +-- | Type-level path encoding using promoted lists and GHC.TypeLits. +-- +-- Paths are type-level lists of 'PathSegment's. Literal segments use +-- 'Symbol' from GHC.TypeLits directly — no marker types, no TH, no +-- proc macros. This is one of the main advantages over typeway's Rust +-- implementation, which needs proc macros to work around the absence +-- of const generic strings. +-- +-- @ +-- type UsersPath = '[ Lit "users" ] +-- type UserByIdPath = '[ Lit "users", Capture Int ] +-- type PostsPath = '[ Lit "users", Capture Int, Lit "posts", Capture Int ] +-- @ +module Acolyte.Core.Path + ( -- * Path segment kind + PathSegment (..) + -- * Type families + , Captures + , CapturesTuple + , CountCaptures + -- * Re-exports for convenience + -- * Path construction helpers + , At + , Param + , At2 + , Param2 + , ParamNamed + -- * Re-exports for convenience + , Symbol + , Nat + , Type + ) where + +import Data.Kind (Type) +import Data.Text (Text) +import GHC.TypeLits (Symbol, Nat, type (+)) + + +-- | A segment in a URL path, used at the type level. +-- +-- * @Lit s@ matches the literal string @s@ (e.g., @Lit "users"@). +-- * @Capture t@ captures a path segment parsed as type @t@ (e.g., @Capture Int@). +-- * @CaptureRest@ captures all remaining segments as @[Text]@. +data PathSegment + = Lit Symbol -- ^ Literal path segment + | Capture Type -- ^ Captured path parameter + | CaptureNamed Symbol Type -- ^ Captured path parameter with a name + | CaptureRest -- ^ Wildcard tail capture + + +-- | Extract the list of captured types from a path. +-- +-- This is a closed type family — evaluated top-to-bottom by GHC with +-- no backtracking. O(n) in path length, no recursive instance resolution. +-- +-- @ +-- Captures '[] ~ '[] +-- Captures '[ Lit "users" ] ~ '[] +-- Captures '[ Lit "users", Capture Int ] ~ '[Int] +-- Captures '[ Capture Int, Capture String ] ~ '[Int, String] +-- @ +type Captures :: [PathSegment] -> [Type] +type family Captures (path :: [PathSegment]) :: [Type] where + Captures '[] = '[] + Captures (Lit _ ': rest) = Captures rest + Captures (Capture t ': rest) = t ': Captures rest + Captures (CaptureNamed _ t ': rest) = t ': Captures rest + Captures (CaptureRest ': _) = '[[Text]] + + +-- | Count the number of captures in a path (for arity checking). +type CountCaptures :: [PathSegment] -> Nat +type family CountCaptures (path :: [PathSegment]) :: Nat where + CountCaptures '[] = 0 + CountCaptures (Lit _ ': rest) = CountCaptures rest + CountCaptures (Capture _ ': rest) = 1 + CountCaptures rest + CountCaptures (CaptureNamed _ _ ': rest) = 1 + CountCaptures rest + CountCaptures (CaptureRest ': _) = 1 + + +-- | Convert a type-level list of capture types to a tuple. +-- +-- Single captures are unwrapped for ergonomics: @Capture Int@ gives the +-- handler an @Int@, not a @(Int,)@. +-- +-- @ +-- CapturesTuple '[] ~ () +-- CapturesTuple '[Int] ~ Int +-- CapturesTuple '[Int, String] ~ (Int, String) +-- CapturesTuple '[Int, String, Bool] ~ (Int, String, Bool) +-- @ +type CapturesTuple :: [Type] -> Type +type family CapturesTuple (cs :: [Type]) :: Type where + CapturesTuple '[] = () + CapturesTuple '[a] = a + CapturesTuple '[a, b] = (a, b) + CapturesTuple '[a, b, c] = (a, b, c) + CapturesTuple '[a, b, c, d] = (a, b, c, d) + CapturesTuple '[a, b, c, d, e] = (a, b, c, d, e) + CapturesTuple '[a, b, c, d, e, f] = (a, b, c, d, e, f) + CapturesTuple '[a, b, c, d, e, f, g] = (a, b, c, d, e, f, g) + CapturesTuple '[a, b, c, d, e, f, g, h] = (a, b, c, d, e, f, g, h) + + +-- | A single literal path segment. The most common path pattern. +-- +-- @ +-- type API = '[ Get (At "health") Text ] +-- -- equivalent to: Get '[ 'Lit "health" ] Text +-- @ +type At (s :: Symbol) = '[ 'Lit s ] + +-- | A literal segment followed by a typed capture. +-- +-- @ +-- type API = '[ Get (Param "users" Int) (Json User) ] +-- -- equivalent to: Get '[ 'Lit "users", 'Capture Int ] (Json User) +-- @ +type Param (s :: Symbol) (t :: Type) = '[ 'Lit s, 'Capture t ] + +-- | Two literal segments. +-- +-- @ +-- type API = '[ Get (At2 "api" "health") Text ] +-- -- equivalent to: Get '[ 'Lit "api", 'Lit "health" ] Text +-- @ +type At2 (s1 :: Symbol) (s2 :: Symbol) = '[ 'Lit s1, 'Lit s2 ] + +-- | Two literal segments followed by a typed capture. +-- +-- @ +-- type API = '[ Get (Param2 "api" "users" Int) (Json User) ] +-- @ +type Param2 (s1 :: Symbol) (s2 :: Symbol) (t :: Type) = '[ 'Lit s1, 'Lit s2, 'Capture t ] + +-- | A literal segment followed by a named typed capture. +-- +-- @ +-- type API = '[ Get (ParamNamed "userId" "users" Int) (Json User) ] +-- -- equivalent to: Get '[ 'Lit "users", 'CaptureNamed "userId" Int ] (Json User) +-- @ +type ParamNamed (name :: Symbol) (s :: Symbol) (t :: Type) = '[ 'Lit s, 'CaptureNamed name t ] diff --git a/src/Acolyte/Core/Session.hs b/src/Acolyte/Core/Session.hs new file mode 100644 --- /dev/null +++ b/src/Acolyte/Core/Session.hs @@ -0,0 +1,73 @@ +-- | Session types for WebSocket protocol enforcement. +-- +-- A session type describes the exact sequence of messages a WebSocket +-- handler must send and receive. The 'Dual' type family computes the +-- mirror protocol that the client sees. +-- +-- At the core level, these are pure type definitions. Runtime enforcement +-- via LinearTypes happens in the server package — a linear @Session s@ +-- value must be used exactly once, consuming it to produce the next +-- session state. +-- +-- @ +-- type ChatProtocol = +-- Recv JoinMsg (Send WelcomeMsg +-- (Rec (Offer +-- (Recv ChatMsg (Send BroadcastMsg Var)) +-- (Recv LeaveMsg End)))) +-- @ +module Acolyte.Core.Session + ( -- * Session type kind + SessionType (..) + -- * Dual computation + , Dual + ) where + +import Data.Kind (Type) + + +-- | A session type describing a WebSocket protocol. +-- +-- * @Send a s@ — send a message of type @a@, continue with session @s@ +-- * @Recv a s@ — receive a message of type @a@, continue with session @s@ +-- * @Offer s1 s2@ — offer the peer a choice between two continuations +-- * @Select s1 s2@ — select one of two offered continuations +-- * @Rec s@ — recursive protocol (binds the recursion variable) +-- * @Var@ — recursion point (unfolds to the enclosing 'Rec') +-- * @End@ — session complete +data SessionType + = Send Type SessionType + | Recv Type SessionType + | Offer SessionType SessionType + | Select SessionType SessionType + | Rec SessionType + | Var + | End + + +-- | Compute the dual (mirror) of a session type. +-- +-- The dual is what the other side of the protocol sees: +-- sends become receives, offers become selects, and vice versa. +-- Recursive structure is preserved. +-- +-- @ +-- Dual (Send a s) ~ Recv a (Dual s) +-- Dual (Recv a s) ~ Send a (Dual s) +-- Dual (Offer s1 s2) ~ Select (Dual s1) (Dual s2) +-- Dual (Select s1 s2) ~ Offer (Dual s1) (Dual s2) +-- Dual (Rec s) ~ Rec (Dual s) +-- Dual Var ~ Var +-- Dual End ~ End +-- @ +-- +-- Involutive: @Dual (Dual s) ~ s@ for all @s@. +type Dual :: SessionType -> SessionType +type family Dual (s :: SessionType) :: SessionType where + Dual ('Send a s) = 'Recv a (Dual s) + Dual ('Recv a s) = 'Send a (Dual s) + Dual ('Offer s1 s2) = 'Select (Dual s1) (Dual s2) + Dual ('Select s1 s2) = 'Offer (Dual s1) (Dual s2) + Dual ('Rec s) = 'Rec (Dual s) + Dual 'Var = 'Var + Dual 'End = 'End diff --git a/src/Acolyte/Core/Versioning.hs b/src/Acolyte/Core/Versioning.hs new file mode 100644 --- /dev/null +++ b/src/Acolyte/Core/Versioning.hs @@ -0,0 +1,106 @@ +-- | Type-level API versioning with typed deltas. +-- +-- Express API evolution as type-level change operations with compile-time +-- backward compatibility checking. +-- +-- @ +-- type V1 = +-- '[ Get '[ Lit "users" ] (Json [UserV1]) +-- , Get '[ Lit "users", Capture Int ] (Json UserV1) +-- ] +-- +-- type V2Changes = +-- '[ 'Added (Get '[ Lit "profiles", Capture Int ] (Json Profile)) +-- , 'Replaced (Get '[ Lit "users", Capture Int ] (Json UserV1)) +-- (Get '[ Lit "users", Capture Int ] (Json UserV2)) +-- , 'Deprecated (Get '[ Lit "users" ] (Json [UserV1])) +-- ] +-- +-- -- Compiles: no Removed changes, so backward compatible. +-- type V2 = VersionedApi V1 V2Changes (ApplyChanges V1 V2Changes) +-- @ +module Acolyte.Core.Versioning + ( -- * Change kind + Change (..) + -- * Versioned API type + , VersionedApi + -- * Type families + , ApplyChanges + , IsBackwardCompatible + -- * Constraint alias + , BackwardCompatible + ) where + +import Data.Kind (Type, Constraint) +import GHC.TypeLits (TypeError, ErrorMessage (..)) + +import Acolyte.Core.API (type (++)) +import Acolyte.Core.Effect (Assert) + + +-- | A change to an API between versions. +data Change + = Added Type -- ^ New endpoint added + | Removed Type -- ^ Endpoint removed (breaking!) + | Replaced Type Type -- ^ Endpoint replaced with a new version + | Deprecated Type -- ^ Endpoint marked for future removal (still works) + + +-- | A versioned API with its base, changes, and resolved endpoint list. +-- +-- The three parameters enable: +-- * @base@ — the previous version's API type +-- * @changes@ — the list of changes applied +-- * @resolved@ — the resulting API type (computed via 'ApplyChanges') +type VersionedApi :: [Type] -> [Change] -> [Type] -> Type +data VersionedApi (base :: [Type]) (changes :: [Change]) (resolved :: [Type]) + + +-- | Apply a list of changes to a base API, producing the new API. +-- +-- * @Added e@ — appends @e@ to the API +-- * @Removed e@ — removes @e@ from the API (via 'Remove') +-- * @Replaced old new@ — removes @old@, appends @new@ +-- * @Deprecated e@ — no change to the endpoint list (it still works) +type ApplyChanges :: [Type] -> [Change] -> [Type] +type family ApplyChanges (base :: [Type]) (changes :: [Change]) :: [Type] where + ApplyChanges base '[] = base + ApplyChanges base ('Added e ': rest) = ApplyChanges (base ++ '[e]) rest + ApplyChanges base ('Removed e ': rest) = ApplyChanges (Remove e base) rest + ApplyChanges base ('Replaced o n ': rest) = ApplyChanges (Remove o base ++ '[n]) rest + ApplyChanges base ('Deprecated _ ': rest) = ApplyChanges base rest + + +-- | Remove a type from a type-level list (first occurrence). +type Remove :: Type -> [Type] -> [Type] +type family Remove (x :: Type) (xs :: [Type]) :: [Type] where + Remove _ '[] = '[] + Remove x (x ': ys) = ys + Remove x (y ': ys) = y ': Remove x ys + + +-- | Check whether a list of changes is backward compatible. +-- +-- A change set is backward compatible if it contains no 'Removed' changes. +-- Added, Replaced, and Deprecated are all considered backward compatible. +type IsBackwardCompatible :: [Change] -> Bool +type family IsBackwardCompatible (changes :: [Change]) :: Bool where + IsBackwardCompatible '[] = 'True + IsBackwardCompatible ('Removed _ ': _) = 'False + IsBackwardCompatible (_ ': rest) = IsBackwardCompatible rest + + +-- | Constraint that a change set is backward compatible. +-- +-- Produces a clear type error if any 'Removed' change is present. +type BackwardCompatible :: [Change] -> Constraint +type family BackwardCompatible (changes :: [Change]) :: Constraint where + BackwardCompatible changes = + Assert (IsBackwardCompatible changes) + ( 'Text "API version change is not backward compatible." + ':$$: 'Text "The change set contains a 'Removed' endpoint." + ':$$: 'Text "Remove the 'Removed' change or use 'Deprecated' instead." + ) + + +-- Assert imported from Acolyte.Core.Effect diff --git a/src/Acolyte/Core/Wrapper.hs b/src/Acolyte/Core/Wrapper.hs new file mode 100644 --- /dev/null +++ b/src/Acolyte/Core/Wrapper.hs @@ -0,0 +1,294 @@ +-- | Type-level endpoint wrappers for compile-time enforcement. +-- +-- These are Layer 2 wrappers (see ARCHITECTURE.md "Two-Layer Middleware +-- Model"). They sit in the API type and modify how individual handlers +-- are bound and dispatched. They are NOT spire Layers — they operate +-- inside the framework's handler dispatch with full type information. +-- +-- * 'Protected' — requires authentication; handler must accept auth type +-- * 'Validated' — validates request body before handler runs +-- * 'Versioned' — scopes endpoint to an API version prefix +module Acolyte.Core.Wrapper + ( -- * Authentication + Protected + -- * Validation + , Validated + , Validate (..) + -- * Versioning prefix + , Versioned + , ApiVersion (..) + -- * Description + , Describe + , Description + -- * Named endpoints + , Named + , AllNamed + , EndpointNames + , NoDuplicateNames + , LookupNamed + -- * Query parameter annotations + , WithParams + , QP + -- * Header annotations + , WithHeaders + , HH + -- * Streaming RPC markers + , ServerStream + , ClientStream + , BidiStream + -- * Response status code annotations + , RespondsWith + , PostCreated + , DeleteNoContent + ) where + +import Data.Kind (Type, Constraint) +import Data.Text (Text) +import GHC.TypeLits (Symbol, KnownSymbol, Nat, TypeError, ErrorMessage (..)) + +import Acolyte.Core.Endpoint (Endpoint, NoBody, Post, Delete) + + +-- | An endpoint that requires authentication. +-- +-- @auth@ is the authentication result type (e.g., @AuthUser@). +-- @endpoint@ is the underlying endpoint type. +-- +-- In the server package, 'Protected' endpoints require a different +-- handler binding function that enforces @auth@ as the first handler +-- argument. Using the normal @bind@ on a 'Protected' endpoint +-- produces a type error. +-- +-- Composes with 'Requires': +-- +-- @ +-- Requires Auth (Protected AuthUser (Get '[ Lit "users" ] (Json [User]))) +-- @ +type Protected :: Type -> Type -> Type +data Protected (auth :: Type) (endpoint :: Type) + + +-- | An endpoint with compile-time request body validation. +-- +-- @validator@ is a type implementing 'Validate' for the request body type. +-- @endpoint@ is the underlying endpoint type. +-- +-- The framework deserializes the request body, runs the validator, +-- and only calls the handler if validation passes. Returns 422 on +-- failure. +-- +-- @ +-- data CreateUserValidator +-- instance Validate CreateUserValidator CreateUser where +-- validate _ = True -- real validation logic in server package +-- +-- Validated CreateUserValidator (Post '[ Lit "users" ] (Json CreateUser) (Json User)) +-- @ +type Validated :: Type -> Type -> Type +data Validated (validator :: Type) (endpoint :: Type) + + +-- | Class for request body validators. +-- +-- At the core level this is just a marker — the actual validation +-- logic lives in the server package where IO is available. +-- The core defines the class so the API type can reference it. +class Validate (validator :: Type) (body :: Type) where + -- | Runtime validation — implemented in the server package. + -- Core only defines the class head. + validate :: body -> Either String body + + +-- | An endpoint scoped to a specific API version. +-- +-- The version prefix is prepended to the path at routing time. +-- +-- @ +-- data V1 +-- instance ApiVersion V1 where versionPrefix = "v1" +-- +-- Versioned V1 (Get '[ Lit "users" ] (Json [User])) +-- -- matches: /v1/users +-- @ +type Versioned :: Type -> Type -> Type +data Versioned (version :: Type) (endpoint :: Type) + + +-- | Class for API version tags. +class ApiVersion (v :: Type) where + versionPrefix :: Text + + +-- | Annotate an endpoint with a human-readable description. +-- Used by OpenAPI generation for endpoint summaries. +-- Transparent to routing — delegates all endpoint metadata to the inner type. +-- +-- @ +-- type API = +-- '[ Describe "Health check" (Get (At "health") Text) +-- , Describe "Get user by ID" (Get (Param "users" Int) (Json User)) +-- ] +-- @ +type Describe :: Symbol -> Type -> Type +data Describe (desc :: Symbol) (endpoint :: Type) + + +-- | Annotate an endpoint with a longer human-readable description. +-- Used by OpenAPI generation for the @description@ field (distinct from summary). +-- Transparent to routing — delegates all endpoint metadata to the inner type. +-- +-- @ +-- type API = +-- '[ Description "Returns detailed user information including profile data" +-- (Get (Param "users" Int) (Json User)) +-- ] +-- @ +type Description :: Symbol -> Type -> Type +data Description (desc :: Symbol) (endpoint :: Type) + + +-- | Associate a type-level name with an endpoint. +-- +-- Transparent to routing — delegates all endpoint metadata to the inner type. +-- Enables record-based handler binding (via 'GHC.Records.HasField') and +-- sets @operationId@ in OpenAPI generation. +-- +-- @ +-- type API = +-- '[ Named "health" (Get (At "health") Text) +-- , Named "getUser" (Get (Param "users" Int) (Json User)) +-- ] +-- @ +type Named :: Symbol -> Type -> Type +data Named (name :: Symbol) (endpoint :: Type) + + +-- | Check that all endpoints in an API are wrapped with 'Named'. +-- Produces a clear 'TypeError' if any endpoint is not named. +type AllNamed :: [Type] -> Constraint +type family AllNamed (api :: [Type]) :: Constraint where + AllNamed '[] = () + AllNamed (Named name ep ': rest) = AllNamed rest + AllNamed (other ': _) = TypeError + ( 'Text "Expected a Named endpoint, but got:" + ':$$: 'Text " " ':<>: 'ShowType other + ':$$: 'Text "All endpoints must be wrapped with Named for record-based APIs." + ':$$: 'Text "Use: Named \"myName\" (" ':<>: 'ShowType other ':<>: 'Text ")" + ) + + +-- | Extract all endpoint names from a Named API list. +type EndpointNames :: [Type] -> [Symbol] +type family EndpointNames (api :: [Type]) :: [Symbol] where + EndpointNames '[] = '[] + EndpointNames (Named name ep ': rest) = name ': EndpointNames rest + + +-- | Look up an endpoint by its name in a Named API list. +-- Produces a clear 'TypeError' if the name is not found. +type LookupNamed :: Symbol -> [Type] -> Type +type family LookupNamed (name :: Symbol) (api :: [Type]) :: Type where + LookupNamed name '[] = TypeError + ( 'Text "Endpoint name \"" ':<>: 'Text name ':<>: 'Text "\" not found in API." + ) + LookupNamed name (Named name endpoint ': _) = Named name endpoint + LookupNamed name (_ ': rest) = LookupNamed name rest + + +-- | Check that a type-level list of names contains no duplicates. +-- Produces a clear 'TypeError' on the first duplicate found. +type NoDuplicateNames :: [Symbol] -> Constraint +type family NoDuplicateNames (names :: [Symbol]) :: Constraint where + NoDuplicateNames '[] = () + NoDuplicateNames (n ': rest) = (NotElem n rest, NoDuplicateNames rest) + +type NotElem :: Symbol -> [Symbol] -> Constraint +type family NotElem (x :: Symbol) (xs :: [Symbol]) :: Constraint where + NotElem x '[] = () + NotElem x (x ': _) = TypeError + ( 'Text "Duplicate endpoint name: \"" ':<>: 'Text x ':<>: 'Text "\"" + ':$$: 'Text "Each Named endpoint must have a unique name." + ) + NotElem x (_ ': rest) = NotElem x rest + + +-- | Annotate an endpoint with its query parameters for documentation. +-- Transparent to routing — the actual extraction still happens in handlers. +-- Used by OpenAPI generation and client generation to document parameters. +-- +-- @ +-- type API = +-- '[ WithParams '[QP "page" Int, QP "limit" Int] +-- (Get (At "users") (Json [User])) +-- ] +-- @ +type WithParams :: [Type] -> Type -> Type +data WithParams (params :: [Type]) (endpoint :: Type) + +-- | A query parameter declaration (name + type). +type QP :: Symbol -> Type -> Type +data QP (name :: Symbol) (a :: Type) + + +-- | Annotate an endpoint with its required/optional headers. +-- +-- @ +-- type API = +-- '[ WithHeaders '[HH "Authorization" Text, HH "X-Request-Id" Text] +-- (Get (At "users") (Json [User])) +-- ] +-- @ +type WithHeaders :: [Type] -> Type -> Type +data WithHeaders (headers :: [Type]) (endpoint :: Type) + +-- | A header declaration (name + type). +type HH :: Symbol -> Type -> Type +data HH (name :: Symbol) (a :: Type) + + +-- | Mark an endpoint as a server-streaming RPC. +-- The server sends multiple response messages. +-- Used by .proto generation to emit @stream@ in the return type. +-- +-- @ +-- type API = '[ ServerStream (Get (At "events") (Json Event)) ] +-- @ +type ServerStream :: Type -> Type +data ServerStream (endpoint :: Type) + +-- | Mark an endpoint as a client-streaming RPC. +-- The client sends multiple request messages. +-- +-- @ +-- type API = '[ ClientStream (Post (At "upload") (Json Chunk) (Json Result)) ] +-- @ +type ClientStream :: Type -> Type +data ClientStream (endpoint :: Type) + +-- | Mark an endpoint as a bidirectional-streaming RPC. +-- Both client and server stream messages. +-- +-- @ +-- type API = '[ BidiStream (Post (At "chat") (Json Msg) (Json Msg)) ] +-- @ +type BidiStream :: Type -> Type +data BidiStream (endpoint :: Type) + + +-- | Declare the expected response status code for documentation. +-- Transparent to routing. Used by OpenAPI generation. +-- +-- @ +-- type API = +-- '[ RespondsWith 201 (Post (At "users") (Json CreateUser) (Json User)) +-- , RespondsWith 204 (Delete (Param "users" Int) (Json ())) +-- ] +-- @ +type RespondsWith :: Nat -> Type -> Type +data RespondsWith (status :: Nat) (endpoint :: Type) + +-- | Convenience: POST that returns 201 Created. +type PostCreated path req resp = RespondsWith 201 (Post path req resp) + +-- | Convenience: DELETE that returns 204 No Content. +type DeleteNoContent path = RespondsWith 204 (Delete path NoBody) diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,357 @@ +-- | Compile-time tests for the core type-level machinery. +-- +-- If this module compiles, all type-level assertions pass. +-- Negative tests (should-fail) are commented out — uncomment to +-- verify they produce compile errors. +module Main (main) where + +import Acolyte.Core +import Data.Kind (Type, Constraint) +import Data.Text (Text) +import GHC.TypeLits (Symbol) +import Data.Proxy (Proxy (..)) + + +-- =================================================================== +-- Domain types (placeholders) +-- =================================================================== + +data User +data UserV1 +data UserV2 +data Profile +data CreateUser +data AuthUser +data JoinMsg +data WelcomeMsg +data ChatMsg +data BroadcastMsg +data LeaveMsg +data Article + + +-- =================================================================== +-- Path definitions +-- =================================================================== + +type UsersPath = '[ 'Lit "users" ] +type UserByIdPath = '[ 'Lit "users", 'Capture Int ] +type UserPostsPath = '[ 'Lit "users", 'Capture Int, 'Lit "posts", 'Capture Int ] +type ProfilePath = '[ 'Lit "profiles", 'Capture Int ] +type HealthPath = '[ 'Lit "health" ] +type ArticlePath = '[ 'Lit "articles", 'Capture Int ] + + +-- =================================================================== +-- 1. Path capture tests +-- =================================================================== + +type CapturesUsersOk = Captures UsersPath ~ ('[] :: [Type]) +type CapturesSingleOk = Captures UserByIdPath ~ '[Int] +type CapturesMultiOk = Captures UserPostsPath ~ '[Int, Int] + +type TupleEmptyOk = CapturesTuple (Captures UsersPath) ~ () +type TupleSingleOk = CapturesTuple (Captures UserByIdPath) ~ Int +type TupleMultiOk = CapturesTuple (Captures UserPostsPath) ~ (Int, Int) + +type Len0Ok = Length ('[] :: [Type]) ~ 0 +type Len3Ok = Length TestAPI ~ 3 + +_assertCaptures :: (CapturesUsersOk, CapturesSingleOk, CapturesMultiOk) => () +_assertCaptures = () + +_assertTuples :: (TupleEmptyOk, TupleSingleOk, TupleMultiOk) => () +_assertTuples = () + +_assertLengths :: (Len0Ok, Len3Ok) => () +_assertLengths = () + + +-- =================================================================== +-- 2. Serves completeness check +-- =================================================================== + +type TestAPI = + '[ Get UsersPath (Json [User]) + , Get UserByIdPath (Json User) + , Post UsersPath (Json CreateUser) (Json User) + ] + +data H1; data H2; data H3; data H4 + +-- 3 endpoints, 3 handlers — compiles +_servesOk :: Serves TestAPI (H1, H2, H3) => () +_servesOk = () + +-- 1 endpoint, 1 handler — compiles +type SingleAPI = '[ Get UsersPath (Json [User]) ] +_servesSingle :: Serves SingleAPI H1 => () +_servesSingle = () + +-- 2 endpoints, 2 handlers — compiles +type TwoAPI = '[ Get UsersPath (Json [User]), Get UserByIdPath (Json User) ] +_servesTwo :: Serves TwoAPI (H1, H2) => () +_servesTwo = () + +-- NEGATIVE: 3 endpoints, 2 handlers — uncomment to see compile error: +-- "API has 3 endpoint(s) but 2 handler(s) were provided." +-- _servesBad :: Serves TestAPI (H1, H2) => () +-- _servesBad = () + + +-- =================================================================== +-- 3. Effect system tests +-- =================================================================== + +type EffectAPI = + '[ Requires Auth (Get UserByIdPath (Json User)) + , Requires Cors (Get UsersPath (Json [User])) + , Get HealthPath String -- no requirements + ] + +-- All effects provided — compiles +_effectsOk :: AllEffectsProvided EffectAPI '[Auth, Cors] => () +_effectsOk = () + +-- Order doesn't matter — compiles +_effectsReorder :: AllEffectsProvided EffectAPI '[Cors, Auth] => () +_effectsReorder = () + +-- Extra effects are fine — compiles +_effectsExtra :: AllEffectsProvided EffectAPI '[Auth, Cors, Tracing] => () +_effectsExtra = () + +-- Nested effects +type NestedEffectAPI = + '[ Requires Auth (Requires RateLimit (Get UserByIdPath (Json User))) + , Get HealthPath String + ] + +_nestedOk :: AllEffectsProvided NestedEffectAPI '[Auth, RateLimit] => () +_nestedOk = () + +-- No effects required — compiles with any provided list +type NoEffectAPI = '[ Get HealthPath String ] + +_noEffectsOk :: AllEffectsProvided NoEffectAPI '[] => () +_noEffectsOk = () + +-- NEGATIVE: Auth missing — uncomment to see compile error: +-- "Missing middleware effect: Auth" +-- _effectsMissing :: AllEffectsProvided EffectAPI '[Cors] => () +-- _effectsMissing = () + +-- Custom user-defined effect — works because effects are any Type +data MyCustomEffect +type CustomEffectAPI = '[ Requires MyCustomEffect (Get HealthPath String) ] + +_customEffectOk :: AllEffectsProvided CustomEffectAPI '[MyCustomEffect] => () +_customEffectOk = () + + +-- =================================================================== +-- 4. Endpoint wrapper tests (Protected, Validated, Versioned) +-- =================================================================== + +-- Protected composes with Requires +type ProtectedAPI = + '[ Requires Auth (Protected AuthUser (Get UserByIdPath (Json User))) + , Get HealthPath String + ] + +_protectedEffectsOk :: AllEffectsProvided ProtectedAPI '[Auth] => () +_protectedEffectsOk = () + + +-- =================================================================== +-- 5. Session type tests +-- =================================================================== + +-- Chat protocol from the architecture doc +type ChatProtocol = + 'Recv JoinMsg ('Send WelcomeMsg + ('Rec ('Offer + ('Recv ChatMsg ('Send BroadcastMsg 'Var)) + ('Recv LeaveMsg 'End)))) + +-- Dual swaps Send/Recv and Offer/Select +type ChatClientProtocol = Dual ChatProtocol + +-- Dual of Recv is Send +type DualRecvOk = Dual ('Recv JoinMsg 'End) ~ 'Send JoinMsg 'End + +-- Dual is involutive: Dual (Dual s) ~ s +type DualInvolutiveSimple = + Dual (Dual ('Send JoinMsg ('Recv WelcomeMsg 'End))) + ~ 'Send JoinMsg ('Recv WelcomeMsg 'End) + +_assertDual :: (DualRecvOk, DualInvolutiveSimple) => () +_assertDual = () + + +-- =================================================================== +-- 6. Versioning tests +-- =================================================================== + +type V1 = + '[ Get UsersPath (Json [UserV1]) + , Get UserByIdPath (Json UserV1) + ] + +-- Backward-compatible changes: Added + Deprecated (no Removed) +type V2Changes = + '[ 'Added (Get ProfilePath (Json Profile)) + , 'Deprecated (Get UsersPath (Json [UserV1])) + ] + +_v2Compatible :: BackwardCompatible V2Changes => () +_v2Compatible = () + +-- ApplyChanges with Added appends the endpoint +type V2Resolved = ApplyChanges V1 V2Changes +type V2LenOk = Length V2Resolved ~ 3 -- 2 original + 1 added + +_assertV2Len :: V2LenOk => () +_assertV2Len = () + +-- NEGATIVE: Removed endpoint — uncomment to see compile error: +-- "API version change is not backward compatible." +-- type BreakingChanges = '[ 'Removed (Get UsersPath (Json [UserV1])) ] +-- _breakingBad :: BackwardCompatible BreakingChanges => () +-- _breakingBad = () + + +-- =================================================================== +-- 7. Content negotiation tests +-- =================================================================== + +-- An endpoint serving Article in multiple formats +type NegotiatedEndpoint = + Get ArticlePath (Negotiate '[JsonFormat, XmlFormat, TextFormat] Article) + +-- This compiles — Negotiate is just a type wrapper +type NegotiatedAPI = '[ NegotiatedEndpoint, Get HealthPath String ] + +_negotiatedServes :: Serves NegotiatedAPI (H1, H2) => () +_negotiatedServes = () + +-- ContentFormat instances provide runtime metadata +_jsonType :: Text +_jsonType = contentType @JsonFormat + +_xmlType :: Text +_xmlType = contentType @XmlFormat + + +-- =================================================================== +-- 8. Path construction helpers +-- =================================================================== + +-- At "health" should equal '[ 'Lit "health" ] +type AtHealthOk = At "health" ~ '[ 'Lit "health" ] + +-- Param "users" Int should equal '[ 'Lit "users", 'Capture Int ] +type ParamUsersOk = Param "users" Int ~ '[ 'Lit "users", 'Capture Int ] + +_assertPathHelpers :: (AtHealthOk, ParamUsersOk) => () +_assertPathHelpers = () + +-- Describe wrapper compiles in an API type +type DescribedAPI = + '[ Describe "Health check" (Get (At "health") String) + , Describe "Get user by ID" (Get (Param "users" Int) (Json User)) + ] + +_describedServes :: Serves DescribedAPI (H1, H2) => () +_describedServes = () + + +-- =================================================================== +-- 9. WithParams / WithHeaders annotation tests +-- =================================================================== + +-- WithParams compiles and is transparent to Serves +type ParamAPI = + '[ WithParams '[QP "page" Int, QP "limit" Int] + (Get (At "users") (Json [User])) + ] + +_paramServes :: Serves ParamAPI H1 => () +_paramServes = () + +-- WithHeaders compiles and is transparent to Serves +type HeaderAPI = + '[ WithHeaders '[HH "Authorization" Text] + (Get (At "users") (Json [User])) + ] + +_headerServes :: Serves HeaderAPI H1 => () +_headerServes = () + +-- Combined: both annotations compose +type ParamHeaderAPI = + '[ WithParams '[QP "page" Int] + (WithHeaders '[HH "Authorization" Text] + (Get (At "users") (Json [User]))) + ] + +_paramHeaderServes :: Serves ParamHeaderAPI H1 => () +_paramHeaderServes = () + + +-- =================================================================== +-- 10. Streaming marker tests +-- =================================================================== + +-- Streaming markers compile +type StreamAPI = + '[ ServerStream (Get (At "events") (Json [User])) + , ClientStream (Post (At "upload") (Json User) (Json User)) + , BidiStream (Post (At "chat") (Json User) (Json User)) + ] +_streamServes :: Serves StreamAPI (H1, H2, H3) => () +_streamServes = () + + +-- =================================================================== +-- 11. RespondsWith / status code annotation tests +-- =================================================================== + +-- RespondsWith compiles +type StatusAPI = + '[ RespondsWith 201 (Post (At "users") (Json User) (Json User)) + , DeleteNoContent (At "users") + ] +_statusServes :: Serves StatusAPI (H1, H2) => () +_statusServes = () + + +-- =================================================================== +-- 12. KnownMethod runtime demoting +-- =================================================================== + +_methodGet :: Method +_methodGet = methodVal @'GET + +_methodPost :: Method +_methodPost = methodVal @'POST + +_methodDelete :: Method +_methodDelete = methodVal @'DELETE + + +-- =================================================================== +-- Main: just verify the module loaded (all real tests are compile-time) +-- =================================================================== + +main :: IO () +main = do + putStrLn "All compile-time checks passed." + putStrLn "" + putStrLn "Runtime witnesses:" + putStrLn $ " GET = " ++ show _methodGet + putStrLn $ " POST = " ++ show _methodPost + putStrLn $ " DELETE = " ++ show _methodDelete + putStrLn " Serves TestAPI (H1,H2,H3): OK (constraint synonym)" + putStrLn $ " JSON content type: " ++ show _jsonType + putStrLn $ " XML content type: " ++ show _xmlType diff --git a/test/TypeErrors.hs b/test/TypeErrors.hs new file mode 100644 --- /dev/null +++ b/test/TypeErrors.hs @@ -0,0 +1,85 @@ +-- | Compile-time error tests for Named endpoint validation. +-- +-- Each test case is a separate .hs file in typeerror-cases/ that should +-- fail to compile. This runner invokes GHC (via cabal exec) on each and +-- verifies the compilation fails with the expected error message. +module Main (main) where + +import System.Exit (ExitCode (..)) +import System.Process (readProcessWithExitCode) +import System.Directory (getCurrentDirectory) + + +assert :: String -> Bool -> IO () +assert label True = putStrLn $ " OK: " ++ label +assert label False = error $ "FAIL: " ++ label + + +shouldFailToCompile :: FilePath -> String -> IO Bool +shouldFailToCompile file expectedFragment = do + cwd <- getCurrentDirectory + let casePath = cwd ++ "/test/typeerror-cases/" ++ file + + (exitCode, _stdout, stderr) <- readProcessWithExitCode "cabal" + [ "exec", "--", "ghc" + , "-fno-code" + , "-no-keep-hi-files" + , "-package", "acolyte-core" + , casePath + ] "" + case exitCode of + ExitFailure _ -> + if expectedFragment `isInfixOf'` stderr + then pure True + else do + putStrLn $ " ERROR (wrong message): " ++ take 500 stderr + putStrLn $ " EXPECTED: " ++ expectedFragment + pure False + ExitSuccess -> do + putStrLn $ " UNEXPECTED: " ++ file ++ " compiled successfully" + pure False + + +isInfixOf' :: String -> String -> Bool +isInfixOf' needle haystack = any (isPrefixOf' needle) (tails' haystack) + +isPrefixOf' :: String -> String -> Bool +isPrefixOf' [] _ = True +isPrefixOf' _ [] = False +isPrefixOf' (x:xs) (y:ys) = x == y && isPrefixOf' xs ys + +tails' :: [a] -> [[a]] +tails' [] = [[]] +tails' xs@(_:xs') = xs : tails' xs' + + +main :: IO () +main = do + putStrLn "Named endpoint compile-time error tests (core):" + putStrLn "" + + putStrLn "AllNamed (negative):" + shouldFailToCompile "AllNamedMixed.hs" "Expected a Named endpoint" + >>= assert "AllNamed rejects mixed API (some unnamed)" + shouldFailToCompile "AllNamedBare.hs" "Expected a Named endpoint" + >>= assert "AllNamed rejects fully bare API" + putStrLn "" + + putStrLn "NoDuplicateNames (negative):" + shouldFailToCompile "DuplicateNames.hs" "Duplicate endpoint name" + >>= assert "NoDuplicateNames rejects duplicate names" + shouldFailToCompile "DuplicateNamesAdjacent.hs" "Duplicate endpoint name" + >>= assert "NoDuplicateNames rejects adjacent duplicates" + putStrLn "" + + putStrLn "Named arity mismatch (negative):" + shouldFailToCompile "NamedArityMismatch.hs" "endpoint(s) but 3 handler(s)" + >>= assert "Serves rejects wrong arity with Named endpoints" + putStrLn "" + + putStrLn "LookupNamed (negative):" + shouldFailToCompile "LookupNamedMissing.hs" "not found in API" + >>= assert "LookupNamed rejects missing endpoint name" + putStrLn "" + + putStrLn "All Named compile-time error tests (core) passed."