如何将约束添加到类型构造函数

Question

请考虑以下数据类型:

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)

但是,这是一个重大变化,需要修改主要版本并重写所有用户的定义.我怀疑限制代码的好处是值得的.

DatatypeContexts

此扩展允许对我们的类型变量进行直接约束

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

Answer 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

我有动力相信这应该基于此 trac 代码中的示例起作用。If这里的某些东西显然没有按其应有的方式运行：即使我用其本身替换对类型函数的调用TypeError，仍然没有触发任何东西 - 看起来TypeErrors不是顶级的仍然会导致一些问题。

另一方面，我真的不确定同义词TypeError中的行为应该是什么，尽管我倾向于说不应该编译，因为事实并非如此。typetype API1 = Get 999type API1 = TypeError (Text "error")