问题标签 [polykinds]

polykinded 类型的应用程序是单射的吗？

当我们启用PolyKinds时，我们知道这f a ~ g b意味着f ~ g和a ~ b吗？

动机

在尝试回答另一个问题时，我将问题减少到仅在PolyKinds启用时收到以下错误的程度。

如果多类应用是单射的，我们可以推论c1 ~ c如下。

类型应用是单射的

在 Haskell 中，类型应用程序是单射的。如果f a ~ g b那么f ~ g和a ~ b。我们可以通过编译以下代码向自己证明这一点

类型应用程序不是单射的

类型应用程序的类型不是单射的。如果我们考虑以下，其中有 kind (* -> *) -> *。

我们可以问ghci，(* -> *) -> *当应用于某种类型时，某种类型的东西有什么类型* -> *，即*

这与* -> *应用于某种事物的某种事物相同*

因此，从 借用语法KindSignatures，第一组种类签名暗示第二组中的任何内容是不正确的。

f1和 和有什么不一样f2？

与关于RankNTypes 和 forall 范围的这个问题有关。示例取自 GHC user's guide on kind polymorphism。

我编写了一个Const3与 非常相似的Const新类型，但包含三个给定类型参数中的第一个：

我可以为这种新类型定义很多有用的实例，但我必须自己完成。

但是，我在类型级别应用的函数类似于函数

这@pl告诉我相当于const . const.

两者(.)和const都有匹配的新类型包装器：Compose和Const. 所以我想我可以写：

并自动继承有用的实例，例如：

但 GHC 不同意：

这似乎与和的种类Compose有关Const：

因此，经过一番搜索，我发现有一个名为 GHC 的扩展PolyKinds程序允许我执行以下操作：

好像魔法一样，这些种类是正确的：

但我仍然无法将它们组合起来写Const3 = Compose Const Const。

是什么赋予了？有没有一些聪明的方法可以做到这一点，所以我可以从和继承Functor等实例中获益？ConstCompose

（作为旁注，导致我的最初想法Const3是写：

捕捉到幺半群是单对象类别的想法。如果有一个解决方案仍然允许我以某种方式编写上述实例，那就太好了。）

用户2426021684的评论使我调查是否有可能提出一个类型函数来证明某些和：FF c1 c2 fafa

1. fa ~ f a
2. c1 f
3. c2 a

事实证明，最简单的形式非常简单。但是，我发现很难弄清楚如何编写多种类的版本。幸运的是，我在写这个问题时设法找到了一种方法。

浏览各种包的黑线鳕时，我经常看到类似这样的实例文​​档（Control.Category）：

或者这个（Control.Monad.Trans.Identity）：

亲切的签名到底是什么意思？它没有出现在源代码中，但我已经注意到它似乎出现在使用PolyKinds扩展的模块中。我怀疑它可能就像一个 TypeApplication 但有一种。因此，例如最后一个示例意味着IdentityT如果它的第一个参数有 kind ，它就是一个 monad 转换器*。

所以我的问题是：

• 我的解释是否正确？善意的签名到底指的是什么？
• 首先Category，我怎么知道这k是一种类型而不是类型？还是我只需要知道 arity 的数量Category？
• 与此语法类似的源代码是什么？

我不是要求对种类进行解释。

我遇到了由 Happy 生成的看似无效的代码。问题归结为 GHC 没有为函数推断出多类型签名。这是一个例子：

由于 GHC 正在推断f :: a -> ()where a :: *，因此失败了

我可以打开任何语言编译指示来编译此代码吗？我知道理论上我可以只添加类型签名，但是因为这是由 Happy 生成的代码，我不想手动修改任何内容。

给定以下代码

我收到类型错误（指向行a :: (Monad m ...）

a我可以向with引入一个参数，Proxy t只要我在调用站点上签名，这将起作用：test = a (Proxy :: Proxy A) B但这是我想要避免的。我想要的是

我想使用类型实例t从上下文中找到。Test A m ()考虑到模块将在删除种类注释后编译，似乎应该是可能的PolyKinds， 和A'. k0来自哪里？

我想解决方法是放弃 PolyKinds 并使用额外的数据类型等data ATag; data A'Tag; data BTag。

我可以像这样定义一个多类自然变换：

它适用于所有类型，所以我可以定义例如

这很酷，也很鼓舞人心。但是无论我玩了多少技巧，我似乎都无法在返回类型中得到一些可变参数。例如我想要

这似乎是不可能的，因为类型族需要完全饱和，并且只能在*.

我什至尝试了一些相当讨厌的技巧

而且我不知道这是否有任何希望，因为我还没有考虑过如何“代表”更高级的事物。但是 GHC 知道我在说谎

有没有其他技巧呢？

我正在尝试实现一个多态函数，它本质上遍历一个类型，累积一个Tag值。我希望用户能够做例如rec ((1,2), ('a', 3)).

我已经以各种方式摆弄了这个，并且在当前的化身中得到了错误（对于ab和c，在第一个实例中）：

我对这个错误有点惊讶，因为它似乎表明第二个基本案例实例是在第一个实例的主体中先验选择的。

有没有办法让它工作，或者更好的方法？

我有两个类型族，其中一个将一种类型映射到另一种类型和多态函数的另一种类型：

此代码不使用以下错误消息进行类型检查：

但我不明白歧义来自哪里以及如何指定缺失的种类？

当我只使用一种类型系列时，它可以工作：