Last active
July 2, 2020 06:52
-
-
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.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 <[email protected]> | |
-- and Andres Loeh <[email protected]>, 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