问题标签 [unification]

我试图推导出的类型(.) (foldr(++)) (map (:))

我首先推导类型foldr (++)

所以

然后我推导出类型map (:)

所以

最后的类型(.) (foldr(++)) (map (:))

所以我得到

但是如果我问 GHCi:t (.) (foldr(++)) (map (:))我得到(.) (foldr(++)) (map (:)) :: [a] -> [[[a] -> [a]]] -> [[a] -> [a]]

这与我的结果不同，有什么帮助可以得出相同的结果吗？

谢谢，
塞巴斯蒂安。

我试图推导出的类型zipWith . uncurry

zipWith . uncurry = (.) zipWith uncurry-- 串联作为函数

a1用(a3 -> b3 -> c3)和替换我得到c1：[a2] -> [b2] -> [c2]

如果我查询 GHCi:t zipWith . uncurry我得到：(a -> b1 -> b -> c) -> [(a, b1)] -> [b] -> [c]

我认为关键在于，b1 ~ (a2 -> b2 -> c2) ~ (a3, b3) -> c3但我不知道如何将我的结果与预期相匹配。

有什么帮助吗？

谢谢，
塞巴斯蒂安。

我认为我对统一有一个根本的误解。这是我的两个子句：

所以-如果我查询 test(func(X), Y, D)，我希望它只能用第二个子句证明，并且 D 将为 0。这是因为（我认为\我正在尝试）确保在第一个子句中，X 必须等于 X。所以我的查询不应该统一，因为 X 与 Y 不同。我认为 == 测试两个操作数是相同的变量。X 和 Y 显然不是。

但是输出：

所以说如果Y = X，它与第一个子句统一。但是，Y不等于X。我在这里误解了什么？

我不明白为什么q's type isOrd t => [t] -> [a]而不是Ord a => [a] -> [a]

在什么情况下输入类型可能与输出不同？

谢谢，
塞巴斯蒂安。

我试图理解为什么这两个评估：(init . cuts) [1,2,3]并且init . cuts [1,2,3]是不同的，其中：

第一个给出了我期望的结果：[([],[1,2,3]),([1],[2,3]),([1,2],[3])]，但是第二个返回此错误：

我假设，init . cuts [1,2,3] = init (cuts[1,2,3])这是正确的吗？

谢谢，
塞巴斯蒂安。

我正在尝试手动导出类型fun xss = \f -> let ope x y = x . f . y in foldr1 ope xss

F 。是的

\f -> 让操作 xy = x 。F 。是的

foldr1 操作 xss

那么a ~ (b2 -> c2), a ~ (a2 -> b1), a ~ (b1 -> b2) and t4 ~ [a]这似乎是一个错误。

有什么帮助吗？

谢谢，
塞巴斯蒂安。

这里有很多关于推导组合函数的推断类型的线程，但我仍然很困惑。我发现的所有帖子都没有给出关于如何统一类型的一般解释。

我的一份考试学习指南有问题，我无法弄清楚。

8) (.) map uncurry :: ________的推断类型是什么

我大部分时间都能推导出推断的类型，但我仍然有点困惑。例如，我知道要获得 (.) map uncurry 的答案，您需要首先导出 map uncurry 的类型。这是我能做到的

给定以下类型

我用 uncurry 统一了 map 中的函数 (a -> b) 所以

然后答案是 map [a] -> [b] 的另一半，带有 a 和 b 的新值，所以

然后你需要统一

答案应该是

但我不明白 b1 来自哪里或基本上是如何完成的。我认为我真正需要的是对类型统一的一般解释。统一两种类型的方法是什么，我如何知道两种类型不能统一。

如果有人可以逐步解释如何导出 (.) map uncurry，我将不胜感激。

考虑理论

显然，引理可以从prems和显示comp。事实上，乍一看，人们会期望它可以通过

但这只是循环。原因是comp与目标的一种可能的统一是f = (λa. a)and g = (λ x. f (g (h x)))（可以通过使用 看出apply (rule comp)）并且没有取得任何进展。

我知道这是rule代表的有效行为。intro. 然而，从实用的角度来看，我经常遇到简化或引入规则，这些规则在它们匹配的所有情况下都非常有用，除非它们匹配(λx. x)。

有什么办法可以comp说明 Isabelle 的匹配器不会考虑 where for gis的解决方案(λx. x)？

如果不是，为什么不是这种情况的技术和/或理论原因是什么？

给定这个整数的包装器：

我可以执行以下操作：

因为幻影参数会统一。但我想阻止这种统一并导致在线类型错误c。

ST monad 使用 rank2 类型来实现类似的效果。我可能可以通过更改addProxy. 但我特别不想这样做。我想以a某种方式注释类型变量以防止它在addProxy调用中统一。

这在 Haskell 中可行吗？有没有理由说明这种选择会很危险？

编辑：

让我详细说明一个部分解决方案（需要-XScopedTypeVariables）。我可以将上面的代码重写为：

这正确地导致类型错误，c因为a1并且a2无法统一。但这有两个缺点：a不能b在顶层定义；并且您必须明确指定mkProxy.

是否有可能解决这些缺点？

我意识到这是非常基本的，但我无法从 Prolog 教程中解决这个问题，所以我希望这里有人可以帮助我解决我的问题。

如果以下几个条件之一适用，我有一个为真的术语：

所有属性和变量都有一个固定值，如果满足“{}”部分中的任何条件，我想提供“答案” - 但由于某种原因，它不起作用。问题是，如果我只检查其中一个条件，比如第一个条件，它会按预期工作。但我不想复制/粘贴规则 4 次，因为我没有得到一个合乎逻辑的“或”来正常工作。

简而言之，如果我编写了完全不同的代码，第一个条件的意思是：检查Att1是否等于one和Att2是否等于2和Att3是否等于3。如果是这种情况，还要确认Var1等于Var中的值。如果没有，请检查是否可以解决任何其他条件。

编辑：原来我只是有一个';' 代码中太多了。