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

JoL*_*JoL 15 haskell ghc ghci

所以我最近才了解并开始使用TypeApplications,并且想知道我们如何能够知道我们分配的类型变量.我发现的文件TypeApplications提到:

用什么顺序来实例化类型变量?

出现在foralls中的类型变量的从左到右的顺序.这是在类型变量级别完成实例化时发生的最合乎逻辑的顺序.嵌套的foralls工作方式略有不同,但在具有多个变量的单个forall位置,会发生从左到右的顺序.(见下面的嵌套泡沫).

但是我没有提到如何确定隐式foralls中类型变量的顺序.我试着查看不同的例子,-fprint-explicit-foralls看看是否有一个简单的模式,但我在不同版本的ghci中得到了不同的结果.:/

在ghci版本8.0.2中,我得到:

> :t (,,)
(,,) :: forall {c} {b} {a}. a -> b -> c -> (a, b, c)
Run Code Online (Sandbox Code Playgroud)

而在ghci版本8.4.3中,我得到:

> :t (,,)
(,,) :: forall {a} {b} {c}. a -> b -> c -> (a, b, c)
Run Code Online (Sandbox Code Playgroud)

然后,也许这只是在8.0.2中如何打印foralls的一个错误,因为否则类型应用程序似乎是从右到左用forall的变量完成的,与文档说的相反:

> :t (,,) @Bool
(,,) @Bool :: forall {c} {b}. Bool -> b -> c -> (Bool, b, c)
Run Code Online (Sandbox Code Playgroud)

那么隐式foralls中的类型变量总是按照它们在类型体中首先从左到右出现的顺序(包括约束)?

Joa*_*ner 16

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

不要用 :type

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

(,) :: forall a b. a -> b -> (a, b)
Run Code Online (Sandbox Code Playgroud)

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

(,) :: a1 -> b1 -> (a1, b1)
Run Code Online (Sandbox Code Playgroud)

如果您申请,这是必要的(,).唉,你没有,所以几乎完成了类型推断,它概括了所有自由变量,例如,

(,) :: forall {b} {a}. a -> b -> (a, b)
Run Code Online (Sandbox Code Playgroud)

此步骤不保证自由变量的顺序,并且编译器可以自由更改.

另请注意,它写forall {a}而不是forall a,这意味着您不能在此处使用可见类型应用程序.

使用 :type +v

但是当然你可以使用(,) @Bool- 但是这里类型检查器以不同的方式处理第一个表达式而不执行此实例化/泛化步骤.

你也可以在GHCi中得到这种行为 - 传递+v:type:

:type +v (,)
(,) :: forall a b. a -> b -> (a, b)
:type +v (,) @Bool
(,) @Bool :: forall b. Bool -> b -> (Bool, b)
Run Code Online (Sandbox Code Playgroud)

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

这个订单来自哪里?

可见的应用程序类型的GHC用户指南部分 规定:

如果标识符的类型签名不包含显式forall,则类型变量参数以从左到右的顺序出现,其中变量出现在类型中.因此,foo :: Monad m => ab - > m(ac)将其类型变量排序为m,a,b,c.

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

  • 我提供了一个编辑,试图将您的评论作为答案的一部分. (3认同)