白马非马

林一二2024年03月07日 13:12

看到鲍老师的GPT群里聊到白马非马,我想到之前工作中还挺常看到这类报错的,就总结了一下。

公孙龙曾提出他骑的白马有两个特征(白+马形),所以和不允许通行的「马」不是一个东西,因为「马」只有一个特征「马型」。他尝试这么说让官吏予以放行他的马,但官吏表示编译不通过还是没放行。

类型安全中的「白马非马」和「白马是马」

在日常生活中,如果有一个TypeScript的库里的函数接受「马」作为参数,此时你作为使用者想传「白马」给它是没问题的。可以说「白马是马」;而如果有一个函数接受「白马」作为参数,你尝试传「马」进去就会编译不通过,可以说「白马非马」。

协变「白马是马」

这是因为TS支持对象参数「协变」:支持子类赋值给父类,此处「白马」是「马」的子类,「马」是父类。接受「马」作为参数的函数里只会用「马」上的字段,所以只要有「马形」就能取到这些字段,不会在运行时出错。

以公孙龙为例,就是「检测马的官吏流程,也会接受检测马的子类白马」,因为「白马是马」。

逆变「白马非马」

而不支持对象参数逆变:不支持父类赋值给子类。如果方法里要用到「白」提供的参数和方法,那传入只有「马形」的「马」,函数在运行时就取不到所需的字段,就会出错,而编译器会自动发现这种行为,提醒你「白马非马」。但别忘了,在协变的时候,「白马是马」。

逆变「白马是马」

但TS支持函数参数里的对象参数「逆变」:当传入一个函数时,此时就算我们的函数只接受子类「(a:白马)->void」,外面也可以传一个「(a:马)->void」进来。因为我们使用这个函数参数时,就算把一个「白马」对象传给它来调用传入的这个函数,它只用了上面的「马」上的字段也不会报错。

以公孙龙为例,就是「县令要求手下提交检测白马的官吏流程,但县令也会接受检测马的官吏流程」,因为「白马是马」,所以这两种官吏流程都可以用于拦下白马。

实例「某种马非马」

不过日常生活中更常遇到的情况是直接报错

Type '白马' is not assignable to type '某种马'.
  '白马' is assignable to the constraint of type '某种马', but '某种马' could be instantiated with a different subtype of constraint '马'.(2322)
type 马   =  { readonly 0: '0'}
type 白马 =  { readonly 0: '0', readonly a: 'a'}
type 黑马 =  { readonly 0: '0', readonly b: 'b'}

const 一只白马: 白马 = { 0: '0', a: 'a' }

const 检查 = <某种马 extends 马>(a: 某种马 = 一只白马) => `hello!` // error!

解决办法是不要提供默认参数 = 一只白马,删了就好了。报错背后的思想是:假设你这里提供一只白马,你可能就会用它的「白」上的特性来做事。但这个函数的调用方可能会传个黑马进来,即「instantiated with a different subtype of constraint '马'」,这时候你用「白」性的地方就会在运行时出错了。所以根据反证法,这里不应该允许你提供一只白马。

在这个例子里,如果在代码里想用「白」性或者「黑」性,也要做明确的类型判断后再使用。不过「马型」倒是可以直接使用。

马的类型

Lean语言来解释的话:

def 白马 : 马 := 加白 马
def 一只白马 : 白马 := 生成一只新的白马
#check 一只白马  -- 白马
#check 白马      -- 马
#check 马       -- Type
#check Type     -- Type 1
#check Type 1   -- Type 2
#check Type 2   -- Type 3
#check Type 3   -- Type 4
#check Type 4   -- Type 5

可以看到「一只白马」、「白马」、「马」处在不同的类型世界里,它们就不在一个世界里,无法相提并论,无法说「是」和「非」。因为不同世界之间的比对判断是未定义的。也可见Lean的类型宇宙

