【问题标题】:How does Haskell's type system generate this error?Haskell 的类型系统是如何产生这个错误的?
【发布时间】:2019-10-22 12:29:33
【问题描述】:

在我通过 Haskell 进行的冒险中,我发现当我在代码中的类型出现错误时,我很难解析我做错了什么并且编译器会抱怨。我认为这是因为在编译器发现错误之前进行了部分类型推断。

当然,我习惯于类型不匹配非常明显的语言。例如类似于function foo expects an argument of type int, but received string 的东西。很明显这意味着什么,我传入了一个字符串,但签名需要一个 int。

所以这里有一些相对简单的代码,它是一个函数,在给定一系列系数和幂的情况下计算多项式:

poly :: [Int] -> [Int] -> Double -> Double
poly a b x = sum . map (\(ai, bi) -> ai * (x ** bi)) . zip a $ b

这会产生以下编译器错误输出:

[1 of 1] Compiling Main             ( solution.hs, solution.o )

solution.hs:11:56: error:
    • Couldn't match type ‘Int’ with ‘Double’
      Expected type: [Double] -> [(Double, Double)]
        Actual type: [Double] -> [(Int, Double)]
    • In the second argument of ‘(.)’, namely ‘zip a’
      In the second argument of ‘(.)’, namely
        ‘map (\ (ai, bi) -> ai * (x ** bi)) . zip a’
      In the expression: sum . map (\ (ai, bi) -> ai * (x ** bi)) . zip a
   |
11 | poly a b x = sum . map (\(ai, bi) -> ai * (x ** bi)) . zip a $ b
   |                                                        ^^^^^

solution.hs:11:64: error:
    • Couldn't match type ‘Int’ with ‘Double’
      Expected type: [Double]
        Actual type: [Int]
    • In the second argument of ‘($)’, namely ‘b’
      In the expression:
        sum . map (\ (ai, bi) -> ai * (x ** bi)) . zip a $ b
      In an equation for ‘poly’:
          poly a b x = sum . map (\ (ai, bi) -> ai * (x ** bi)) . zip a $ b
   |
11 | poly a b x = sum . map (\(ai, bi) -> ai * (x ** bi)) . zip a $ b
   |                                                                ^

所以我已经知道这里出了什么问题。 ab[Int] 类型,但我需要它们是 [Double] 类型。但是,我不明白的是为什么编译器会说它是什么:

  1. a 在表达式中出现在b 之前并且同样错误时,为什么它会抱怨b
  2. 在最上面的错误中,预期的类型是[(Double, Double)]。酷,有道理。但是 actual 类型怎么会是[(Int, Double)]?如果ab 都是[Int],那么双重是如何出现的?

无论哪种情况,我认为我真正需要的是有人指导我了解类型系统最终是如何生成这些错误的,这样我才能更好地理解为什么错误消息是这样的。

【问题讨论】:

  • 编译器恰好首先发现b 有一个矛盾的类型。这完全是武断的,但可能是因为它通过函数应用程序向后工作(f a b = (f a) b。)至于为什么它不抱怨a,——既然知道有错误,为什么还要更进一步?
  • 感谢@AJFarmar,它的任意性对我来说已经足够了。我有一种感觉,要么是这种情况,要么递归堆栈以b而不是a开头。都好。但是,我仍然对为什么看到 [(Int, Double)] 感到困惑。
  • 出于同样的原因。它可能通过这些功能向前或向后工作。 ai\ (ai, bi) -> ai * (x ** bi) 中第一个应用的类型,因此只有应该受影响的类型才有意义。再一次,这和抱怨b 一样武断。
  • @AJFarmar 谢谢。所以,这里的想法是编译器首先捕获b,无论出于何种原因,并且由于它尚未到达a,它假设它会是Double,如果正确的话,不知道如果它处理了a,那也是错误的(因为一旦我们发现错误就没有理由继续前进)?
  • 但它没有先捕获b。它捕获zip a。然后它继续运行并且还捕获了b

标签: haskell


【解决方案1】:

a 在表达式中出现在b 之前并且同样错误时,它为什么抱怨b

