packages feed

acolyte-core (empty) → 0.1.0.0

raw patch · 15 files changed

+1823/−0 lines, 15 filesdep +acolyte-coredep +basedep +directory

Dependencies added: acolyte-core, base, directory, process, text

Files

+ CHANGELOG.md view
@@ -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.
+ LICENSE view
@@ -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.
+ acolyte-core.cabal view
@@ -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 <joshburgess.webdev@gmail.com>+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
+ src/Acolyte/Core.hs view
@@ -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
+ src/Acolyte/Core/API.hs view
@@ -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)+
+ src/Acolyte/Core/Effect.hs view
@@ -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+    )
+ src/Acolyte/Core/Endpoint.hs view
@@ -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)
+ src/Acolyte/Core/Method.hs view
@@ -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
+ src/Acolyte/Core/Negotiate.hs view
@@ -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
+ src/Acolyte/Core/Path.hs view
@@ -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 ]
+ src/Acolyte/Core/Session.hs view
@@ -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
+ src/Acolyte/Core/Versioning.hs view
@@ -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
+ src/Acolyte/Core/Wrapper.hs view
@@ -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)
+ test/Main.hs view
@@ -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
+ test/TypeErrors.hs view
@@ -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."