问题标签 [data-kinds]

我想编写一个分析异构列表的函数。为了争论，让我们有以下

最终目标是编写如下内容

显着位是analyzeRec使用在Rec. 这种基于类的机制有效，但在您必须一遍又一遍地执行此操作的情况下（我会这样做），它会显得笨重且冗长。

singletons所以，我想用基于 - 的机制来代替它。我想写一个函数，比如

但这显然至少在几个维度上是平的。

使用 Singletons 技术在异构列表上编写这样一个函数的“正确”方法是什么？有没有更好的方法来解决这个问题？在解决这类问题时我应该期待什么？

（作为参考，这是一个名为 Serv 的实验性 Servant 克隆。相关文件是Serv.Internal.Header.Serialization和Serv.Internal.Header作为背景。我想编写一个函数，该函数接受标记的标头值的异构列表，然后将headerEncode它们放入实际(ByteString, ByteString)对的列表中。 )

下面的代码不起作用，因为它可以编译。它不应该（直观地）。

1）为什么这段代码编译？

2）我怎样才能“修复”这个程序，以便isKm $ getMeter 1在编译期间拒绝“坏”程序？

使用高级类型系统的东西。我想命名 kind 和几个产生这种类型的类型构造函数：

在这里，据我了解，我们命名了 kindSubject和 type 构造函数 New，Existing它们是:: Subject. 这些类型构造函数不带参数（我打算将它们用作幻像类型），它应该大致相当于：

不同的是，现在我可以写：

这甚至可以编译。令人困惑的是数据类型的声明与数据类型声明无法区分，所以这段代码似乎产生了数据类型Subject以及命名的种类Subject（？）对我来说更清楚的是，我们可以指定我们在哪个级别声明事物（种类，然后New和Existing是类型构造函数；或类型，然后New 和Existing是类型事物的值构造函数Subject）。我没有通过“推广所有似乎可行的东西”来做出这个设计决定。

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

同时在哪里

应该是恶意的，它不应该编译。

这是我尝试导出它们的方式：

我得到什么：

不在作用域类型构造函数或类'New'中</p>

不在作用域类型构造函数或类“现有”中</p>

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

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

如何导出New和Existing键入构造函数，最重要的是，我目前的理解有什么问题吗？

这段代码没有被编译是否有一些原因：

有错误：

但是如果我将类型族定义更改为

它编译好了吗？

(ghc-7.10.3)

我正在使用下面的代码从电话簿中获取联系人姓名

我注意到当有一个没有名字保存的联系人时，上面的代码将返回电话号码作为联系人姓名。我知道这就是 android 的工作方式，以防联系人在没有名字的情况下保存。但是我必须阻止这种行为并强制它返回 null 或空字符串，以防没有“Display_Name”..

可能吗？

我知道我可以Bool像这样提升到善良的水平，Bool可能在哪里True或False：

我想推广()，当然只有一个价值()。但这似乎不起作用：

我想我可以只使用Booland True，但是有没有一种可以提升到 kind 级别的单值类型？

给出错误

Butt是 Kind 变量，而不是类型变量。这是怎么回事？

我正在研究 Haskell 的类型族特性和类型级计算。使用以下方法在类型级别获得参数多态性似乎很容易PolyKinds：

我可以做类似:kind! Bool == Boolor:kind! Int == Int或:kind! Z == Zand的事情:kind! (I Z (S Z)) == (I (S Z) (S (S Z)))。

但是我想使type +临时多态。所以它仅限于我给它的实例。这里的 2 个实例是 kindNatK类型和 kind 类型IntK。

我首先尝试使其参数化多态：

这行得通，我可以做到:kind! (I (S Z) Z) :+ (I (S Z) Z)。

不过我也可以:kind! Bool :+ Bool。这没有任何意义，但它允许它作为一个简单的类型构造函数。我想创建一个不允许此类错误类型的类型系列。

在这一点上，我迷路了。type我尝试了带参数的类型类。但这没有用。

它仍然允许:kind! Add Bool Bool.

这是否与ConstraintKinds扩展有关，我需要将:+or限制Add为某种“类”？

这是我之前提出的问题的后续。现在，我正在尝试修改该toText方法，以便它也可以处理Maybe a重载toText函数。下面是一个编译和工作正常的代码 - 现在，我想重载toText以Maybe a将toText定义本身用于其他类型：

如果我按照以下评论中的指示更新类型的toTextC定义：TTMMaybe

我收到此错误 - 将感谢有关如何解决此重载的指示：

更新1：

按照评论中的建议，我使用附加约束对其进行了修复。但是，它需要UndecidableInstances打开扩展！有没有更好的方法可以在不使用的情况下做到这一点UndecidableInstances？也许某种类型的运算符或函数来表达类型级计算？

尝试基于具有类型级别列表的 GADT 定义模式同义词时出现错误。

我设法把它归结为这个例子：

给我：

这是一个错误，还是我做错了什么？