haskell - haskell如何确定隐式foralls中类型变量的顺序？

Question

所以我最近刚刚了解并开始使用 TypeApplications，并且想知道我们如何才能知道我们要分配的类型变量。 The documentation on TypeApplications I found提及:

What order is used to instantiate the type variables?

Left-to-right order of the type variables appearing in the foralls. This is the most logical order that occurs when the instantiation is done at the type-variable level. Nested foralls work slightly differently, but at a single forall location with multiple variables, left-to-right order takes place. (See below for nested foralls).

但是，我没有发现提及如何确定隐式 forall 中类型变量的顺序。我尝试使用 -fprint-explicit-foralls 查看不同的示例，看看是否存在简单的模式，但我在不同版本的 ghci 中得到了不同的结果。 :/

在 ghci 版本 8.0.2 中，我得到:

> :t (,,)
(,,) :: forall {c} {b} {a}. a -> b -> c -> (a, b, c)

在 ghci 版本 8.4.3 中，我得到:

> :t (,,)
(,,) :: forall {a} {b} {c}. a -> b -> c -> (a, b, c)

话又说回来，也许这只是 8.0.2 中 foralls 打印方式的一个错误，因为否则类型应用程序似乎是使用 forall 变量从右到左完成的，这与文档所述相反:

> :t (,,) @Bool
(,,) @Bool :: forall {c} {b}. Bool -> b -> c -> (Bool, b, c)

那么，放入隐式 forall 中的类型变量是否总是按照它们在类型主体中从左到右首先出现的顺序(包括约束)？

Answer 1

TL;DR:类型变量顺序由第一次从左到右的遇到确定。如有疑问，请使用 :type +v。

不要使用:type

使用 :type 在这里会产生误导。 :type 推断整个表达式的类型。因此，当您编写 :t (,) 时，类型检查器会查看

(,) :: forall a b. a -> b -> (a, b)

并使用新的类型变量实例化所有 forall

(,) :: a1 -> b1 -> (a1, b1)

如果您要应用(,)，这是必需的。唉，你没有，所以类型推断几乎完成了，它概括了所有自由变量，例如，你得到，

(,) :: forall {b} {a}. a -> b -> (a, b)

此步骤不保证自由变量的顺序，编译器可以自由更改。

还要注意，它写的是 forall {a} 而不是 forall a，这意味着您不能在此处使用可见类型应用程序。

使用:键入+v

但是当然您可以使用(,) @Bool - 但这里类型检查器以不同的方式对待第一个表达式，并且不执行此实例化/泛化步骤。

您也可以在 GHCi 中获得此行为 – pass +v to :type :

:type +v (,)
(,) :: forall a b. a -> b -> (a, b)
:type +v (,) @Bool
(,) @Bool :: forall b. Bool -> b -> (Bool, b)

看，类型变量周围没有 {…}!

这个订单从哪里来？

the GHC user's guide section on visible type application状态:

If an identifier’s type signature does not include an explicit forall, the type variable arguments appear in the left-to-right order in which the variables appear in the type. So, foo :: Monad m => a b -> m (a c) will have its type variables ordered as m, a, b, c.

这仅适用于具有显式类型签名的事物。推断类型中的变量没有保证顺序，但您也不能将具有推断类型的表达式与 VisibleTypeApplication 一起使用。