...为什么不呢?你自己说他们都错了。 GHC 也发现他们都错了。它告诉你他们都错了。此外,a 并没有真正出现在“之前”,因为在 Haskell 中没有“之前”和“之后”的真正概念。如果有的话,它是“进出”,而不是“左右”,然后b(仅在($)下方)是a“之前”(在zip下方,(.) ($))。反正没关系。

在最上面的错误中,预期的类型是[(Double, Double)]。酷,有道理。但是为什么实际类型是[(Int, Double)]?如果ab 都是[Int],那么双重是如何出现的?

sum . map _etc . zip a 应该具有类型 [Int] -> Double,因为类型签名并且因为它是 ($) 的左侧。钻得更深,zip a 应该是[Int] -> [(Double, Double)]。它实际上是forall b. [b] -> [(Int, b)]。使用参数类型,我们可以选择设置b ~ Int,从而推导出zip a实际上是[Int] -> [(Int, Int)](这是真的)在预期[Double] -> [(Double, Double)]的地方,或者我们可以选择设置b ~ Double(来自返回类型)并确定实际上是zip a :: [Double] -> [(Int, Double)]也是正确的)。两种方式都会出错。事实上,我认为 GHC 正在以第三种方式做到这一点,类似于第一种方式,但我不会详细说明。

问题的核心是:在 Haskell 程序中,如果您知道表达式周围或其中的内容的类型,则有多种方法可以确定表达式的类型。在类型良好的程序中,所有这些推导彼此一致,而在类型错误的程序中,它们通常以多种方式不一致。 GHC 只是选择了其中两个,以一种希望是有意义的方式称它们为“预期的”和“实际的”,并抱怨他们不同意。在这里,您发现第三个推导也与“预期”推导相冲突,但 GHC 出于某种原因,选择不将您的推导用于“实际类型”。选择要显示的派生并不容易,尤其是在 Haskell 中,允许一切都影响其他一切的类型,尽管它肯定会更好。几年前,GHC 的一位领导者在更好的错误消息上做了some work,但它似乎有轻微的链接腐烂——Haskell-analyzer 桥似乎已经从互联网上腐烂了。

如果您遇到这样的错误,我首先建议您不要使用_ . _ . ... $ _ 样式书写。如果您将其写为_ $ _ $ ... $ _,则更容易遵循我的主要建议。我不会在这里改变它,但你应该记住这一点。

poly :: [Int] -> [Int] -> Double -> Double
poly a b x = sum . map (\(ai, bi) -> ai * (x ** bi)) . zip a $ b

您会看到一个错误,但并不清楚要更改什么。很好,干脆放弃尝试破译象形文字并用_ 替换部分RHS。您删除的 RHS 越多,发现错误的机会就越大,如果您将其全部删除,则会达到约 95%:

poly a b x = sum . map (\(ai, bi) -> ai * (x ** bi)) . _ $ _
-- personally, I'd nuke the scary-looking map _lambda, too,
-- but I'm also trying to keep this short

GHC 会告诉你左边的__a -> [(Double, Double)],右边是_a。添加zip:

poly a b x = sum . map (\(ai, bi) -> ai * (x ** bi)) . zip _ $ _

你会被告知你需要两个[Double]s,你会意识到使用ab不起作用,因为a, b :: [Int](而GHC实际上在错误中说a :: [Int]; b :: [Int]消息,因为有时不清楚)。然后你想办法解决它:

poly a b x = sum . map (\(ai, bi) -> ai * (x ** bi)) . zip (fromIntegral <$> a) $ fromIntegral <$> b

一切都好。

