17

考虑以下数据类型：

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

因此，问题是：有没有办法限制可以应用于Get类型构造函数的自然集合？

尝试了什么

为了清楚起见，我将省略代码示例中的所有编译指示和导入。

一种不同的statusCode

一种明显的解决方法是为状态代码定义一个单独的 ADT，并使用它来代替Nat使用数据类型提升。

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

但是，这是一个重大更改，需要升级主要版本并重写所有用户的定义。我怀疑限制代码的好处是否值得。

数据类型上下文

这个扩展允许对我们的类型变量有一个直接的约束

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

但它要求用户将约束添加到他们的所有声明中。再次，一个突破性的变化。此外，DatatypeContexts已弃用。

类型家庭

我们可以Get'使用类型族从下面的示例有条件地创建，但由于某种原因，声明类型别名会很高兴地编译。为了得到一个错误，我们需要构造一个这种类型的值，这也是一个突破性的变化。

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
4

1 回答 1

1

I'll start with a solution, then discuss the other possibilities (which appear to not have panned out):

{-# 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

No type families needed, no need to ever drop down to the value level. The type synonyms, however, will compile just fine. Using a type synonym of an invalid Get will lead to a compile time crash at the usage site. I reckon this is as good a solution as you can hope for. Please let me know if anything is unclear.

Next, just some thoughts on the other approaches:

DatatypeContexts

This one will never work: besides being deprecated, all this does is add the constraint to constructors. You specifically indicated you don't want to have to construct anything of the type, so this is pointless. The new GADT syntax fixes this ambiguity - the constraints are now clearly bound to the data or type constructors.

Type Families and TypeError

I believe this should work, and without having to construct a value of the type. (So the following should be fine:)

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

I am motivated to believe this should work based on the example in this trac ticker. Something here is clearly not behaving as it should: even if I replace the call to the type function If with the TypeError itself, still nothing gets triggered - it appears that TypeErrors that aren't top-level still cause some problems.

On the other hand, I am really unsure what the behaviour of TypeError in type synonyms should be, although I'm inclined to say that type API1 = Get 999 should not compile, since type API1 = TypeError (Text "error") doesn't.

于 2016-09-15T07:44:44.190 回答