Расшифровка продвижения типа DataKind в библиотеке Servant

При включении DataKinds вы получаете новые типы, которые автоматически создаются на основе обычных определений типов данных:

• Если у вас есть data A = B T | C U, теперь вы получаете новый вид A и новые типы 'B :: T -> A и 'C :: U -> A, где T и U — новые виды аналогично расширенных типов T и U.
• Если нет двусмысленности, вы можете написать B вместо 'B и т. д.
• Все строки уровня типа имеют один и тот же тип Symbol, поэтому у вас есть, например. "foo" :: Symbol и "bar" :: Symbol как допустимые типы.

В вашем примере "users" и "sortby" являются типами в виде Symbol, JSON - это (старомодный) тип в виде * (определено здесь), а '[JSON] — это тип вида [*], т. е. это одноэлементный список на уровне типов (он эквивалентен JSON ': '[] точно так же [x] эквивалентно x:[] в целом).

Тип [User] является обычным типом вида *; это просто тип списков Users. Это не одноэлементный список на уровне типов.

Давайте построим Слугу

Цели

Наши цели будут целями Слуги:

• Укажите наш REST API как единый тип API
• Реализуйте сервис как одну побочную (читай: монадическую) функцию.
• Используйте реальные типы для моделирования ресурсов, сериализуя только меньший тип в самом конце, например. JSON или байтовая строка
• Подчиняйтесь общему интерфейсу WAI (Интерфейс веб-приложений), который используется большинством HTTP-фреймворков Haskell.

Переступить порог

Наш первоначальный сервис будет просто /, который возвращает список User в формате JSON.

-- Since we do not support HTTP verbs yet we will go with a Be
data User = ...
data Be a
type API = Be [User]

Хотя нам еще предстоит написать ни одной строки кода на уровне значений, мы уже достаточно представили наш REST-сервис — мы просто схитрили и сделали это на уровне типов. Нам это кажется захватывающим, и впервые за долгое время мы снова надеемся на веб-программирование.

Нам понадобится способ преобразовать это в WAI type Application = Request -> (Response -> IO ResponseReceived) -> IO ResponseReceived. Недостаточно места для описания того, как работает WAI. Основы: нам дан объект запроса и способ создания объектов ответа, и ожидается, что мы вернем объект ответа. Есть много способов сделать это, но простой выбор таков.

imp :: IO [User]
imp =
  return [ User { hopes = ["ketchup", "eggs"], fears = ["xenophobia", "reactionaries"] }
         , User { hopes = ["oldies", "punk"], fears = ["half-tries", "equivocation"] }
         ]

serve :: ToJSON a => Be a -> IO a -> Application
serve _ contentIO = \request respond -> do
  content <- contentIO
  respond (responseLBS status200 [] (encode content))

main :: IO ()
main = run 2016 (serve undefined imp)

И это действительно работает. Мы можем запустить это, свернуть и получить ожидаемый ответ.

% curl 'http://localhost:2016/'
[{"fears":["xenophobia","reactionaries"],"hopes":["ketchup","eggs"]},{"fears":["half-tries","equivocation"],"hopes":["oldies","punk"]}]%

Обратите внимание, что мы никогда не конструировали значение типа Be a. Мы использовали undefined. Сама функция полностью игнорирует параметр. На самом деле нет способа создать значение типа Be a, поскольку мы никогда не определяли никаких конструкторов данных.

Зачем вообще иметь параметр Be a? Бедная простая истина заключается в том, что нам нужна эта переменная a. Он говорит нам, каким будет наш тип контента, и позволяет нам установить это приятное ограничение Aeson.

Код: 0Main.hs.

:‹|>ы на дороге

Теперь мы ставим перед собой задачу разработать систему маршрутизации, в которой у нас могут быть отдельные ресурсы в разных местах в иерархии поддельных URL-адресов. Нашей целью будет поддержка этого вида услуг:

type API =
       "users" :> Be [User]
  :<|> "temperature" :> Int

Для этого нам сначала нужно включить расширения TypeOperators и DataKinds. Как подробно описано в ответе @Cactus, типы данных позволяют нам хранить данные на уровне типа, а GHC встроен со строковыми литералами на уровне типа. (Что здорово, поскольку определение строк на уровне типа не является моей идеей развлечения.)

(Нам также понадобится PolyKinds, чтобы GHC мог определить этот тип. Да, мы сейчас глубоко в джунглях расширений.)

Затем нам нужно придумать умные определения для :> (оператор подкаталога) и :<|> (оператор дизъюнкции).