Code
看到鲍老师的GPT群里聊到白马非马,我想到之前工作中还挺常看到这类报错的,就总结了一下。

公孙龙曾提出他骑的白马有两个特征(白+马形),所以和不允许通行的「马」不是一个东西,因为「马」只有一个特征「马型」。他尝试这么说让官吏予以放行他的马,但官吏表示编译不通过还是没放行。

!! 类型安全中的「白马非马」和「白马是马」

在日常生活中,如果有一个TypeScript的库里的函数接受「马」作为参数,此时你作为使用者想传「白马」给它是没问题的。可以说「白马是马」;而如果有一个函数接受「白马」作为参数,你尝试传「马」进去就会编译不通过,可以说「白马非马」。

!!! 协变「白马是马」

这是因为TS支持对象参数「协变」:支持子类赋值给父类,此处「白马」是「马」的子类,「马」是父类。接受「马」作为参数的函数里只会用「马」上的字段,所以只要有「马形」就能取到这些字段,不会在运行时出错。

''以公孙龙为例,就是「检测马的官吏流程,也会接受检测马的子类白马」,因为「白马是马」。''

!!! 逆变「白马非马」

而不支持对象参数逆变:不支持父类赋值给子类。如果方法里要用到「白」提供的参数和方法,那传入只有「马形」的「马」,函数在运行时就取不到所需的字段,就会出错,而编译器会自动发现这种行为,提醒你「白马非马」。但别忘了,在协变的时候,「白马是马」。

!!! 逆变「白马是马」

但TS支持函数参数里的对象参数「逆变」:当传入一个函数时,此时就算我们的函数只接受子类「(a:白马)->void」,外面也可以传一个「(a:马)->void」进来。因为我们使用这个函数参数时,就算把一个「白马」对象传给它来调用传入的这个函数,它只用了上面的「马」上的字段也不会报错。

''以公孙龙为例,就是「县令要求手下提交检测白马的官吏流程,但县令也会接受检测马的官吏流程」,因为「白马是马」,所以这两种官吏流程都可以用于拦下白马。''

!!! 实例「某种马非马」

不过日常生活中更常遇到的情况是直接报错

```ts
Type '白马' is not assignable to type '某种马'.
  '白马' is assignable to the constraint of type '某种马', but '某种马' could be instantiated with a different subtype of constraint '马'.(2322)
```
```ts
type 马   =  { readonly 0: '0'}
type 白马 =  { readonly 0: '0', readonly a: 'a'}
type 黑马 =  { readonly 0: '0', readonly b: 'b'}

const 一只白马: 白马 = { 0: '0', a: 'a' }

const 检查 = <某种马 extends 马>(a: 某种马 = 一只白马) => `hello!` // error!
```
解决办法是不要提供默认参数 ` = 一只白马`,删了就好了。报错背后的思想是:假设你这里提供一只白马,你可能就会用它的「白」上的特性来做事。但这个函数的调用方可能会传个黑马进来,即「instantiated with a different subtype of constraint '马'」,这时候你用「白」性的地方就会在运行时出错了。所以根据反证法,这里不应该允许你提供一只白马。

在这个例子里,如果在代码里想用「白」性或者「黑」性,也要做明确的类型判断后再使用。不过「马型」倒是可以直接使用。

!! 马的类型

用[[Lean|学Lean]]语言来解释的话:

```lean
def 白马 : 马 := 加白 马
def 一只白马 : 白马 := 生成一只新的白马
#check 一只白马  -- 白马
#check 白马      -- 马
#check 马       -- Type
#check Type     -- Type 1
#check Type 1   -- Type 2
#check Type 2   -- Type 3
#check Type 3   -- Type 4
#check Type 4   -- Type 5
```
可以看到「一只白马」、「白马」、「马」处在不同的类型世界里,它们就不在一个世界里,无法相提并论,无法说「是」和「非」。因为不同世界之间的比对判断是未定义的。也可见[[Lean的类型宇宙]]。