What does an apostrophe in front of a list ( '

问题:

I was reading the Servant documentation and came across this line:

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

What is the ' doing to that list?

回答1:

This is DataKinds in action, which:

• lifts values at the type level, and
• lifts types to the kind level

This however causes confusion at the type level. Now, in types, [X] might either be [X] :: *, the list-of-X type, or instead we might have [X] :: [T] due to the lifting -- that is the value [X] (list containing only the single value X), with X of type T, lifted at the type level.

To overcome this ambiguity, GHC requires a quote in front of lifted value constructors. So, we have [X] :: *, and '[X] :: [T].

Concretely, in your case, Get '[JSON] [User] involves both the list value [JSON] lifted to the type level, and the list type [User]. To better appreciate the difference, note that there are no terms of type '[JSON], since this is not a list type. We could even have Get '[JSON,JSON,JSON] [User] as a well-kinded expression, or even Get '[] [User]. Instead, we can't have Get '[JSON] [User,User] since [User,User] is not a type.

(The type Get '[JSON,JSON,JSON] [User], even if it is valid, could not be meaningfully used by the Servant library. I have no idea of what that lifted list is used for in Servant.)

回答2:

Quotes are used to distinguish type-level constructors vs. term-level constructors of promoted types.

For instance:

{-# LANGUAGE DataKinds #-}

data Which = One | Two

myPick :: Which -- Type
myPick = One

type MyPick :: Which -- Kind
type MyPick = 'One

By the way, the kind annotation type MyPick :: Which is not valid Haskell but it gives you an idea of the correspondence between the term and the type level. The closest you can get to this requires turning on another extension:

{-# LANGUAGE TypeFamilies #-}

type family MyPick :: Which where
  MyPick = 'One