haskell - 跟踪約束的技巧



constraints ghc (1)

首先,你的函數有錯誤的類型; 我很確定它應該是(沒有上下文) a -> (a -> b) -> b 。 GHC 7.10在指出這一點時更有幫助,因為用你的原始代碼,它會抱怨缺少約束Internal (a -> b) ~ (Internal a -> Internal a) 。 確定share類型後,GHC 7.10仍然有助於指導我們:

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

  2. 添加上面後,我們得到Could not deduce (sup ~ Domain (a -> b))

  3. 添加後,我們得到Could not deduce (Syntactic a)Could not deduce (Syntactic b)Could not deduce (Syntactic (a -> b))

  4. 加入這三個之後,它終於敲定了; 所以我們結束了

    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的調試標誌 ,特別是-ddump-tc-trace ,然後通過結果日誌讀取Internal (a -> b) ~ t -ddump-tc-trace(Internal a -> Internal a) ~ t被添加到Wanted集中,但這將是相當長的一段時間。

以下是這種情況:我寫了一些帶有類型簽名的代碼,GHC抱怨無法為xy推出x〜y。 您通常可以將GHC投入骨骼,並簡單地將同構添加到函數約束中,但出於以下幾個原因,這是一個糟糕的主意:

  1. 它不強調理解代碼。
  2. 最終可以有5個約束條件,其中一個條件就足夠了(例如,如果5條約定有一個更具體的約束條件)
  3. 如果您做錯了某些事情,或者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) 。 我基本上碰到了正確的約束。 我仍然沒有系統的方法來找到它們。

我的問題是:

  1. GHC為什麼提出這個約束? 在句法上沒有任何限制Internal a ~ Internal b a〜 Internal a ~ Internal b ,那麼GHC從哪裡來拉?
  2. 一般來說,可以使用哪些技術來追溯GHC認為需要的約束的起源? 即使是我可以發現自己的限制,我的方法基本上是通過物理寫下遞歸約束來強制違規路徑。 這種方法基本上是沿著一個無限的兔子洞的約束,並且是我能想像到的效率最低的方法。




ghc