问题标签 [constraint-kinds]

是否可以编写一个类型函数来接受像 Show 这样的约束并返回一个将 RHS 约束为不是Show 实例的类型？

签名将类似于

我想表达一个Constraint关于 kind 的类型k -> k -> Type，用英语可以表述为：

一种类型s，使得, forall x x', y, and y'where Coercible x x'and Coercible y y',Coercible (s x y) (s x' y')

或者用更简单的英语：

如果它的两个参数是可强制的，则该类型s始终是可强制的。

后者似乎已经非常接近haskell，而且我有一些看起来确实应该这样做的代码：

然而这不起作用，ghc 想Coercible (s x y) (s x' y')成为一个类型，但它是一个Constraint（ConstraintKinds并且QuantifiedConstraints在）。

我不完全理解发生了什么，但我认为 ghc 不喜欢 aConstraint右侧的=>存在type。由于我可以使用 kind 创建类型别名，Constraint并且可以使用 创建type别名=>，所以没问题。

问题是什么，我如何以它接受的方式向 ghc 表达这种约束？

这是一个关于受约束的多态值的问题，即：类型的值forall f. cxt f => a，哪里cxt是一些约束。

通常，要使用这样的值，我们需要一些具体的约束类型：

现在，直接使用这样的值很简单：

但是，我在实际调用此函数时遇到了麻烦。

给出此错误消息：

尽管x具有所需的类型forall a. c a => b，但 GHC 似乎已尝试x在使用时立即单态化，将c a约束实例化为c a0for unknown a0。显然，这失败了。

相比之下，这个定义很好用：

那么，我怎样才能真正调用一个接受类型参数的函数forall f. cxt f => a呢？

更广泛的背景：

我的最终目标是编写一个函数mapAll，它将类型（或其他类型）到值* -> a的映射提升为从类型列表到值列表的映射[*] -> [a]，即： mapAll :: (All cxt fs) => (forall f. cxt f => a) -> [a]. 在这里，All cxt fs意味着这fs是一些类型的列表，并且cxt f适用于每个f 类型fs（请参阅docs）。如果我使用 aforall f. Dict cxt f -> a而不是 a ，我可以编写这个函数forall f. cxt f => a。

编辑

看起来 usingforall a. c a => Proxy a -> b也可以。现在应该可以完成这项工作，但我会留下这个问题。听起来问题确实是过早的单态化。

作为比较，我之前尝试过 using forall a. c a => () -> b，它给出了与原始示例相同的错误。

最近，我想出了一个想法，即可以在 Haskell 中模拟“交叉类型”。具体来说，我的意思是“接口”的交集，因为它们通常是用 OOP 语言构思的。例如，对具有接口和交集类型的语言使用一些伪代码来了解我的意思：

我希望用 Haskell 类型类做类似的事情。我的方法是用* -> ConstraintHaskell 中的元素替换接口（例如，单参数类型类）：

现在，给定这样的类型类，想法是表单exists a. C a => a（where c :: * -> Constraint）类型的元素对应于“接口”的实现C。给定这样的标识，我们可以通过附加约束轻松构造非匿名交集类型，例如：

问题是，试图概括这一点并使其在[* -> Constraint]“对象”实现的接口列表中通用，我无法让 GHC 推断出它需要什么才能使其正常工作。这是我最近的尝试：

看来我需要做更多的刺激才能让 GHC 在这里最后接受我想要的实例。当我尝试编译上述内容时，出现如下错误：

直观地说，只要是 in就HasName应该成立，因为它是具有约束的存在类型。例如，但是，我不确定如何让 GHC 类型检查器相信这一事实。AbstractType csHasNamecsAbstractType csAll cs aAll '[HasName, HasAge] a = (HasName a, HasAge a)

我也收到如下错误：

因此，看来我的类型级别的实现elem不正确，或者 GHC 无法测试 kind 术语之间的相等性* -> Constraint，所以我不确定当前版本的 GHC 是否可行。

我不断地欺骗自己认为有可能以某种方式（至少模仿）拥有一个类型类，比如说，不受base任意约束

（对于我所有的搜索，我都没有找到任何令人满意的解决来自外部库的约束类型参数的东西）。

TL;DR我如何编写Arrow实例，即使我需要更改MyArr，但必须保留Typeable其值？：

考虑Arrows 的这个定义：

有时我真的希望它是

我想为我上面提到的 GADT 提供它；我的构造函数带有其参数的证明Typeable：

我不能直接为此写一个Arrow实例，因为arrmust beforall a b.并且不能一般地召唤Typeable a. 我认为这是问题的症结所在。

如果我可以编写自己的，我可以使用一个善良的家庭来class Arrow使它工作：ConstraintKinds

但是由于我想保持与proc符号和其他库的兼容性，所以我不能这样做。所以我一直在想我可以以某种方式定义我的 Arrow 的数据类型，利用ConstraintKinds, or 约束, or, reify andreflection

但是我Dict可以将什么传递给实例的定义arr？也许

但是 dangit，这也不起作用，因为arr'sa and b必须是不受约束的

我尝试过让singleton值携带证明或约束a and b的 技巧TypeFamilies，但可惜无济于事。

这些选项之一必须是可能的，对吧？

几个月来，我一直在困惑中扭曲自己，不断地重新审视这个问题，并欺骗自己认为这是可能的。

我收到一个错误

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

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

这是代码

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