【发布时间】：2015-01-11 22:59:24
【问题描述】：
我最近一直在玩 Haskell 的 -XDataKinds 功能，并且发现自己想要创建一种。
我不确定我的愿望能否实现，但从 Edward Kmett 的constraints package 看来，似乎有一个声明的类型Constraint（带有排序BOX），据说在GHC.Prim 中定义，但我找不到。
有没有办法在 Haskell 或 GHC 中手动声明一种？这可能需要手动断言使用data 声明的数据类型将是正确的类型。我的想法是这样的：
data Foo :: BOX
data Bar a :: Foo where
Bar :: a -> Bar a
【问题讨论】：
-
DataKinds的使用意味着每个数据声明都会创建一个新的类型，不是吗？例如data Nat = Z | S Nat创建了一个新类型Nat，由Z :: Nat和S :: Nat -> Nat类型居住。 -
没错，但前提是提升的类型是正确的 Haskell98 数据类型。就我而言，我发现自己需要宣传类似于
data Foo (x :: Bar) (y :: Bar) = Foo | ...的东西，其中Bar是一种。这不会使用-XDataKinds进行推广 - 我需要手动 使用相同的名称进行推广。这对于想要推广 GADT 也非常有用。 -
我已经多次阅读您的问题，但在弄清楚您需要/正在提议什么时遇到了一些麻烦。 似乎您要求声明一种新类型，其中包含一些新类型，这些新类型本身就存在于术语级别 - 目前这是不可能的。这是你要求的，还是别的什么？如果是别的东西，一个小的用例会很有启发性。至于推广 GADT，我相信这仍然是一个开放的研究问题。
-
@DanielWagner 你非常接近。我不确定是否需要术语级别的类型（如单例），但我非常想声明一种独立于其类型的类型，然后临时声明类型为先前定义的类型的居民。不清楚，我知道，但如果我可以简单地声明一个种类，然后以不同的表达式创建这种类型的居民类型，那将是理想的。我不确定我是否需要这些类型的术语，但它们也不会受到伤害。理想情况下，我想做
data FooKind :: BOX where，然后是data Bar a :: FooKind where ...。 -
@AthanClark 我想你是在问，除了
k1 -> ... kN -> *和k1 -> ... -> kM -> Constraint之外，是否还有一种方法可以在 GHC 中声明新的开放世界类型。据我所知，答案是“不”。 GHC 中的所有其他类型都是作为（封闭）数据类型的提升而出现的。
标签： haskell dependent-type data-kinds type-kinds