问题标签 [data-kinds]

这有效：

我可以在没有嵌套函数的情况下以某种方式编写 unF 吗？我通常这样做“正确”吗？

我认为我的问题很容易从简单的代码中理解，但另一方面，我不确定答案！直观地说，我想做的是给定一个类型列表 [*] 和一些依赖类型 Foo，生成类型 [Foo *]。也就是说，我想将依赖类型“映射”到基本类型上。

首先，我正在使用以下扩展

假设我们有一些依赖类型

它表征了某个概率分布的样本空间。如果我们想在潜在的异质值上定义产品分布，我们可能会写类似

并补充它

这样我们就可以定义

现在这一切都相当不错，除了 PSampleSpace 的类型会导致一些问题。特别是，如果我们想直接构造一个PSampleSpace，例如

我们必须明确地给它一组生成它或遇到单态限制的分布。此外，由于两个分布当然可以共享一个 SampleSpace（Normals 和 Exponentials 都描述了 Doubles），因此选择一个分布来修复类型似乎很愚蠢。我真正想定义的是定义一个简单的异构列表

并写下类似的东西

其中 mxs 已以某种方式转换为我想要的 SampleSpaces 列表。当然，这最后一段代码不起作用，我不知道如何修复它。干杯!

编辑

就像我所提出的解决方案的问题的一个可靠的例子一样，假设我有这个类

即使它看起来应该输入检查，以下

才不是。GHC 抱怨它

现在我可以使用我的 PDistribution GADT 进行工作，因为我在子发行版上强制使用所需的类型类。

最终编辑

所以有几种方法可以解决这个问题。TypeList 是最通用的。在这一点上，我的问题得到了更多的回答。

为什么用数据类型构建值更难，而与它们进行模式匹配却相对容易？

我正在尝试构建一种数据类型来控制类似于列表的结构，不同之处在于我们可能会向元素添加箭头。此外，我要求某些函数仅在向上箭头和向下箭头的数量正好等于 1 的列表上运行。

在上面的代码中，函数listToChain编译失败，而chainToList编译正常。我们如何修复listToChain代码？

我正在尝试使用类型 [*] 的幻像类型折叠数据。这是我的代码的简化版本

我想要一个折叠运算符

但这不起作用。a和不同的编译器HAppendList a '[]，即使它们不是。

为什么编译不能统一HAppendList a '[]和a？

（虽然我不能在 ghci 中手动折叠:t a !++! b !++! b !++! b => T '[Int]

如果我有一个受有限约束的类型DataKind

和一个存在类型，它忘记了类型中的确切选择K......但在传递的字典中记住了它。

确实是这样ATy <-> Either (Ty A) (Ty B)，但是如果我想写其中一个证人，我需要使用unsafeCoerce

所以一般来说这是可行的——我可以忘记使用的选择K并ATy部分记住使用getATy. 总之，这利用了我可用的尽可能多的类型信息。

但是，如果正确完成，这种类型的信息感觉好像应该是“显而易见的”。

有没有办法在不使用的情况下实现上述目标unsafeCoerce？有没有办法摆脱AK存在主义的束缚？这种技术是否可以完全基于数据类型提供的信息约束来执行？

使用 DataKinds，定义如下

介绍种类KFoo :: BOX和类型TFoo :: KFoo。为什么我不能继续定义

这样CFoo :: TFoo, TFoo :: KFoo, KFoo :: BOX?

是否所有构造函数都需要属于属于该种类的类型*？如果是这样，为什么？

编辑：当我这样做时，我没有收到错误，因为构造函数和类型共享一个命名空间，但 GHC 允许冲突，因为它将名称消除歧义作为常规类型，而不是提升的构造函数。文档说要以 a 作为前缀'来引用提升的构造函数。当我将第二行更改为

我得到错误

错误的类型或类声明头：TFoo

当使用类型族的数据类型时，我发现了一个有趣的情况。

编译器的错误信息是No instance for (C (ID ())) arising from a use of W. 这表明类型族应用程序没有得到充分评估，即使它已经饱和。:kind! ID ()计算结果为()，因此应根据C ()实例使用。

我可以以某种方式强制评估ID ()吗？它是编译器错误吗？

我正在使用 GHC 7.8.3

所以，我在玩HaskellDataKinds并TypeFamilies开始研究生成的 Core GHC。

这是一个小测试用例来激发我的问题：

让我们看一下为eval函数生成的Core

显然，我们需要携带有关a特定分支中可能存在的信息。如果我不对 Datakind 进行索引并且不使用 TypeFamilies，则演员表更容易理解。

它会是这样的：

这个我可以很好理解，TypeFamilies例子中让我困扰的是这部分：

第二行是真正让我感到困惑的地方。分号在那里做什么？这里似乎有点不合适，或者我错过了什么？有没有地方可以读到这个（如果你能推荐的话，我很乐意拿论文）

亲切的问候，

来秋

我正在使用该genifunctors包为定义涉及类型族的类型生成函子实例。

第一个模块定义数据类型本身：

这正如预期的那样工作：

该Functor实例在一个单独的模块中定义：

并给出此错误：

发生这种情况是因为genifunctors，就像 一样geniplate，只能处理来自newtype或data声明的类型构造函数。

这可以通过在递归检查之前规范化类型来解决。

那么，有没有办法在模板 Haskell 拼接中做到这一点？（即在Q单子内？）