如何在使用DataKinds扩展时导出类型构造函数？

Question

玩弄高级类型系统的东西。我想要一个命名的类型以及一些生成该类型的类型构造函数：

{-# LANGUAGE DataKinds #-}

data Subject = New | Existing

据我理解，这里我们定义了一个名为Subject的类型和两个叫做New和Existing的构造函数，它们都是类型构造器:: Subject。这些类型构造器不需要参数（我计划将它们用作幽灵类型），大致相当于：

{-# LANGUAGE EmptyDataDecls #-}

data New
data Existing

现在我可以写出以下内容：

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE GADTs          #-}
{-# LANGUAGE KindSignatures #-}

-- …

data MyConfig :: Subject -> * -> * where
  MyConfig
    { mcOneThing :: Path t File
    } :: MyConfig k t

这段代码甚至可以编译。令人困惑的是，数据种类的声明与数据类型声明无法区分，因此此代码似乎会生成命名为Subject的数据类型和命名为Subject的数据种类（?）。如果我们可以指定在哪个级别上声明事物（种类，然后New和Existing是类型构造函数;或者类型，然后New和Existing是Subject类型的值构造函数），那么这将更清晰明了。我不理解这种“提升一切看起来可行的”设计决策。

现在，我的问题是我无法将New和Existing导出为类型构造函数以在其他模块中使用，例如声明以下内容：

foo :: MyConfig New Dir -> …

同时，在哪里

foo :: MyConfig Int Dir -> …

代码应该是有缺陷的并且不能编译。

以下是我尝试导出它们的方法：

module MyModule
  ( New
  , Existing
  -- …
  )
where

我所得到的：

类型构造函数或类‘New’不在作用域内

类型构造函数或类‘Existing’不在作用域内

GHC手册在第7.9.3节中指出，为了区分“类型和构造函数”，可以使用单引号'，所以我尝试：

module MyModule
  ( 'New
  , 'Existing
  -- …
  )
where

...但现在出现了解析错误。

---

我该如何导出New和Existing类型构造函数，最重要的是，我的理解有什么问题吗？

- Mark Karpov

Answer 1

使用常规的语法导出构造函数：

module MyModule (Subject(..)) where

data Subject = New | Existing

目前，提升的构造函数和未提升的构造函数是绑定在一起的，因此我们只能一起导出/导入它们。

此外，在MyModule中不需要使用DataKinds，只需要在打算使用提升的构造函数的模块中使用。

- András Kovács

---

换句话说，晋升的构造函数永远不会被导出 - 只有在您导入它们的任何地方才会晋升普通构造函数。 - leftaroundabout