【讨论】:

  • 您能否详细说明您喜欢_ $ _ $ _ $ _ 而不是_ . _ . _ $ _ 样式的意思?我敢说后者更像是惯用的 Haskell 风格,作为一种普遍趋势。
  • 因为zip a b 是一个概念单元,但您已将其拆分为两个遥远的部分:(_ . (_ . zip a)) $ b。你最终需要两个_ 孔来覆盖错误,即使那样你也会得到像_ :: a0 -&gt; [(Double, Double)] 这样的奇怪输出。新的a0 变量是“glue”:它是显示两个孔之间关系的名称。你用一个洞,你会得到一个更好的_ :: [(Double, Double)]
  • @HTNW 如果您将zip a b 视为一个概念块,则很容易通过sum . map foo $ zip a b 将其保留为_ . _ . _ $ _ 样式。 (当然,在这种情况下sum $ zipWith foo a b 会更好,并且两种风格都有!)
  • @DanielWagner 但是你又回到了你开始的地方!如果错误实际上在foo 中,或者您不应该使用map,则错误消息会再次转移。对我来说,简单的事实是这里有一个线性结构:zipab,然后是mapfoo,然后是sum。这由_ $ _ $ _ 反映,而_ . _ $ _ 总是引入人工分支:将(sum after map foo)应用到(zip a b)。
【解决方案2】:
  1. 当表达式中的 a 出现在 b 之前并且同样错误时,为什么它会抱怨 b

嗯,有两个错误。它抱怨zip a,它抱怨b。它会按照它们在源代码中出现的顺序发出这些错误。

  1. 在最上面的错误中,预期的类型是[(Double, Double)]。酷,有道理。但是实际类型怎么会是[(Int, Double)]?如果ab 都是[Int],那么双重是如何出现的?

没那么快。该错误中的实际类型不是[(Int, Double)]。它说zip a 是错误的,它说预期类型是[Double] -&gt; [(Double, Double)],而实际类型是[Double] -&gt; [(Int, Double)]。这与预期类型为 [(Double, Double)] 而实际上类型为 [(Int, Double)] 的表达式不同。

