问题标签 [data-kinds]

在 Haskell 中玩弄DataKinds，我生成了以下代码，它实现并滥用了一些类型级别的一元 nat：

当我尝试在 GHC 8.2.2 中编译它时，我收到以下类型错误：

这无疑是对 GHC 8.0.1 中发生的情况的改进，在 GHC 8.0.1 中它编译得很好，然后在运行时失败：

似乎在 GHC 8.2.2 中，unNat采用了一个(IsNat (Pred n))未出现在类型签名中的隐式约束：

我有什么办法可以打电话unNat来实现类似的东西predSuccIsNat吗？

与 GHC 的 DataKinds 混在一起，我尝试实现类型级二进制 nats。它们很容易实现，但是如果我希望它们在常见情况下有用，那么 GHC 需要相信Succ类型族是单射的（因此类型推断至少与一元类型级别一样有效纳特）。但是，我很难说服 GHC 就是这种情况。考虑以下二进制 nat 的编码：

GHC 无法接受这一点，因为它无法判断这Succ1是单射的：

我们认为它是单射的，因为通过检查Succ1,One永远不会出现在它的形象中，所以Bit0 (Succ1 x)case 永远不会返回Bit0 One，因此Bit1case 永远不会与 case 冲突One。同样的论点（“One不在”的形象中Succ1）表明它Succ本身也是单射的。然而，GHC 还不够聪明，无法找到这个论点。

所以，问题：在这种情况下（以及类似的情况），有没有办法让 GHC 相信内射型家族实际上是内射的？（也许是一个类型检查器插件，我可以在其中提供一个反转 Succ1 的函数？也许是一个编译指示说“尝试从这个系列向后推断，就好像它是单射的；如果你遇到任何歧义，你就可以崩溃”？）

我试图写下Category（^{有限维自由）}向量空间，但我似乎无法说服 GHC 任何给定长度的索引向量都是Applicative.

这就是我所拥有的：

向量是带有长度参数的列表

要获得类别，我们需要矩阵乘法。明显的实现使索引与我们通常想要的有点倒退。

编辑

在@Probie 的帮助下，我设法解决了前面的问题，这足以为Semigroupoids定义一个实例

但是我在定义时遇到了与以前类似的问题Category.id：

Applicative (Vec n)我现在不需要凭空召唤一个Finite n.

似乎没有办法为此需要一个附带条件。

结束编辑

对于上下文，这是我以前的，Vec n是归纳的Applicative

要获得类别实例，我们需要重新排列a索引后面...

但是如果不重新排列其中一个术语，就无法重新排列索引本身......

然而：

我有以下类型类

但是，我不断收到错误消息：不在范围内：数据构造函数'Bool'。Haskell 是否出于某种原因不允许这样做，或者是否包含数据构造函数？如果不是，为什么不呢？

我可以union在 Haskell 中有一个类型安全的联合（如 C 中的）吗？这是我尝试过的最好的，这里Variant以 C++ 命名std::variant：

这会产生如下错误消息：

我不明白这种歧义是如何出现的。

我在实现代表嵌套数组中值结构的IsList实例时遇到了麻烦。GADT这是完整的代码：

我看到这样的错误：

我部分理解为什么我有这个错误。但我想知道是否可以IsList为类型实现实例Val？

我想让 Fortran 中的子例程和函数支持实数的单精度和双精度，以及各种变量的其他类型，与 Fortran 中的内在函数相同。如果 x 是双精度，sin(x) 会给我们正弦函数的双精度值，而单精度是 x 是单精度。

我编写了以下测试，并声明了我的常量 a64 和 b64 并将它们与它们的 kind 值 (8) 相关联。如果输入变量 a 和 b 为双精度，我希望我的函数divide_real输出双精度结果，如果输入为单精度，则输出单精度。这可以通过将 rk 参数包含为函数的输入来实现，但编译器抱怨 rk 未声明或者是不简化为常量表达式的变量（GNU 编译器）。

关于如何让它工作的任何提示？

查看来自freer-simple的示例代码

我不明白 Eff '[Console, IO] 中好奇的 '[...] 来自哪里。

我知道它为解释器声明了一个效果列表，但它在哪里声明？

我浏览了库的源代码，但看不到任何我认为是“构造函数”的东西。

它是 Haskell 的一个特性吗？它来自低级的 type-fu 库吗？

对其目的更严格的描述是什么？

我想从一个类型到值如下，但不使用折旧的 DatatypeContexts：

如果使用这种或其他方法（Peano 数等），我不太担心；要求是能够仅从类型信息中构造值。

谢谢！

基本上我已经创建了一个具有三个属性的类型，我们称之为“Foo”

每个属性都是 3 个值之一，我用这种格式声明了每个属性：

现在，在对何时使用“数据”或“类型”之间的区别进行了一些猜测之后，我尝试制作 Foo 的 2D 列表：

编辑：当我组装这个列表时，我也会遇到同样的错误

这在编译时导致两个主要错误：

和

我在哪里错了？我或多或少地尝试跟随 learnyouahaskell 到发球台，但无论我尝试了多少种方法，我都会不断收到类似的错误。