Search code examples
apihaskellservant

Understanding 'echo' service example API from Servant paper

The introduction of the servant paper contains the following example API type:

type Echo = "echo"
          :> ReqBody ’[PlainText] String
          :> Get ’[PlainText] String

I am attempting to understand this example. It appears to be defining a type synonym, but seems to involve some things that I have not seen before.

Here are three questions that I have about it:

  1. How is there a string literal in the definition of a type?

"echo" is a string literal. I thought these were only used to define specific strings and don't know what this means when used in a type declaration.

  1. What is the symbol :>?

The definition of this symbol in the 'servant' package appears to be defined here and looks like this:

data (path :: k) :> a
    deriving (Typeable)
infixr 9 :>

I would guess that :> corresponds to a / in an api string, but do not see how this definition would make that happen.

This is the first time I am seeing a non-alphanumeric type other than the function type ->.

  1. What does the apostrophe before the list type mean?

[PlainText] I would understand to simply represent a list of PlainText elements, but in contrast I do not understand what ’[PlainText] means.

Solution

  • How is there a string literal in the definition of a type?

    The DataKinds extension lets you use these string literals in type signatures. Each one of them represents a different type. They all belong to the kind Symbol; we can test this using the :kind command in ghci:

    Prelude> :set -XDataKinds
Prelude> :kind "foo"
"foo" :: GHC.Types.Symbol

    Because in Haskell only types of kind * have values, these type-level strings are not inhabited. But there are functions that let you obtain the corresponding term-level string anyway.

    What is the symbol :>?

    The TypeOperators extension lets you define types with operator names. This is useful for parameterized types that are mostly used to combine other types. Notice that :> has two type parameters but no value-level constructors: it is only used at the type level.

    What does the apostrophe before the list type mean?

    DataKinds does more than enabling symbols. It lets you use value constructors as types, and the types of these constructors become kinds in its turn. For example:

    Prelude> :set -XDataKinds
Prelude> :kind True
True :: Bool

    These promoted constructors are not inhabited by any term (because they have kinds other than *).

    In particular, we can promote lists to the type-level. But this creates some ambiguity. What is [Int] in a signature? Is it the type of lists of Ints (that has kind *) or is it a type-level list with one element, the type Int? The apostrophe makes clear that we are talking about the type-level list.

    Prelude> :set -XDataKinds
Prelude> :kind [Int]
[Int] :: *
Prelude> :kind '[Int]
'[Int] :: [*]
Prelude> :kind '[True]
'[True] :: [Bool]

    Type-level lists of more than one element don't require the apostrophe, because there's no ambiguity:

    Prelude> :kind [Int,Int]
[Int,Int] :: [*]