代码之家 › 专栏 › 技术社区 › Mark Karpov sheikh_anton

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

data-kinds types haskell

5

Mark Karpov sheikh_anton · 技术社区 · 10 年前

玩高级系统的东西。我想命名为kind和生成此类类型的两个类型构造函数:

{-# LANGUAGE DataKinds #-}

data Subject = New | Existing

在这里,据我所知,我们命名为kind 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

这甚至可以编译。令人困惑的是,数据类型的声明是与数据类型声明不可区分,因此此代码似乎产生数据类型 主题 以及命名的种类 主题 (?) 这会更清楚对我来说,我们可以指定在什么层次上声明事物(种类,和然后 新 和 现有的 是类型构造函数;或类型,然后 新 和 现有的 是以下内容的值构造函数 主题 类型)。我不通过推广一切看起来有效的东西来做出这个设计决定。

现在,我的问题是我不能出口 新 和 现有的 像类型构造函数以在其他模块中使用,例如声明如下内容:

foo :: MyConfig New Dir -> â¦

在同一时间

foo :: MyConfig Int Dir -> â¦

应该是恶意的,不应该编译。

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

module MyModule
  ( New
  , Existing
  -- â¦
  )
where

我得到的:

不在作用域类型构造函数或类New中

不在作用域类型构造函数或类Existing中

GHC手册 section 7.9.3 表示要区分类型和构造函数,可以使用单引号 ' ,所以我尝试:

module MyModule
  ( 'New
  , 'Existing
  -- â¦
  )
where

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

如何导出 新 和 现有的 类型构造函数,以及大多数重要的是,我目前的理解有什么问题吗?

1 回复 | 直到 10 年前

1

5

András Kovács 10 年前

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

module MyModule (Subject(..)) where

data Subject = New | Existing

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

而且,你不需要 DataKinds 在里面 MyModule ,仅在您打算使用提升构造函数的模块中。