cleaned up some type level stuff, added some type level bits

This commit is contained in:
Samuel Schlesinger 2020-08-08 18:46:09 -04:00
parent ef7915fc97
commit 59470bbee3
2 changed files with 46 additions and 10 deletions

3
.gitignore vendored
View File

@ -1,2 +1,3 @@
dist-newstyle/
.stack-work/
*~
*~

View File

@ -1,3 +1,5 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
@ -16,49 +18,81 @@
module Roboservant where
import Control.Applicative
import Prelude hiding (lookup)
import GHC.TypeLits
import Servant.API
-- | Extract the response types from a single servant endpoint, i.e. one
-- without any ':<|>' type constructors in it.
type family ExtractRespType (path :: *) :: * where
ExtractRespType (_ :> b) = ExtractRespType b
ExtractRespType (Verb (method :: StdMethod) (responseCode :: Nat) (contentTypes :: [*]) (respType :: *)) = respType
-- | Extract the response types from a flattened servant API, i.e. one
-- which has the distributive law (modulo isomorphism) applied to it until
-- it reaches a normal form.
type family ExtractRespTypes (paths :: *) :: [*] where
ExtractRespTypes (a :<|> b) = ExtractRespTypes a <> ExtractRespTypes b
ExtractRespTypes a = '[ExtractRespType a]
-- | Append two type level lists.
type family (<>) (xs :: [k]) (ys :: [k]) :: [k] where
(x ': xs) <> ys = x ': (xs <> ys)
'[] <> ys = ys
-- | A homogeneous-functor-list, I guess.
data List :: (* -> *) -> [*] -> * where
Cons :: f a -> List f as -> List f (a ': as)
Nil :: List f '[]
-- | So we can use efficient container types for specific types if the need
-- arises.
class Listy f a where
cons :: a -> f a -> f a
empty :: f a
uncons :: f a -> Maybe (a, f a)
instance Listy [] a where
cons = (:)
empty = []
uncons = \case
a : as -> Just (a, as)
[] -> Nothing
-- | A function for inserting elements into their slot in the store.
class Insert f a as where
insert :: a -> List f as -> List f as
instance {-# OVERLAPPABLE #-} Listy f a => Insert f a (a ': as) where
insert a (Cons as ls) = Cons (cons a as) ls
instance {-# OVERLAPPABLE #-} Insert f a as => Insert f a (b ': as) where
insert a (Cons as ls) = Cons as (insert a ls)
-- | A function for looking up the container of elements for a specific
-- type in the store.
class Lookup f a as where
lookup :: List f as -> f a
instance Show (List f '[]) where
show Nil = "Nil"
instance {-# OVERLAPPABLE #-} Lookup f a (a ': as) where
lookup (Cons fa ls) = fa
instance {-# OVERLAPPABLE #-} Lookup f a as => Lookup f a (b ': as) where
lookup (Cons fa ls) = lookup ls
instance (Show (List f as), forall a. Show a => Show (f a), Show a) => Show (List f (a ': as)) where
show (Cons fa fas) = "(Cons " <> show fa <> " " <> show fas <> ")"
deriving instance (Show (List f as), forall a. Show a => Show (f a), Show a)
=> Show (List f (a ': as))
storeOfApi :: forall api xs. (ExtractRespTypes api ~ xs, BuildStore [] xs) => List [] (ExtractRespTypes api)
instance Show (List f '[]) where show _ = "Nil"
storeOfApi :: BuildStore [] (ExtractRespTypes api) => List [] (ExtractRespTypes api)
storeOfApi = buildStore
class BuildStore f (xs :: [*]) where
class BuildStore f xs where
buildStore :: List f xs
instance BuildStore f '[] where
buildStore = Nil
instance (BuildStore f xs, Alternative f) => BuildStore f (x ': xs) where
buildStore = Cons empty (buildStore @_ @xs)
instance (BuildStore f as, Listy f a) => BuildStore f (a ': as) where
buildStore = Cons empty buildStore
-- 1.
-- Instead of just the resptype, let's return a tuple of (resptype, '[]::[ ? respType])
@ -69,3 +103,4 @@ instance (BuildStore f xs, Alternative f) => BuildStore f (x ': xs) where
-- 'Baz -> whole value
-- '(Key Bar) -> key2
-- '(Key Foo) -> key1
--