跟踪约束的技术 - 开卷题库

跟踪约束的技术

这是一个场景:我写了一些带有类型签名的代码，GHC抱怨不能为一些x和y推导x ~ y。你通常可以抛弃GHC，简单地将同构添加到函数约束中，但这是一个坏主意，原因如下:

它不强调理解代码。
您最终可以得到5个约束，其中一个约束就足够了(例如，如果这5个约束是由一个更具体的约束暗示的)
如果你做错了什么，或者GHC没有帮助，你就会得到虚假的约束

我刚花了几个小时处理三号病例。我正在使用syntactic-2.0，并试图定义一个与领域无关的share版本，类似于在NanoFeldspar.hs中定义的版本。

我有这个:

{-# LANGUAGE GADTs, FlexibleContexts, TypeOperators #-}
import Data.Syntactic


-- Based on NanoFeldspar.hs
data Let a where
Let :: Let (a :-> (a -> b) :-> Full b)


share :: (Let :<: sup,
Domain a ~ sup,
Domain b ~ sup,
SyntacticN (a -> (a -> b) -> b) fi)
=> a -> (a -> b) -> a
share = sugarSym Let

GHC could not deduce (Internal a) ~ (Internal b)，这当然不是我想要的。所以，要么是我写了一些我不打算写的代码(这需要约束)，要么是GHC因为我写的其他一些约束而想要那个约束。

结果是，我需要将(Syntactic a, Syntactic b, Syntactic (a->b))添加到约束列表中，其中没有一个包含(Internal a) ~ (Internal b)。我基本上是偶然发现了正确的约束条件;我仍然没有一个系统的方法来找到它们。

我的问题是:

为什么GHC提出这个限制?在语法中没有约束Internal a ~ Internal b，那么GHC从哪里拉出来的呢?
一般来说，可以使用哪些技术来追踪GHC认为它需要的约束的起源?即使对于我可以自己发现的约束，我的方法本质上是通过物理地写下递归约束来强制使用违规路径。这种方法基本上是在一个无限的限制条件的兔子洞里，是我能想象到的最低效的方法。

10451

小开

首先，你的函数类型是错误的;我很确定它应该是(没有上下文)a -> (a -> b) -> b。GHC 7.10在指出这一点方面更有帮助，因为在您的原始代码中，它会抱怨缺少约束 Internal (a -> b) ~ (Internal a -> Internal a)。在修复share的类型后，GHC 7.10仍然有助于指导我们:

Could not deduce (Internal (a -> b) ~ (Internal a -> Internal b))

加上上面的内容后，我们得到Could not deduce (sup ~ Domain (a -> b))

添加后，我们得到Could not deduce (Syntactic a)， Could not deduce (Syntactic b)和Could not deduce (Syntactic (a -> b))

添加这三个后，它最终进行类型检查;最后得到

share :: (Let :<: sup,
Domain a ~ sup,
Domain b ~ sup,
Domain (a -> b) ~ sup,
Internal (a -> b) ~ (Internal a -> Internal b),
Syntactic a, Syntactic b, Syntactic (a -> b),
SyntacticN (a -> (a -> b) -> b) fi)
=> a -> (a -> b) -> b
share = sugarSym Let

So I'd say GHC hasn't been useless in leading us.

As for your question about tracing where GHC gets its constraint requirements from, you could try GHC's debugging flags, in particular, -ddump-tc-trace, and then read through the resulting log to see where Internal (a -> b) ~ t and (Internal a -> Internal a) ~ t are added to the Wanted set, but that will be quite a long read.