At first we had "Get a" [note that I'm going to be pretty loose about distinguishing type variables in Haskell and in the metalanguage]. OK, the "Get" part should be static - each endpoint can only "be" one method. The 'a' type can be anything, but in the description (i.e., the API type) it is static and that's fine, since these are algebraic data types, and can themselves represent sums and products of other things (in comparison, the method "place" for the endpoints is just a sum.)
So far we pretended status codes didn't need to be represented, because they could be statically determined by the method type. But of course that's bad HTTP practice - an empty body should probably cause a 204 No Content, for instance. So what we did was defined instances that overlapped on the method argument ("a" in "Get a"). Kind of ugly.
Then came content types. That turned out okay, because generally we're fine considering the acceptable content-types for and endpoint to be static. It would be more general to consider them dynamic, though.
Then we got headers. Those we decided should be static. Not great, but that'd work, especially if we allow Maybe values to indicate no header, so that the static claim is the maximal set of headers. Except that the values for the headers are sort of tacked on at the end of the return type, which introduces a sort of weird excrescence to the cleanliness of handler return types.
Also, we've always had the left of the EitherT. That's an embarassment. We pretend the types say anything about the possible return values, but of course they don't because of that either.
Much more recently, we talked about unifying instances for method types. So we started thinking about how, and an idea popped up.
Basically, I think this is what we want:
Get '['[JSON, XML], '[Header "Expires" Date, Header "Etag" UTCTime], 200, a]
'['[JSON, XML], '[Header "Etag"], 204, b]
(We could think of making the syntax nicer. E.g.:
Get :| a `ServedAs` '[JSON, XML] `WithHeaders` '[Header "Expires" Date, Header "Etag" UTCTime] `AndStatus` 200
:| b `ServedAs` '[JSON, XML] `WithHeaders` '[Header "Etag"] `AndStatus` 204
Though here there are fixity issues that we'd likely solve with operators again.)
This is, I think, at last a complete description. The only components of a response are the method, the headers, the reason phrase, the status code, and the body. The reason phrase is pretty much irrelevant, and is generally taken to be a function of the status code. We have all the rest. We additionally also have content-types, which are headers, as a separate thing rather than as normal headers, which makes some sense, though maybe we should rethink.
And I think we can do this!
Just as the content-type list encodes that the return value must be encodable via the tags that the content-type types represent, we require that there be a function (a -> Proxy (Header headername headerType) -> ByteString) for all "headerName" and "headerType" in the list. (There might be questions about what this gets us in practice - let's talk about those too.) (An interesting idea is to not require the status code, and associate it to a type via classes. Another idea is that, if we do so, we could provide a type function AndStatus to try to unify with that type, so that it'd basically be a type-level assert. But this is a digression.)
But what's the type of the handler? In the case above, "Either a b" would work. But, what about three elements? We could just create sum types up to, say, 10. So the handler above would be of type "Sum2 a b" (plus a load of class constraints, of course). ("Sum2" etc. would be instances of MonadIO, but that'd be it.) See the note below for a different idea.
We talked about type-level variable binding/lambdas. If we go this route, we might want to consider them again.
("Any sufficiently complicated Haskell program contains a Lisp.")
But I don't know how that'd work.
In any case, I used to think we should try to keep our types from being "too big". But why again?
Instead of SumN, we could actually have there be a constraint that there be a prism between "a" and "b" in the running example and the type "x" of the handler. Then Server of the large Get type above would resolve to (ALotOfConstraints x) => x! I think that is a pretty different way of thinking about things, and much more general. It is, I think, a really good abstraction boundary: any datatype that should works as a response can be made to work by declaring the appropriate classes. If we then provide concrete datatypes (such as the ResponseHeaders one which we already have) to facilitate development, great. But I get a warm fuzzy feeling knowing our internals wouldn't be giving special privilege to an arbitrary datatype. And it'd allow for others to develop interesting "servant-compatible" datatypes: e.g. an "ETag" typeclass that might delegate to Hashable, or a class that represents the known lenses into a datatype and represents that appropriately in an "Accept-Patch" header.