Consider the following data type:
data Get (statusCode :: Nat)
Actually, it's a simplified type constructor from servant which is then used in a type-level API like this:
type API = "users" :> Verb 'GET 200 '[JSON] [User]
For our purposes we can cut down the API to
type API = Get 200
Now, having a restriction of the status code being of kind Nat
is too loose, allowing to define a non-existing HTTP status code:
type API = Get 999
Hence, the question: Is there a way to restrict the set of naturals that can be applied to the Get
type constructor?
What was Tried
I'll omit all the pragmas and imports in the code samples for clarity.
A different kind for statusCode
One obvious way to fix it would be to define a separate ADT for status codes and use it in place of Nat
utilizing data type promotion.
data StatusCode = HTTP200 | HTTP201 | HTTP202
data Get (statusCode :: StatusCode)
However, this is a breaking change, which'd require to bump a major version and rewrite all the users' definitions. I doubt the benefit of restricted codes is worth it.
DatatypeContexts
This extension allows to have a straightforward constraint on our type variable
data IsStatusCode statusCode => Get (statusCode :: Nat)
but it requires users to add the constraint to all their declaration. Again, a breaking change. Besides, DatatypeContexts
is deprecated.
Type Families
We could conditionally create Get'
from the example below using type families, but for some reason declaring a type alias happily compiles. In order to get an error we need to construct a value of this type, which is also a breaking change.
data Get' (statusCode :: Nat) = Get
type family Get x where
Get x = If (x <=? 600) (Get' x) (TypeError (Text "Invalid Code"))
type API1 = Get 200
type API2 = Get 999 -- compiles.
api :: Get 999 -- doesn't compile.
api = Get
type API2 = TypeError ...
. I argue that this should compile, otherwise either 1) no code with aTypeError
could type check, or 2) we can no longer substitute aliases and get equivalent programs (type E = TypeError ... ; type X = If .. .. E
should be equivalent totype X = if .. .. (TypeError ..)
, whenE
is not used later on). Note that I'm only guessing here -- I'm not an expert on how these type errors actually work. – chitype HttpStatusCodeOK = (200 :: Nat)
and then supply them intoGet
. This approach doesn't catch attempts to supply wrong codes but it documents the valid ones. – user2556165IsStatusCode
instance for your custom code. – shock_one