问题标签 [quantified-constraints]

编辑：我跟进了一个更具体的问题。谢谢这里的回答者，我认为后续问题可以更好地解释我在这里介绍的一些困惑。

TL; DR我正在努力将约束证明纳入表达式，同时在构造函数上使用具有存在约束的 GADT。（这是一个严重的嘴，对不起！）

我将一个问题提炼为以下内容。我有一个简单的 GADT，它表示点调用X和函数应用程序调用F。点X被限制为Objects。

Constrained指的是其对象受某物约束的容器，Object即某物。（编辑：我真正的问题涉及约束类别中的Category类）Cartesian

我想写一个表达式：

虽然显而易见的解决方案有效，但在构建更大的表达式时它很快就会变得冗长：

我认为正确的解决方案应该是这样的：

但我仍然无法得到那个证明Object ix Int。

我敢肯定它比我想象的要简单。我已经尝试向类实例Object中的约束族添加约束。GADT我尝试在表达式的签名中提供约束。我试过了QuantifiedConstraints，虽然，我不确定我是否完全掌握它。请有智慧的人帮助我！

可运行：

这是对我之前的问题的跟进。我在那里收到了一些很好的答案，但是，由于我简化了我的实际问题的方式，我认为我误导了回答者，我希望在这里解决这个问题。

TL;DR我有一个类型类Category，constrained-categories它Category使用名为Object. 我想做一个 Free Category，但我很难证明表达式满足Object约束。

考虑我的Free数据类型及其constrained-categories.Category实例：

为了解释更多，让我们也考虑一个Category我可能想要的非自由eval：

我想写一个这样的表达式（这显然比我将在实践中编写的表达式简单得多）：

我可以用明显的方式解决这个问题，但是对于更大的表达式来说这会变得冗长。Object p _想象一下组合元组的函数，并且需要为组合中的每个中间步骤显式地提供一个实例：

我可以选择不抽象Category p, 并且，这行得通：

但我想抽象一下。我应该认为添加一个约束Category p应该起作用，并将其约束纳入范围type Object (Free p) a = Object p a，并给我我需要的任何Object p _实例，但是唉，它不起作用。

在我看来，这QuantifiedConstraints可能会有所帮助，例如forall a. Object (Free p) a => Object p a，但你不能TypeFamily在谓词的头部有 a 。

我也考虑过type Object p :: * -> Constraint在 Conal Elliot 的concat库中使用 like，但是，这将需要不同的库、不同的Category类，而且，上次我使用这种方式限制的类别时，它似乎有点麻烦，我什至没有确定这是否可以解决我的样板问题。该库中的一条评论QuantifiedConstraints表明了 .

可运行

我试图表达一个给定的想法

它应该遵循，只要有实例，任何t1 (t2 ... (tn m))也是。但是，当我尝试将其写下来时，它不起作用：MonadXtxMonadTrans

这会导致以下错误：

有什么办法让它工作吗？