跟踪约束的技术 [英] Techniques for Tracing Constraints

问题描述

这里是场景：我写了一些类型签名的代码，GHC抱怨不能推导出一些 x 和 y的x〜y 。你通常可以抛出GHC一个骨头，只是添加同构到函数约束，但这是一个坏主意的几个原因：

2. 您可以结束5个约束，其中一个已经足够（例如，如果5由一个更具体的约束隐含）
$

我可以使用这种方法刚刚花了几个小时战斗案例3.我正在玩 语法-2.0 ，我试图定义 share 的与域无关的版本，类似于在 NanoFeldspar.hs 。 p>

我有这个：

  { - ＃LANGUAGE GADTs，FlexibleContexts，TypeOperators ＃ - } 
 import Data.Syntactic 
 
  - 基于NanoFeldspar.hs 
数据让其中
让:: 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让
  

和GHC 无法推导内部a）〜（内部b），这当然不是我要去的。所以，我写了一些代码我不打算（这需要约束），或GHC想要约束，由于一些其他约束我写了。

它结果我需要添加（语法a，语法b，语法（a-> b））到约束列表，没有一个暗示 （内部a）〜（内部b）。我基本上偶然遇到正确的约束;我仍然没有系统的方法找到它们。

我的问题是：

1. 为什么GHC提出了约束？无法在句法中有一个约束 Internal a〜Internal b ，那么GHC从哪里得到？


2. 可以用于跟踪GHC认为需要的约束的起源？即使对于我可以发现自己的约束，我的方法本质上是通过物理地记录递归约束来粗暴强迫违规路径。

解决方案这个方法基本上是无限兔子的约束， / div>

首先，你的函数有错误的类型;我很肯定应该是（没有上下文） a - > （a→b）→ b 。 GHC 7.10在指出这一点有点更有帮助，因为你的原始代码，它抱怨缺少约束
Internal（a - > b）〜（Internal a - > Internal a ）。修复共享类型后，GHC 7.10仍然有助于指导我们：

1. 无法推导（Internal（a - > b）〜（Internal a - > Internal b））




2. 添加上述内容后，我们得到无法推导（sup〜Domain（a→b））




3. 添加完毕后，我们得到无法推导（语法a）， 和无法推导出（句法（a - > b））



4. p>添加这三个后，它终于typechecks;所以我们最终得到

     share ::（Let：< ;: sup，
    Domain a〜sup，
   域b〜sup，
   域（a→b）〜sup，
   内部（a→b）〜（内部a→内部b），
   语法a，语法b，语法（a→b），
   语法N（a→a→b）→b）fi）
    => a  - > （a→b）→ b 
    share = sugarSym Let 
     

所以我想说，GHC在引导我们没有没有用。

对于跟踪GHC从哪里获得其约束要求的问题，您可以尝试 GHC的调试标志，特别是 -ddump-tc-trace ，然后读取生成的日志以查看 Internal（a - > b）〜t （Internal a - > Internal a）〜t 被添加到 Wanted 长读。

Here's the scenario: I've written some code with a type signature and GHC complains could not deduce x ~ y for some x and y. You can usually throw GHC a bone and simply add the isomorphism to the function constraints, but this is a bad idea for several reasons:

1. It does not emphasize understanding the code.
2. You can end up with 5 constraints where one would have sufficed (for example, if the 5 are implied by one more specific constraint)
3. You can end up with bogus constraints if you've done something wrong or if GHC is being unhelpful

I just spent several hours battling case 3. I'm playing with syntactic-2.0, and I was trying to define a domain-independent version of share, similar to the version defined in NanoFeldspar.hs.

I had this:

{-# 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

and GHC could not deduce (Internal a) ~ (Internal b), which is certainly not what I was going for. So either I had written some code I didn't intend to (which required the constraint), or GHC wanted that constraint due to some other constraints I had written.

It turns out I needed to add (Syntactic a, Syntactic b, Syntactic (a->b)) to the constraint list, none of which imply (Internal a) ~ (Internal b). I basically stumbled upon the correct constraints; I still don't have a systematic way to find them.

My questions are:

1. Why did GHC propose that constraint? Nowhere in syntactic is there a constraint Internal a ~ Internal b, so where did GHC pull that from?
2. In general, what techniques can be used to trace the origin of a constraint which GHC believes it needs? Even for constraints that I can discover myself, my approach is essentially brute forcing the offending path by physically writing down recursive constraints. This approach is basically going down an infinite rabbit hole of constraints and is about the least efficient method I can imagine.

解决方案

First of all, your function has the wrong type; I am pretty sure it should be (without the context) a -> (a -> b) -> b. GHC 7.10 is somewhat more helpful in pointing that out, because with your original code, it complains about a missing constraint Internal (a -> b) ~ (Internal a -> Internal a). After fixing share's type, GHC 7.10 remains helpful in guiding us:

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

2. After adding the above, we get Could not deduce (sup ~ Domain (a -> b))

3. After adding that, we get Could not deduce (Syntactic a), Could not deduce (Syntactic b) and Could not deduce (Syntactic (a -> b))

4. After adding these three, it finally typechecks; so we end up with

   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.

这篇关于跟踪约束的技术的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！