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

Question

使用高级类型系统的东西。我想要命名 kind 和 a几个生成此类类型的类型构造函数:

{-# LANGUAGE DataKinds #-}

data Subject = New | Existing

据我了解，在这里，我们命名了 kind Subject 和类型构造函数新和现有是::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 是类型构造函数；或类型，然后新建和 Existing 是 Subject 类型事物的值构造函数)。我不通过“推广一切似乎有效的东西”来做出这个设计决策。

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

foo :: MyConfig New Dir -> …

同时在哪里

foo :: MyConfig Int Dir -> …

应该是恶意的并且它不应该编译。

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

module MyModule
  ( New
  , Existing
  -- …
  )
where

我得到了什么:

Not in scope type constructor or class ‘New’

Not in scope type constructor or class ‘Existing’

GHC 手册 section 7.9.3说要区分“类型和构造函数”，可以使用单引号 '，所以我尝试了:

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

…但现在这是一个解析错误。

<小时/>

如何导出 New 和 Existing 类型构造函数以及大多数重要的是，我目前的理解有什么问题吗？

Answer 1

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

module MyModule (Subject(..)) where

data Subject = New | Existing

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

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