data path :> rest
data left :<|> right =
  left :<|> right

infixr 9 :>
infixr 8 :<|>

Я сказал умный? Я имел в виду мертвую простоту. Обратите внимание, что мы дали :<|> конструктор типа. Это потому, что мы будем склеивать наши монадические функции вместе, чтобы реализовать дизъюнкт и... о, проще привести пример.

imp :: IO [User] :<|> IO Int
imp =
  users :<|> temperature
  where
    users =
      return [ User ["ketchup", "eggs"] ["xenophobia", "reactionaries"]
             , User ["oldies", "punk"] ["half-tries", "equivocation"]
             ]
    temperature =
      return 72

Теперь давайте обратим наше внимание на специальную проблему serve. Мы больше не можем писать функцию serve, которая полагается на то, что API является Be a. Теперь, когда у нас есть небольшой DSL на уровне типов для сервисов RESTful, было бы неплохо, если бы мы могли каким-то образом сопоставить шаблоны для типов и реализовать разные serve для Be a, path :> rest и left :<|> right. И есть!

class ToApplication api where
  type Content api
  serve :: api -> Content api -> Application

instance ToJSON a => ToApplication (Be a) where
  type Content (Be a) = IO a
  serve _ contentM = \request respond -> do
    content <- contentM
    respond . responseLBS status200 [] . encode $ content

Обратите внимание на использование здесь связанных типов данных (которые, в свою очередь, требуют от нас включения либо TypeFamilies, либо GADTs). Хотя конечная точка Be a имеет реализацию с типом IO a, этого будет недостаточно для реализации дизъюнкции. Как малооплачиваемые и ленивые функциональные программисты, мы просто добавим еще один уровень абстракции и определим функцию уровня типа с именем Content, которая принимает тип api и возвращает тип Content api.

instance Exception RoutingFailure where

data RoutingFailure =
  RoutingFailure
  deriving (Show)

instance (KnownSymbol path, ToApplication rest) => ToApplication (path :> rest) where
  type Content (path :> rest) = Content rest
  serve _ contentM = \request respond -> do
    case pathInfo request of
      (first:pathInfoTail)
        | view unpacked first == symbolVal (Proxy :: Proxy path) -> do
            let subrequest = request { pathInfo = pathInfoTail }
            serve (undefined :: rest) contentM subrequest respond
      _ ->
        throwM RoutingFailure

Мы можем разбить строки кода здесь:

• Мы гарантируем экземпляр ToApplication для path :> rest, если компилятор может гарантировать, что path является символом уровня типа (это означает, что он может [среди прочего] быть сопоставлен с String с symbolVal) и что ToApplication rest существует.

• Когда запрос поступает, мы сопоставляем шаблон на pathInfos, чтобы определить успех. В случае неудачи мы будем делать ленивую вещь и генерировать непроверенное исключение в IO.

• В случае успеха мы выполним рекурсию на уровне типа (вызов лазерных шумов и генератора тумана) с помощью serve (undefined :: rest). Обратите внимание, что rest является "меньшим" типом, чем path :> rest, очень похоже на то, как при сопоставлении с шаблоном в конструкторе данных вы получаете "меньшее" значение.

• Перед рекурсией мы сокращаем HTTP-запрос с помощью удобного обновления записи.

Обратите внимание, что:

• Функция type Content сопоставляет path :> rest с Content rest. Еще одна форма рекурсии на уровне типов! Также обратите внимание, что это означает, что дополнительный путь в маршруте не меняет тип ресурса. Это соответствует нашей интуиции.

• Генерация исключения в IO — это не Great Library Design™, но я оставлю решение этой проблемы на ваше усмотрение. (Подсказка: ExceptT/throwError.)

• Надеюсь, мы постепенно мотивируем использование здесь DataKinds строковыми символами. Возможность представлять строки на уровне типа позволила нам использовать типы для сопоставления с образцом маршрутизации на уровне типа.

• Я использую линзы для упаковки и распаковки. Просто мне быстрее эти ТАК ответы халтурить с линзами, но можно было конечно просто использовать pack из библиотеки Data.Text.

Хорошо. Еще один экземпляр. Дышать. Сделайте перерыв.

instance (ToApplication left, ToApplication right) => ToApplication (left :<|> right) where
  type Content (left :<|> right) = Content left :<|> Content right
  serve _ (leftM :<|> rightM) = \request respond -> do
    let handler (_ :: RoutingFailure) =
          serve (undefined :: right) rightM request respond
    catch (serve (undefined :: left) leftM request respond) handler

В данном случае мы

