Как добавить ограничение в конструктор типов

Рассмотрим следующий тип данных:

data Get (statusCode :: Nat)

На самом деле это упрощённый конструктор типа из servant, который затем используется в API-интерфейсе уровня типа:

type API = "users" :> Verb 'GET 200 '[JSON] [User]

В наших целях мы можем сократить API до

type API = Get 200

Теперь ограничение кода статуса вида Nat слишком слабое, что позволяет определить несуществующий код состояния HTTP:

type API = Get 999

Следовательно, вопрос: Есть ли способ ограничить набор naturals, которые могут быть применены к конструктору типа Get?

Что было пробовано

Я пропущу все прагмы и импорт в образцах кода для ясности.

Другой тип для statusCode

Один очевидный способ исправить это - это определить отдельный код ADT для кодов состояния и использовать его вместо Nat, используя продвижение типа данных.

data StatusCode = HTTP200 | HTTP201 | HTTP202
data Get (statusCode :: StatusCode)

Тем не менее, это перерыв в изменении, который требует, чтобы удар основной версии и переписать все определения пользователей. Я сомневаюсь, что преимущество ограниченных кодов стоит того.

DatatypeContexts

Это расширение позволяет иметь прямое ограничение для нашей переменной типа

data IsStatusCode statusCode => Get (statusCode :: Nat)

но для этого требуется, чтобы пользователи добавили ограничение во все свои объявления. Опять же, нарушение. Кроме того, DatatypeContexts устарел.

Семейство типов

Мы могли условно создать Get' из приведенного ниже примера с использованием семейств типов, но по какой-то причине объявление типа alias с удовольствием компилируется. Чтобы получить ошибку, нам нужно построить значение этого типа, что также является нарушением изменений.

data Get' (statusCode :: Nat) = Get

type family Get x where
  Get x = If (x <=? 600) (Get' x) (TypeError (Text "Invalid Code"))

type API1 = Get 200
type API2 = Get 999 -- compiles.

api :: Get 999 -- doesn't compile.
api = Get

Ответы

Ответ 1

Я начну с решения, а затем обсужу другие возможности (которые, как представляется, не были развернуты):

{-# LANGUAGE TypeOperators, TypeInType, GADTs #-}

import GHC.TypeLits (Nat, type (<=))
import Data.Proxy (Proxy(..))
import Data.Kind (type (*))

data Get (statusCode :: Nat) :: (statusCode <= 600) => *

type API1 = Get 900 -- compiles
type API2 = Get 200 -- compiles

api1 :: Proxy (Get 900) -- doesn't compile
api1 = Proxy

api2 :: Proxy (Get 200) -- compiles
api2 = Proxy

Нет семейств типа, которые вам нужны, и не нужно никогда не опускаться до уровня ценности. Однако синонимы типов будут скомпилированы. Использование синонима типа недействительного Get приведет к сбою времени компиляции на сайте использования. Я считаю, что это так же хорошо, как вы можете надеяться. Пожалуйста, дайте мне знать, если что-то неясно.

Далее, только некоторые мысли о других подходах:

DatatypeContexts

Этот никогда не будет работать: помимо устаревания все это добавляет ограничение к конструкторам. Вы специально указали, что не хотите создавать что-либо типа, поэтому это бессмысленно. Новый синтаксис GADT устраняет эту неоднозначность - ограничения теперь явно связаны с конструкторами данных или типов.

Тип семейства и TypeError

Я считаю, что это должно работать, и не нужно строить значение типа. (Итак, должно быть хорошо:)

data Get' (statusCode :: Nat)

type family Get x where
  Get x = If (x <=? 600) (Get' x) (TypeError (Text "Invalid Code"))

api2 :: Proxy (Get 200) -- should compile.
api2 = Proxy

api1 :: Proxy (Get 999) -- shouldn't compile, but currently does
api1 = Proxy

Я мотивирован полагать, что это должно работать на основе example в этом тике. Что-то здесь явно не ведет себя так, как должно: даже если я заменю вызов функции типа If самой TypeError, все равно ничего не запускается - кажется, что TypeErrors, которые не являются верхним уровнем, все еще вызывают некоторые проблемы.

С другой стороны, я действительно не знаю, как должно выглядеть поведение синтаксисов TypeError в type, хотя я склонен сказать, что type API1 = Get 999 не следует компилировать, так как type API1 = TypeError (Text "error") этого не делает.