多态变体和类型签名 [英] Polymorphic variants and type signatures

问题描述

(这是多态变体和 let%bind 类型错误的扩展/提炼)

考虑以下代码:

版本 1:

let x : [>`Error1 ] = (`Error1 : [> `Error1 ])让 y : [>`错误1 |`错误2] = x

版本 2:

let x : [>`Error1 ] = (`Error1 : [ `Error1 ])让 y : [>`错误1 |`错误2] = x

版本 1 类型检查，但版本 2 失败(我用 4.09.0 编译):

文件test.ml"，第2行，第33-34个字符:2 |让 y : [>`错误1 |`错误2] = x^错误:此表达式的类型为 [`Error1]但是期望类型为 [> 的表达式.`错误1 |`错误2]第一个变体类型不允许标记`Error2

注意这个错误出现在y的定义中，但是x的签名在两种情况下是一样的！y 怎么能看到x 的定义?关于 x 的类型检查信息是否比其签名更多?

解决方案

简而言之，显式类型注释不是类型签名.特别是在

let x : [>`Error1 ] = (`Error1 : [ `Error1 ])

x 的类型是 [ `Error1 ].

问题的根源在于显式类型注解中的统一类型变量可以与具体类型统一.

你的问题的一个更简单的例子是

let f: 'a ->'a = 乐趣 x ->× + 1

这里，'a ->'a 注释与实际类型 int->int 统一，因此此代码类型检查.如果你想让类型变量'a通用，你需要通过添加一个显式的通用量化来更加明确

让 f: 'a.'a ->'a = 乐趣 x ->× + 1

<块引用>

错误:此定义的类型为 int ->int 比'一种.'a ->'一种

同样的现象发生在你的带有隐式行变量的代码中:

let x : [>`Error1 ] = (`Error1 : [ `Error1 ])

这个注解不保证x的类型是[>;`Error1] 但只能与 [> 统一；`错误1].并且由于类型 [ `Error1 ] 可以与 [> 统一；`Error1 ]，没有理由提出错误.

和以前一样，如果你想避免这个问题，你需要明确说明哪些变量在你的注释中被普遍量化:

let x : 'row.([> `Error1 ] as 'row) = (`Error1 : [ `Error1 ])

<块引用>

错误:此表达式的类型为 [ `Error1 ]但是期望类型为 [> 的表达式.`错误1]第二个变体类型绑定到通用类型变量'a，它不能关闭

(This is an extension / distillation of Polymorphic variants and let%bind type error)

Consider the following code:

Version 1:

let x : [> `Error1 ] = (`Error1 : [> `Error1 ])
let y : [> `Error1 | `Error2 ] = x

Version 2:

let x : [> `Error1 ] = (`Error1 : [ `Error1 ])
let y : [> `Error1 | `Error2 ] = x

Version 1 typechecks, but version 2 fails (I'm compiling with 4.09.0):

File "test.ml", line 2, characters 33-34:
2 | let y : [> `Error1 | `Error2 ] = x
                                     ^
Error: This expression has type [ `Error1 ]
       but an expression was expected of type [> `Error1 | `Error2 ]
       The first variant type does not allow tag(s) `Error2

Note that this error occurs in the definition of y, but the signature of x is the same in both cases! How is it that y can see inside the definition of x? Is there more typechecking information about x than its signature?

解决方案

In brief, explicit type annotations are not type signatures. In particular, in

let x : [> `Error1 ] = (`Error1 : [ `Error1 ])

the type of x is [ `Error1 ].

The root of the issue is that unification type variables in explicit type annotations can be unified with concrete types.

A simpler instance of your problem is

let f: 'a -> 'a = fun x -> x + 1

Here, the 'a -> 'a annotation is unified with the real type int->int and thus this code typechecks. If you want to make the type variable 'a universal, you need to be more explicit by adding an explicit universal quantification

let f: 'a. 'a -> 'a = fun x -> x + 1

Error: This definition has type int -> int which is less general than
'a. 'a -> 'a

The same phenomenon happens with your code with the implicit row variable:

let x : [> `Error1 ] = (`Error1 : [ `Error1 ])

This annotation does not guarantee that the type of x is [> `Error1] but only that it can be unified with [> `Error1]. And since the type [ `Error1 ] can be unified with [> `Error1 ], there is no reason to raise an error.

As before, if you want to avoid this issue, you need to be explicit about which variables are universally quantified in your annotation:

let x : 'row. ([> `Error1 ] as 'row) = (`Error1 : [ `Error1 ])

Error: This expression has type [ `Error1 ]
      but an expression was expected of type [> `Error1 ]
      The second variant type is bound to the universal type variable 'a,
      it cannot be closed

这篇关于多态变体和类型签名的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！