• Гарантируйте ToApplication (left :<|> right), если компилятор может гарантировать, бла-бла-бла, что вы его получите.

• Введите еще одну запись в функцию type Content. Вот строка кода, которая позволяет нам создать тип IO [User] :<|> IO Int и заставить компилятор успешно разбить его в ходе разрешения экземпляра.

• Перехватите исключение, которое мы бросили выше! Когда исключение происходит слева, мы идем направо. Опять же, это не Great Library Design™.

Запустите 1Main.hs, и вы сможете curl сделать это так.

% curl 'http://localhost:2016/users'
[{"fears":["xenophobia","reactionaries"],"hopes":["ketchup","eggs"]},{"fears":["half-tries","equivocation"],"hopes":["oldies","punk"]}]%

% curl 'http://localhost:2016/temperature'
72%

Давать и брать

Теперь давайте продемонстрируем использование списков на уровне типов, еще одну особенность DataKinds. Мы расширим наш data Be, чтобы хранить список типов, которые может выдать конечная точка.

data Be (gives :: [*]) a

data English
data Haskell
data JSON

-- | The type of our RESTful service
type API =
       "users" :> Be [JSON, Haskell] [User]
  :<|> "temperature" :> Be [JSON, English] Int

Давайте также определим класс типов, который соответствует списку типов, которые конечная точка может предоставить, со списком типов MIME, которые может принять HTTP-запрос. Здесь мы будем использовать Maybe для обозначения ошибки. Опять же, не Great Library Design™.

class ToBody (gives :: [*]) a where
  toBody :: Proxy gives -> [ByteString] -> a -> Maybe ByteString

class Give give a where
  give :: Proxy give -> [ByteString] -> a -> Maybe ByteString

Почему два отдельных класса типов? Ну, нам нужен один для типа [*], который соответствует списку типов, и один для вида *, который является видом только одного типа. Точно так же, как вы не можете определить функцию, которая принимает в качестве аргумента что-то, что является одновременно и списком, и не-списком (поскольку она не будет проверять тип), мы не можем определить класс типов, который принимает в качестве аргумента что-то, что одновременно является типом. список уровня и не-список уровня типа (поскольку он не будет проверять вид). Если бы только у нас были добрые классы...

Давайте посмотрим на этот класс типов в действии:

instance (ToBody gives a) => ToApplication (Be gives a) where
  type Content (Be gives a) = IO a
  serve _ contentM = \request respond -> do
    content <- contentM
    let accepts = [value | ("accept", value) <- requestHeaders request]
    case toBody (Proxy :: Proxy gives) accepts content of
      Just bytes ->
        respond (responseLBS status200 [] (view lazy bytes))
      Nothing ->
        respond (responseLBS status406 [] "bad accept header")

Очень хорошо. Мы используем toBody как способ абстрагироваться от вычисления преобразования значения типа a в базовые байты, которые нужны WAI. В случае неудачи мы просто выдадим ошибку 406, один из самых загадочных (и, следовательно, более интересных) кодов состояния.

Но подождите, зачем вообще использовать списки на уровне типов? Потому что, как и раньше, мы собираемся сопоставить два его конструктора: nil и cons.

instance ToBody '[] a where
  toBody Proxy _ _ = Nothing

instance (Give first a, ToBody rest a) => ToBody (first ': rest) a where
  toBody Proxy accepted value =
    give (Proxy :: Proxy first) accepted value
      <|> toBody (Proxy :: Proxy rest) accepted value

Надеюсь, в этом есть смысл. Сбой происходит, когда список становится пустым до того, как мы находим совпадение; <|> гарантирует, что мы замкнёмся в случае успеха; toBody (Proxy :: Proxy rest) - рекурсивный случай.

Нам понадобится несколько забавных экземпляров Give для игры.

instance ToJSON a => Give JSON a where
  give Proxy accepted value =
    if elem "application/json" accepted then
      Just (view strict (encode value))
    else
      Nothing

instance (a ~ Int) => Give English a where
  give Proxy accepted value =
    if elem "text/english" accepted then
      Just (toEnglish value)
    else
      Nothing
    where
      toEnglish 0 = "zero"
      toEnglish 1 = "one"
      toEnglish 2 = "two"
      toEnglish 72 = "seventy two"
      toEnglish _ = "lots"

instance Show a => Give Haskell a where
  give Proxy accepted value =
    if elem "text/haskell" accepted then
      Just (view (packed . re utf8) (show value))
    else
      Nothing

Запустите сервер еще раз, и вы сможете curl вот так:

% curl -i 'http://localhost:2016/users' -H 'Accept: application/json'
HTTP/1.1 200 OK
Transfer-Encoding: chunked
Date: Wed, 04 May 2016 06:56:10 GMT
Server: Warp/3.2.2

[{"fears":["xenophobia","reactionaries"],"hopes":["ketchup","eggs"]},{"fears":["half-tries","equivocation"],"hopes":["oldies","punk"]}]%

% curl -i 'http://localhost:2016/users' -H 'Accept: text/plain'
HTTP/1.1 406 Not Acceptable
Transfer-Encoding: chunked
Date: Wed, 04 May 2016 06:56:11 GMT
Server: Warp/3.2.2

bad accept header%

% curl -i 'http://localhost:2016/users' -H 'Accept: text/haskell'
HTTP/1.1 200 OK
Transfer-Encoding: chunked
Date: Wed, 04 May 2016 06:56:14 GMT
Server: Warp/3.2.2

[User {hopes = ["ketchup","eggs"], fears = ["xenophobia","reactionaries"]},User {hopes = ["oldies","punk"], fears = ["half-tries","equivocation"]}]%

% curl -i 'http://localhost:2016/temperature' -H 'Accept: application/json'
HTTP/1.1 200 OK
Transfer-Encoding: chunked
Date: Wed, 04 May 2016 06:56:26 GMT
Server: Warp/3.2.2

72%

% curl -i 'http://localhost:2016/temperature' -H 'Accept: text/plain'
HTTP/1.1 406 Not Acceptable
Transfer-Encoding: chunked
Date: Wed, 04 May 2016 06:56:29 GMT
Server: Warp/3.2.2

bad accept header%

% curl -i 'http://localhost:2016/temperature' -H 'Accept: text/english'
HTTP/1.1 200 OK
Transfer-Encoding: chunked
Date: Wed, 04 May 2016 06:56:31 GMT
Server: Warp/3.2.2

seventy two%

Ура!

Обратите внимание, что мы перестали использовать undefined :: t и переключились на Proxy :: Proxy t. Оба являются хаками. Вызов функций в Haskell позволяет нам указывать значения для параметров-значений, но не типы для параметров-типов. Печальная асимметрия. И undefined, и Proxy являются способами кодирования параметров типа на уровне значения. Proxy может сделать это без затрат времени выполнения, и t в Proxy t является многородным. (undefined имеет тип *, поэтому undefined :: rest даже не стал бы проверять здесь.)

Оставшаяся работа

Как мы можем пройти весь путь до полноценного конкурента Servant?

• Нам нужно разбить Be на Get, Post, Put, Delete. Обратите внимание, что некоторые из этих команд теперь также принимают данные in в форме тела запроса. Моделирование типов контента и тел запросов на уровне типа требует аналогичного механизма уровня типа.

• Что, если пользователь захочет смоделировать свои функции как что-то помимо IO, например, как стек преобразователей монад?

• Более точный, но более сложный, алгоритм маршрутизации.

• Эй, теперь, когда у нас есть тип для нашего API, можно ли сгенерировать клиент службы? Что-то, что делает HTTP-запросы к службе, подчиняющейся описанию API, а не создает саму службу HTTP?

• Документация. Убедиться, что все понимают, что представляют собой все эти шутки на уровне типов. ;)

Эта галочка

Мне также непонятно, что означает галочка (') перед "[JSON].

Ответ неясен и застрял в руководстве GHC в разделе 7.9.

Поскольку конструкторы и типы используют одно и то же пространство имен, при повышении вы можете получить неоднозначные имена типов. В этих случаях, если вы хотите сослаться на продвигаемый конструктор, вы должны поставить перед его именем кавычки.

С -XDataKinds типы списков и кортежей Haskell изначально повышаются до видов и пользуются тем же удобным синтаксисом на уровне типов, хотя и с префиксом кавычки. Для списков на уровне типов из двух или более элементов, таких как сигнатура foo2 выше, кавычки могут быть опущены, поскольку значение однозначно. Но для списков из одного или нуля элементов (как в foo0 и foo1) кавычки обязательны, потому что типы [] и [Int] имеют существующие значения в Haskell.

Это, то, насколько многословным был весь код, который нам пришлось написать выше, и многое другое, кроме того, связано с тем, что программирование на уровне типов все еще является гражданином второго сорта в Haskell, в отличие от языков с зависимой типизацией (Agda, Idris, Coq). Синтаксис странный, расширений много, документация скудная, ошибки бессмысленны, но программирование на уровне типов — это весело.