zip a 是一个函数。我们知道它应该返回[(Double, Double)](因为组合链的其余部分会处理从poly 返回最终的Double 结果。

函数zip a 的剩余参数必须是[Double] 类型(zip 类型)才能使返回类型适合[(Double, Double)],这很好; zip a 可以接受[Double] 参数。

问题是zip a不是[Double] -&gt; [(Double, Double)]类型的函数;它可以管理的最接近的是[Double] -&gt; [(Int, Double)],因为在表达式zip a 中使用了a。所以这就是错误所抱怨的。

你在问为什么它不抱怨[(Int, Int)] 而不是[(Int, Double)],因为如果你将zip a 应用到b 就会得到这样的结果。但是您的代码中没有任何地方这样做!您将整个函数sum . map (\(ai, bi) -&gt; ai * (x ** bi)) . zip a 应用于b(通过$ 运算符)。类型错误不是抱怨zip a b 是错误的列表类型,而是抱怨zip a 是错误的函数类型。

然后它分别抱怨$ 运算符的第二个参数是也是错误类型作为参数传递给整个函数(其中zip a 是一小部分) ,但这是与其他错误完全不同的问题。


Haskell 在类型检查期间所做的是查看每个表达式(包括子表达式,在每个嵌套级别),并进行比较:

  1. 表达式必须具有的类型,以适应其上下文(它称之为“预期类型”)
  2. 表达式基于其组件的类型(它称之为“实际类型”)

你可以大致认为这个例子中的过程如下:

  1. sum . map (\(ai, bi) -&gt; ai * (x ** bi)) . zip a $ b 必须导致 Double,因为 poly 的类型签名
  2. 第一个子表达式是$ 应用于sum . map (\(ai, bi) -&gt; ai * (x ** bi)) . zip a
    1. $ 具有类型 (a -&gt; b) -&gt; a -&gt; b(实际类型)1
    2. 我们知道上面的b必须是Double,最终的预期返回类型为poly,所以$应该是(a -&gt; Double) -&gt; a &gt; Double(预期类型)的形式
    3. $ 的预期和实际类型统一没有问题
  3. 现在我们知道sum . map (\(ai, bi) -&gt; ai * (x ** bi)) . zip a 的预期类型是a -&gt; Double 的形式。让我们检查它的实际类型:
    1. 该组合链中的第一个子表达式是.,应用于sum(sum .) 在运算符部分表示法中,或(.) sum 在前缀表示法中):
      1. . 具有 (b -&gt; c) -&gt; (a -&gt; b) -&gt; a -&gt; c 类型;它在这个位置的预期类型是(b -&gt; Double) -&gt; (a -&gt; b) -&gt; a -&gt; Double
      2. sum 的类型为 (Foldable t, Num a) =&gt; t a -&gt; a;它在这个位置的预期类型是b -&gt; Double(需要Num Double:✔)
      3. 所以(sum .) 的类型为Foldable t =&gt; (a -&gt; t Double) -&gt; a -&gt; Double
    2. 组合链中的下一个子表达式是(sum .),应用于map (\(ai, bi) -&gt; ai * (x ** bi)) . zip a
      1. map (\(ai, bi) -&gt; ai * (x ** bi)) . zip a 预计适合 Foldable t =&gt; a -&gt; t Double。让我们检查它的实际类型:
        1. 它的第一个子表达式是. 应用于map (\(ai, bi) -&gt; ai * (x ** bi))
        2. . 的类型为 (b -&gt; c) -&gt; (a -&gt; b) -&gt; a -&gt; c;它在这个位置的预期类型是Foldable t =&gt; (b -&gt; t Double) -&gt; (a -&gt; b) -&gt; a -&gt; t Double
        3. 所以map (\(ai, bi) -&gt; ai * (x ** bi)) 应该适合b -&gt; t Double
        4. 略过细节,map (\(ai, bi) -&gt; ai * (x ** bi)) 实际上具有 [(Double, Double)] -&gt; [Double] 类型(因为从 poly 的签名中已知 x 具有 Double 类型)。
        5. 这符合预期的类型b -&gt; t Double,并告诉我们b 实际上是[(Double, Double)]t 实际上是[](需要Foldable []:✔)
      2. 所以现在我们知道.的实际类型应用于map (\(ai, bi) -&gt; ai * (x ** bi))(a -&gt; [(Double, Double)]) -&gt; [Double],这意味着.的第二个参数,即zip a,应该是@的形式987654416@。让我们检查它的实际类型:
        1. zip[a] -&gt; [b] -&gt; [(a, b)] 类型
        2. a 的类型为 [Int],来自 poly 的类型签名
        3. 所以zip a 的类型类似于[b] -&gt; [(Int, b)]。试图统一预期类型和实际类型迫使我们将b 实例化为Double,而将zip a 的实际类型留给[Double] -&gt; [(Int, Double)]。但是现在没有更多类型变量可以实例化。这是我们发现的第一个实际类型与预期类型不匹配的地方。所以我们发出一个类型错误。在报告类型错误时,我们保留b 被实例化为Double 的事实,因为这并没有错。所以预期类型显示为[Double] -&gt; [(Double, Double)],实际类型显示为[Double] -&gt; [(Int, Double)]
        4. 进一步深入zip a 没有什么意义,因为子组件没有有意义的预期类型,因为我们不知道我们刚刚报告的问题是否是预期类型错误或者实际类型是错误的(我们只知道它们不可能都是正确的)。我们不能说问题是zip 不适合[Int] -&gt; [Double] -&gt; [(Double, Double]),还是a 不适合[Double],或者zip a 实际上是否正确,问题是上下文期待@ 987654438@.
      3. 但是回过头来假装zip a确实符合它的预期类型,我们确定map (\(ai, bi) -&gt; ai * (x ** bi)) . zip a具有“实际类型”[Double] -&gt; [Double],它与我们预期的Foldable t =&gt; a -&gt; t Double类型一致
    3. 这意味着sum . map (\(ai, bi) -&gt; ai * (x ** bi)) . zip a 具有实际类型[Double] -&gt; Double,它与我们预期的a -&gt; Double 类型一致(我们现在知道aDouble)。
  4. 最终允许我们进入下一个顶级表达式,即(sum . map (\(ai, bi) -&gt; ai * (x ** bi)) . zip a $)应用于b
    1. b 应该有 [Double] 类型
    2. b 实际上有 [Int] 类型(由 poly 的签名)
    3. 这是我们的第二个实际类型和预期类型不匹配的地方,所以我们报告第二个类型错误。

