Why the difference in type-inference over the as-pattern in two similar function definitions?

Question

I have the following two similar function definitions:

left f (Left x) = Left (f x)
left _ (Right x) = Right x

left' f (Left x) = Left (f x)
left' _ r@(Right _) = r

When I check the type signatures of the two functions, I am confused by the following types:

ghci> :t left
left :: (t -> a) -> Either t b -> Either a b
ghci> :t left'
left' :: (a -> a) -> Either a b -> Either a b

I suppose left and left' should be of the same type signature, but the haskell's type inference gives me a suprise.

I can't figure out why the type signatures of left and left' are different. Can anybody give me some information? Thanks!

Answer 1

In the second line of left':

left' _ r@(Right _) = r
--      ^^^^^^^^^^^   ^

Since you use an as-pattern, you require the input type to be equal to the return type, since clearly they're the exact same value. left''s type is then restricted to something of the form a -> b -> b.

This restriction then propogates backwards to in turn restrict the function's type – hopefully you can see how; it's not too difficult.

However, in the second line of left, you construct a new value

left _ (Right x) = Right x
--                 ^^^^^^^

The type of this new value has not been restricted, and thus the same problem doesn't occur; it can be something of the form a -> b -> c, which is what you want.

For this reason, the type of left' is more restricted than the type of left, which is what causes their types to be unequal.

为了更具体地说明此概念，我将更精确地向您描述此限制如何向后传播。

我们知道left'签名是形式(a -> b) -> Either a q -> Either b q。但是，第2行规定了Either a q = Either b q，这意味着a = b，因此类型现在变为(a -> a) -> Either a q -> Either a q。

Answer 2

这里的问题是，有些“隐藏”类型会有所不同。类型推断引擎可以在第一种情况下进行推断，而在第二种情况下则不能。

当我们使用

Right :: forall a b. b -> Either a b

我们实际上需要选择什么类型a和b是什么。幸运的是，在大多数情况下，类型推断为我们做出了选择。类型b很容易选择：它是的参数内的值的类型Right。a相反，类型可以是任何东西-推理引擎必须依靠上下文来“强制”选择a。例如，请注意所有这些类型检查：

test0 :: Either Int Bool
test0 = Right True

test1 :: Either String Bool
test1 = Right True

test2 :: Either [(Char, Int)] Bool
test2 = Right True

现在，在您的第一个功能中

left :: (t -> a) -> Either t b -> Either a b
left f (Left x) = Left (f x)
left _ (Right x) = Right x

第一个匹配Right x实际上是Right x :: Either t b，其中隐式类型参数选择为tand b。这使x具有类型b。利用此信息，类型推断将尝试确定second的类型Right x。在那里，可以看到，它的形式应该的Either ?? b，因为x :: b，但是，因为它发生了我们test上面，我们可以使用任何东西的例子??。因此，类型推断引擎会选择另一个类型变量a（一个类型可能是t，但也可能是其他类型）。

相反，在第二个功能

left' :: (t -> t) -> Either t b -> Either t b
left' f (Left x) = Left (f x)
left' _ r@(Right _) = r

我们给模式起一个名字（r）Right _。如上所述，推断具有type Either t b。但是，现在我们使用r右侧的名称=，因此类型推断不必在此推断任何内容，并且可以（实际上必须）简单地重用已经为其推断的类型r。这使输出类型与输入类型相同Either t b，这又迫使f其为type t -> t。

如果这令人困惑，则可以尝试完全避免类型推断，并使用语法Right @T @U选择函数为类型提供显式选择U -> Either T U。（你需要打开ScopedTypeVariables，TypeApplications扩展这一点，虽然）。然后，我们可以这样写：

left :: forall t a b. (t -> a) -> Either t b -> Either a b
left f (Left x) = Left @a @b (f x)
left _ (Right x) = Right @a @b x
                      -- ^^ -- we don't have to pick @t here!

我们也可以

left :: forall t b. (t -> t) -> Either t b -> Either t b
left f (Left x) = Left @t @b (f x)
left _ (Right x) = Right @t @b x

它会很好地工作。GHC更喜欢第一种类型，因为它更通用，可以a是任何类型（包括t，也可以包括其他类型）。

在第二个定义中没有要指定的类型应用程序，因为它r在右侧和左侧重用了相同的值：

left' :: forall t b. (t -> t) -> Either t b -> Either t b
left' f (Left x) = Left @t @b (f x)
left' _ r@(Right x) = r
                   -- ^^ -- can't pick @a here! it's the same as on the LHS