代码之家 › 专栏 › 技术社区 › Greg Nisbet

ocaml为什么空数组有多态类型?

ocaml

Greg Nisbet · 技术社区 · 6 年前

OCAML数组是可变的。对于大多数可变类型,即使“空”值也没有多态类型。

例如,

# ref None;;
- : '_a option ref = {contents = None}
# Hashtbl.create 0;;
- : ('_a, '_b) Hashtbl.t = <abstr>

但是,空数组没有多态类型

# [||];;
- : 'a array = [||]

这似乎是不可能的,因为数组是可变的。

在这种情况下,它正好可以解决,因为数组的长度不能更改,因此没有机会破坏稳定性。

类型系统中是否有特殊的数组来允许这样做?

2 回复 | 直到 6 年前

ivg 6 年前

答案很简单——空数组具有多态类型,因为它是常量。是特例吗?嗯,有点,主要是因为数组是内置类型,它不表示为ADT,所以是的,在 typecore.ml 在 is_nonexpansive 函数,数组有一个事例

  | Texp_array [] -> true

然而,这并不是一个特殊的情况,它只是一个推断哪些句法表达式形成常数的问题。

注意,一般来说,宽松的值限制允许非扩展表达式的泛化(不仅仅是传统值限制中的句法常量)。其中,非扩展表达式要么是正常形式的表达式(即常量),要么是其计算不具有任何 可观测的 副作用。在我们的例子中, [||] 是一个完美的常数。

OCAML值限制甚至比这更宽松,因为它允许一些扩展表达式的泛化,以防类型变量具有正方差。但这是一个完全不同的故事。

也, ref None 不是空值。一 ref 值本身只是一个带有一个可变字段的记录, type 'a ref = {mutable contents : 'a} 所以它永远不会是空的。它包含一个不可变的值(或者引用不可变的值,如果您愿意的话)这一事实并不能使它成为空的或多态的。一样 [|None|] 这也是非空的。这是单人间的。另外,后者具有弱多态性。

gsg 6 年前

我不相信。用户定义的数据类型也会出现类似的情况,其行为也是相同的。

例如,考虑:

type 'a t = Empty | One of { mutable contents : 'a }

就像数组一样, 'a t 是可变的。但是, Empty 构造函数可以像空数组一样以多态方式使用:

# let n = Empty in n, n;;
- : 'a t * 'b t = (Empty, Empty)

# let o = One {contents = None};;
val o : '_weak1 option t = One {contents = None}

即使存在类型为的值,也可以执行此操作 'a 现在,只要它不处于非宗教立场:

type 'a t = NonMut of 'a | Mut of { mutable contents : 'a }

# let n = NonMut None in n, n;;
- : 'a option t * 'b option t = (NonMut None, NonMut None)

注意的论点 A T 仍然是非变量的,在函数或模块中隐藏构造函数时,您将丢失多态性(大致是因为方差将从类型构造函数的参数中推断出来)。

# (fun () -> Empty) ();;
- : '_weak1 t = Empty

与空列表比较:

# (fun () -> []) ();;
- : 'a list = []