首页 文章

追踪约束的技巧

提问于
浏览 次
319

这里's the scenario: I'已经写了一些带有类型签名的代码，并且GHC抱怨无法推断某些 x 和 y 的x~y . 你通常可以将GHC作为一个骨骼并简单地将同构函数添加到函数约束中，但这有几个原因：

  • 它并不强调理解代码 .

  • 你最终可以得到5个约束，其中一个就足够了（例如，如果5个被一个更具体的约束暗示）

  • 如果你做错了或者GHC没有帮助，你最终可能会受到假的限制

我只花了几个小时与案例3作斗争 . 我正在玩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认为需要的约束的起源？即使对于我可以发现自己的约束，我的方法本质上是通过物理写下递归约束来强制违规路径 . 这种方法基本上是一个限制的无限兔洞，是我能想象的效率最低的方法 .

haskell constraints ghc

1 回答

  • 5

    首先，你的函数类型错误;我很确定它应该是（没有上下文） 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

    所以我说GHC在领导我们方面毫无用处 .

    至于关于跟踪GHC获取其约束要求的问题，您可以尝试GHC's debugging flags，特别是 -ddump-tc-trace ，然后读取结果日志以查看 Internal (a -> b) ~ t 和 (Internal a -> Internal a) ~ t 添加到 Wanted 集的位置，但这将是一个相当的长读 .

    回复于

相关问题