Skip to content

Instantly share code, notes, and snippets.

@edsko
Last active July 2, 2020 06:52
Show Gist options
  • Star 5 You must be signed in to star a gist
  • Fork 3 You must be signed in to fork a gist
  • Save edsko/edab2eeadbf1a463f221 to your computer and use it in GitHub Desktop.
Save edsko/edab2eeadbf1a463f221 to your computer and use it in GitHub Desktop.
See "Dependently typed servers in Servant" (http://www.well-typed.com/blog/2015/12/dependently-typed-servers/) for the blog post accompanying this gist.
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
-- | Defining dependently typed servers in Servant
--
-- Written by Edsko de Vries <edsko@well-typed.com>
-- and Andres Loeh <andres@well-typed.com>, Well-Typed LLP.
module Main (main) where
import GHC.Prim (Constraint)
import Data.Text (Text)
import Network.Wai
import Network.Wai.Handler.Warp
import Servant
import Servant.Server.Internal
import Text.Read (readMaybe)
import qualified Data.Text as Text
import qualified Data.ByteString.Lazy.Char8 as BS
{-------------------------------------------------------------------------------
Preliminaries
-------------------------------------------------------------------------------}
-- | Existential
data Some :: (k -> *) -> * where
Some :: f a -> Some f
-- | Constraint reification
data Dict (c :: Constraint) where
Dict :: c => Dict c
-- | Type level application
-- (Unlike in the blogpost, we make 'Apply' kind polymorphic)
type family Apply (f :: s) (a :: k) :: *
{-------------------------------------------------------------------------------
Dependent servers
-------------------------------------------------------------------------------}
-- | Server dependent on some index @ix@
newtype DepServer (ix :: k -> *) (f :: s) (m :: * -> *) =
DepServer (forall a. ix a -> ServerT (Apply f a) m)
-- | Dependent analogue of `HasServer`
class HasDepServer ix f where
hasDepServer :: Proxy f -> ix a -> Dict (HasServer (Apply f a))
{-------------------------------------------------------------------------------
Dependent capture
-------------------------------------------------------------------------------}
-- | Dependent capture on some index @ix@
data DepCapture (ix :: k -> *) (f :: s)
instance (FromText (Some ix), HasDepServer ix f) => HasServer (DepCapture ix f) where
type ServerT (DepCapture ix f) m = DepServer ix f m
route Proxy (DepServer subserver) request respond =
case processedPathInfo request of
(p:ps) ->
case fromText p :: Maybe (Some ix) of
Nothing ->
respond $ failWith NotFound
Just (Some (p' :: ix a)) ->
case hasDepServer (Proxy :: Proxy f) p' of
Dict -> route (Proxy :: Proxy (Apply f a))
(subserver p')
request{ pathInfo = ps }
respond
_ ->
respond $ failWith NotFound
{-------------------------------------------------------------------------------
Example
-------------------------------------------------------------------------------}
data Value :: * -> * where
VStr :: Text -> Value Text
VInt :: Int -> Value Int
data Op :: * -> * where
OpEcho :: Op a
OpReverse :: Op Text
OpCaps :: Op Text
OpInc :: Op Int
OpNeg :: Op Int
data ExecOp
type instance Apply ExecOp a = Capture "op" (Op a) :> Get '[PlainText] (Value a)
instance HasDepServer Value ExecOp where
hasDepServer _ (VStr _) = Dict
hasDepServer _ (VInt _) = Dict
type API = DepCapture Value ExecOp
server :: Server API
server = DepServer serveExecOp
serveExecOp :: Value a -> Server (Apply ExecOp a)
serveExecOp val op = return $ execOp val op
execOp :: Value a -> Op a -> Value a
execOp val OpEcho = val
execOp (VStr str) OpReverse = VStr $ Text.reverse str
execOp (VStr str) OpCaps = VStr $ Text.toUpper str
execOp (VInt i) OpInc = VInt $ i + 1
execOp (VInt i) OpNeg = VInt $ negate i
{-------------------------------------------------------------------------------
Parsing and rendering
-------------------------------------------------------------------------------}
instance FromText (Some Value) where
fromText t = Just $ case readMaybe (Text.unpack t) of
Just n -> Some $ VInt n
Nothing -> Some $ VStr t
instance FromText (Op Text) where
fromText "echo" = Just OpEcho
fromText "reverse" = Just OpReverse
fromText "caps" = Just OpCaps
fromText _ = Nothing
instance FromText (Op Int) where
fromText "echo" = Just OpEcho
fromText "inc" = Just OpInc
fromText "neg" = Just OpNeg
fromText _ = Nothing
instance MimeRender PlainText (Value Text) where
mimeRender p (VStr t) = mimeRender p t
instance MimeRender PlainText (Value Int) where
mimeRender _ (VInt n) = BS.pack (show n)
{-------------------------------------------------------------------------------
Main application driver
-------------------------------------------------------------------------------}
app :: Application
app = serve (Proxy :: Proxy API) server
main :: IO ()
main = run 8081 app
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment