on master help sign in
with thanks to samspace
commita796dc401e9bf5dac6854309a25be6e210874304 authorMark Wotton <mwotton@gmail.com> dateFri 5 Jun 2020, 12:01 (6 years ago)
1 file changed+106
src/Lib.hs+106
src/Lib.hsnew file+106
@@ -0,0 +1,106 @@
1+
2+
3+{-# LANGUAGE QuantifiedConstraints #-}
4+{-# LANGUAGE FlexibleContexts #-}
5+{-# LANGUAGE AllowAmbiguousTypes #-}
6+{-# LANGUAGE FlexibleInstances #-}
7+{-# LANGUAGE MultiParamTypeClasses #-}
8+{-# LANGUAGE ScopedTypeVariables #-}
9+{-# LANGUAGE TypeApplications #-}
10+{-# LANGUAGE RankNTypes #-}
11+{-# LANGUAGE GADTs #-}
12+{-# LANGUAGE TypeOperators #-}
13+{-# LANGUAGE DataKinds #-}
14+{-# LANGUAGE KindSignatures #-}
15+{-# LANGUAGE PolyKinds #-}
16+{-# LANGUAGE TypeFamilies #-}
17+{-# LANGUAGE UndecidableInstances #-}
18+module Lib where
19+
20+import GHC.TypeLits
21+import Control.Applicative
22+import Servant.API
23+
24+newtype Foo = Foo Int
25+ deriving Show
26+
27+newtype Bar = Bar String
28+ deriving Show
29+
30+type FooApi = "foo" :> "fle" :> "far" :> Get '[JSON] Foo
31+
32+type BarApi = "bar" :> ReqBody '[JSON] Foo :> Post '[JSON] Bar
33+
34+type Api = FooApi
35+ :<|> BarApi
36+
37+type family ExtractRespType (path :: *) :: * where
38+ ExtractRespType (_ :> b) = ExtractRespType b
39+ ExtractRespType (Verb (method :: StdMethod) (responseCode :: Nat) (contentTypes :: [*]) (respType :: *)) = respType
40+
41+type Foo' = ExtractRespType FooApi
42+
43+
44+test :: ()
45+test = foo'EqualFoo where
46+ foo'EqualFoo :: Foo' ~ Foo => ()
47+ foo'EqualFoo = ()
48+
49+
50+test' :: ()
51+test' = blah where
52+ blah :: ExtractRespTypes Api ~ '[Foo, Bar] => ()
53+ blah = ()
54+
55+type family ExtractRespTypes (paths :: *) :: [*] where
56+ ExtractRespTypes (a :<|> b) = ExtractRespTypes a <> ExtractRespTypes b
57+ ExtractRespTypes a = '[ExtractRespType a]
58+
59+type family (<>) (xs :: [k]) (ys :: [k]) :: [k] where
60+ (x ': xs) <> ys = x ': (xs <> ys)
61+ '[] <> ys = ys
62+
63+data List :: (* -> *) -> [*] -> * where
64+ Cons :: f a -> List f as -> List f (a ': as)
65+ Nil :: List f '[]
66+
67+class Insert f a as where
68+ insert :: a -> List f as -> List f as
69+
70+class Lookup f a as where
71+ lookup :: List f as -> f a
72+
73+instance Show (List f '[]) where
74+ show Nil = "Nil"
75+
76+instance (Show (List f as), forall a. Show a => Show (f a), Show a) => Show (List f (a ': as)) where
77+ show (Cons fa fas) = "(Cons " <> show fa <> " " <> show fas <> ")"
78+
79+storeOfApi :: forall api xs. (ExtractRespTypes api ~ xs, BuildStore [] xs) => List [] (ExtractRespTypes api)
80+storeOfApi = buildStore
81+
82+storeOfOurApi = storeOfApi @Api
83+
84+class BuildStore f (xs :: [*]) where
85+ buildStore :: List f xs
86+
87+instance BuildStore f '[] where
88+ buildStore = Nil
89+
90+instance (BuildStore f xs, Alternative f) => BuildStore f (x ': xs) where
91+ buildStore = Cons empty (buildStore @_ @xs)
92+
93+main :: IO ()
94+main = pure ()
95+
96+-- 1.
97+-- Instead of just the resptype, let's return a tuple of (resptype, '[]::[ ? respType])
98+
99+-- 2.
100+-- break down respType into "useful" components
101+-- data Baz = Baz { key1 :: Key Foo, key2 :: Key Bar }
102+-- should insert into type-indexed list three elements
103+-- 'Baz -> whole value
104+-- '(Key Bar) -> key2
105+-- '(Key Foo) -> key1
106+