Deciphering DataKind type promotion in Servant library

I am trying to gork the tutorial for the servant library, a type-level web DSL. The library makes extensive use of the DataKind language extension.

Early in that that tutorial we find the following line which defines a web service end point:

type UserAPI = "users" :> QueryParam "sortby" SortBy :> Get '[JSON] [User]

I don't understand what it means to have string and arrays in a type signature. I am also unclear what the tick mark (') means in front of '[JSON].

So my questions boil down to what is the type/kind of the string and arrays, and how is this later interpreted when it is turned into a WAI end point?

As a side note, the consistent use of Nat and Vect when describing DataKinds leave us with a frustratingly limited set of examples to look at when trying to understand this stuff. I think I've read through that example at least a dozen times at different places and I still don't feel like I understand what is going on.

Solution

With DataKinds turned on, you get new types that are automatically created based on regular data type definitions:

If you have data A = B T | C U, you now get a new kind A and new types 'B :: T -> A and 'C :: U -> A, where T and U are the new kinds of the similarly lifted T and U types
If there is no ambiguity, you can write B for 'B etc.
Type-level strings all share the same kind Symbol, so you have e.g. "foo" :: Symbol and "bar" :: Symbol as valid types.

In your example, "users" and "sortby" are both types at kind Symbol, JSON is an (old-fashioned) type at kind * (defined here), and '[JSON] is a type at kind [*], i.e. it is a singleton type-level list (it is equivalent to JSON ': '[] the same way [x] is equivalent to x:[] in general).

The [User] type is a regular type at kind *; it is simply the type of lists of Users. It is not a singleton type-level list.