问题标签 [constraint-kinds]

我搜索了 Hackage，找不到类似以下的内容，但它似乎相当简单且有用。是否有包含某种数据类型的库？

我发现的所有 HList 都可以具有任何类型，并且不受限制。

如果没有我会上传我自己的。

我想为具有指向可以解除超类约束的字典的静态指针的类型编写一个类型类。在这个人为的例子中，超级约束是Typeable，因为现代 GHC 版本会自动为所有类型提供实例。

实际上，超级约束是非平凡的，并且Static a允许这些约束的字典被序列化的实例，因为forall a. StaticPtr a可以被序列化。

首先，以下代码编译没有问题，

但是当我使用静态指针以所需的方式编写类时，

GHC 抱怨静态表单主体中的类型应用程序：

然后我尝试让 GHC 完全自行解析实例，而不使用Lifting引导类型检查器

但这也失败了，

一个更单态的实例也会失败，并出现非常相似的错误No instance for (Static a)：

这让我更多地了解了 GHC 的类型类实例解析是如何工作的：类的超级约束直到实例被实际解析后才会应用。但是 GHC 能够满足Dict :: Static a => Dict (Static a)第一个示例，这显然需要一个Static a实例在范围内。

如果可能的话，有什么建议如何写这个吗？希望对约束包有更多经验的人可以提供正确的扭曲来满足类型检查器。

下面的代码片段从Haskell wiki 借用了一个类型类字典和一个存在类型：

是否可以编写一个f :: (forall x. x -> result) -> result能够将Showable构造函数（或任何其他存在类型的数据构造函数）作为参数的函数？

一次失败的尝试如下所示：

正如我上面评论的导入所暗示的那样，我的印象是约束包可能允许我传递必要的证明，但我看不出它是如何工作的？

要找出一个类型是否是更高种类的类型，ghci 提供：

并尝试了类型类，如：

为什么我可以在 typeclass 上要求更高种类的类型？约束是什么意思？

I understand the following type family shouldn't and perhaps can't be implemented in GHC:

This is problematic because classes are open, so MatchesConstraint c a could evaluate to True for some parts of the program and False in others depending on what instances are in scope, which I imagine could be potentially quite disastrous.

But consider the following:

This seems quite safe. In some parts of our program we might fail to reduce if an instance is not in scope, but we'll never have an inconsistency.

Can I make something like this work in GHC?

The reason I'm asking for this, is because one could perhaps select instances based on not just type directly but class. Which could be a useful thing in some contexts I believe.

怎么能代表空约束？

对于以下文件

ghc 8.2.2 答案

我想念什么？

我知道以下解决方案

但我想知道为什么 () 不起作用

在使用 ConstraintKinds 和 TypeSynonymInstances 时尝试使用 GHC 8.6.1 编译小型 Haskell 文件时出现意外错误。

我想做一个以类为参数的类，我想在编写实例时使用别名。这是代码：

该错误令人惊讶，因为据我所知，FooBar它具有预期的类型，即* -> Constraint，但编译器表示应该为其提供一个参数。

正如我在这里尝试的那样，甚至可以在实例声明中使用约束别名吗？如果是这样，我如何理解看似矛盾的错误信息？

（我知道我可以简单地声明FooBar为一个类而不是别名，但我真的不想这样做，因为我还想要一个实例，那时我必须拉入UndecidableInstances。）

以下代码段使 GHC（使用 8.6.2 和 8.4.4 检查）在编译期间卡住：

我认为它被卡住了，因为tGHC 试图找到C T，这导致F T C通过类型族扩展F回C T，这就是它正在寻找的（无限循环）。

我想理论上 GHC 可以说它C T从自身达到了它的要求，并且任何依赖于自身的东西都可以递归地工作，还是我误解了什么？

旁注：在我偶然发现这种行为的真实示例中，我能够实现我想要的，而编译器不会被替换为UndecidableSuperClasses卡住Data.Constraint.Dict。

我想有一个更高种类的空约束。

假设我有以下课程：

现在我想为函数创建一个实例，这样它就不会以任何方式约束元素。我该举个什么例子Obj？

假设：导致Constraints 的类型族总是分布在它们的representational参数上。

例如，Fam x Eq `And` Fam x Show相当于Fam x (Eq `And` Show)ifFam的第二个参数具有代表性。

问题：

• 上述假设真的正确吗？有没有参考？
• GHC 是否允许利用此规则转换等效约束？