问题标签 [polykinds]

我有以下类表示类别，其中对象类由一种表示，并且每个 hom 类由由上述种类的类型索引的类型表示。

一个简单的实例示例是：

现在我想为产品类别建模。作为一个简单的起点，这里有一个类型，它对对应于->with 自身乘积的类别的态射进行建模：

下面是相应的操作：

但是当我尝试将操作粘贴到类的实例中时：

我遇到以下问题：

我相信消息的重要部分如下：

特别是它不能将 typeforall x y. Bifunction '(x, y) '(x, y)与 type统一起来forall (a :: (*, *)). Bifunction a a。

剥离大部分领域特定的东西，我们只剩下以下问题的最小重现：

有没有办法可以bifunction_id与bifunction_id'上面统一？

我尝试过的另一种方法是使用类型族，但这仍然不能完全解决问题：

但是我真的不明白为什么这个相同的表达式有效，并且宁愿不必在代码的其余部分中管理像这样的有点不明显的区别。

假设我有一种类型l :: * -> * -> *，例如，我需要应用 2 种类型a，并b获得一个简单类型l a b。

如何将类型映射到与each相同的l :: * -> * -> *新类型？这里不是常数。是否可以？这么想有错吗？m(l) :: * -> * -> *m(l) b al a ba,ba,b

当我正在处理haskell-exercises问题时。Constraint我看到以下代码通过将每种类型应用于约束构造函数来创建聚合。在 GHC 中，深度嵌套的 s 元组似乎Constraint仍然是一种类型Constraint（可能是扁平化的？）。

我尝试使用PolyKinds以下扩展名对其进行概括。

是种'(,) (a :: k) (b :: k)也是种k。往下看，似乎并非如此，所以我想知道为什么All' c (x ': xs) = (c x, All' c xs)首先接受类型族定义（考虑到类型族返回 kind 是r）？

更新

正如@Daniel Wagner 下面已经提到的，(,)这里使用的被认为是Type -> Type -> Type，并且 kind 参数在上面的第二个等式中r被实例化（ ）。事实上，如果我们使用了，它会正确地返回一个类型错误。我能够使用此博客文章中描述的技术进一步确认它，如下所示（使用 kind和实例化）：TypeAll' c (x ': xs) = (c x, All' c xs)'(,)All'k*

我在 Haskell 中研究类型族以更深入地了解这个主题，并尝试同时使用多态类型和类型族。

例如，文件的开头具有以下语言扩展名（文件中的内容比此处显示的要多）：

然后我在类型声明中使用多态类型：

效果很好。但当时我正试图在具有更丰富定义的类型家族中使用它们：

GHC 抛出错误：

有解决办法吗？GHC 版本是 8.10.7。感谢您提前提供任何想法和帮助。

我收到一个错误

我不知道为什么b和约束(Set b, Set s)正在匹配？我希望约束能够存在性地量化 b 类型，但为什么它会匹配它们呢？

我相信在收到错误之前我更改的最后一件事是将 OpOutcome 添加到课程中。

这是代码

编辑：更小的版本，感谢 Krzysztof Gogolewski