1 但不是它的 actual 实际类型。说$只是一个类型为(a -&gt; b) -&gt; a -&gt; b的函数其实是一种简化,因为$需要支持unlifted类型之类的东西,而普通类型变量是无法支持的。但我不打算在这里讨论。这种简化在 99% 的情况下都有效。


您可以看到,要弄清楚类型系统如何生成这些错误,需要执行大量步骤。所以我真的不认为这是一个有助于理解类型错误的过程。

编译器精确地指出了它所谈论的确切表达式:无论是在解析树的下降方面,所有这些“in the second argument of (.)”行,还是(通常更有帮助)在下面使用^^^^ 字符的图形指示。

所以第一步是考虑“为什么那个表达式应该是那种类型”,看看周围的环境。在这种情况下,很清楚为什么zip a 应该 具有[Double] -&gt; [(Double, Double)] 类型;结果被输入最终产生Double的数学运算,因此列表中元组的两个元素都必须是Doublezip a的参数也必须是[Double]

第 2 步是思考“为什么那个表达式实际上会有那种类型”。同样,这更加明显。如果a :: [Int],那么zip a 不可能产生适合_ -&gt; [(Double, _)] 的东西。

编译器在验证导致这些错误的上下文中的所有其他内容时所经历的挑剔的细节大多是无关紧要的;它有效地告诉你一切都很好(不会在那里发出任何类型错误)。

为什么它首先发现zip a而不是b,或者为什么它抱怨zip a是一个导致[(Int, Double)]的函数而不是抱怨a[Int]类型也无关紧要。从根本上说,它只是找到一个预期类型和实际类型不一致的地方,没有任何方法可以判断哪个是正确的(通常两者都不是)。

这些东西可以理解的,并且随着您使用编译器的时间越长,它们变得相当直观,但是这些事实很少能真正帮助您理解和修复错误。只需选择它报告的第一个错误,专注于它正在谈论的表达式,思考为什么上下文会导致它具有报告的“预期类型”,以及为什么表达式的子部分会导致它具有报告的“实际类型”。

与 GHC 以高深莫测的错误消息而闻名的名声相反,我实际上发现它们的质量比我在使用其他语言时通常得到的要高得多。当您不熟悉它们时,它们以新格式包含大量信息,因此它们会令人困惑。但是一旦你熟悉了它们,它们实际上是非常好的。

事实上,这个特定的错误消息完全符合您所期望的function foo expects an argument of type int, but received string!只是“函数 foo”是 . 运算符(您在同一行使用了两次,因此它可以准确识别它正在谈论的那个),它所期望的参数是另一个具有复杂类型的函数。它看起来比您与之比较的错误消息类型更复杂的唯一原因是它将预期/实际部分分成两行以提高可读性(并准确指出这两种类型中的哪一部分不匹配!)并给出您详细说明了哪个子表达式包含错误,而不仅仅是说line 11: function (.) expects an argument of type [Double] -&gt; [(Double, Double)], but received [Double] -&gt; [(Int, Double)]

【讨论】:

  • 这是一个非常深入的答案。错误可能是如何产生的描述很好,但后半部分确实有助于巩固我对问题的一般理解。
【解决方案3】:

拥有

poly :: [Int] -> [Int] -> Double -> Double
poly a b x = sum . map (\(ai, bi) -> ai * (x ** bi)) . zip a $ b

,一方面,

    a ::        [ Int]
zip a :: [t] -> [(Int,t)]
x :: Double
x ** bi :: Double
     bi :: Double
                      t ::    Double
zip a   :: [Double] -> [(Int, Double)]                     derived

,但另一方面,

poly a b x          ::                      Double
sum                 ::          [Double] -> Double
    ai * (x ** bi)  ::           Double
   (ai ,       bi)  ::  (Double, Double)
zip a   :: [Double] -> [(Double, Double)]                  expected

【讨论】:

    猜你喜欢
    • 1970-01-01
    • 1970-01-01
    • 1970-01-01
    • 2017-10-17
    • 1970-01-01
    • 1970-01-01
    • 2012-06-29
    • 2011-10-27
    • 1970-01-01
    相关资源
    最近更新 更多