6

OCaml 给出function `A -> 1 | _ -> 0了类型[> `A] -> int,但为什么不是[> ] -> int呢?

这是我的推理:

  • function `B -> 0有类型[<`B] -> int。添加一个`A -> 0分支以使其function `A -> 1 | `B -> 0松散到[<`A|`B] -> int. 该函数在它可以接受的参数类型上变得更加宽容。这是有道理的。
  • function _ -> 0有类型'a -> int。这种类型可以与 统一[> ] -> int,并且[> ]是一个已经开放的类型(非常宽松)。添加`A -> 0分支以使其将类型function `A -> 1 | _ -> 0 限制[>`A] -> int. 这对我来说没有意义。事实上,再添加一个分支`C -> 1就可以了[>`A|`C] -> int,进一步限制了类型。为什么?

注意:我不是在寻找解决方法,我只是想知道这种行为背后的逻辑。

在相关说明中,function `A -> `A | x -> x有 type ([>`A] as 'a) -> 'a,虽然这也是参数的限制性开放类型,但我可以理解原因。'a -> 'a类型应与, [>` ] -> 'b, 'c -> [>`A];统一 这样做的唯一方法似乎是([>`A] as 'a) -> 'a

我的第一个例子是否存在类似的原因?

4

3 回答 3

6

一个可能的答案是该类型[> ] -> int将允许一个参数(`A 3),但这是不允许的function `A -> 1 | _ -> 0。换句话说,类型需要记录`A不带参数的事实。

于 2012-05-26T19:31:03.720 回答
6

原因很实际:
在旧版本的 OCaml 中,推断类型是

[`A | .. ] -> int

这意味着 A 没有参数,但可能不存在。

然而,这种类型是统一的

[`B |`C ] -> int

这导致 `A 在没有任何检查的情况下被丢弃。

它很容易引入拼写错误的错误。
因此,变体构造函数必须出现在上限或下限中。

于 2012-05-28T13:30:00.363 回答
3

的类型(function `A -> 1 | _ -> 0)是合理的,正如 Jeffrey 所解释的那样。之所以

(function `A -> 1 | _ -> 0) ((fun x -> (match x with `B -> ()); x) `B)

在我看来,没有进行类型检查应该由表达式的后半部分来解释。实际上,该函数(fun x -> (match x with `B -> ()); x)具有输入类型[< `B],而其参数`B具有类型[> `B ]。两种类型的统一给出了非[ `B ]的封闭类型。它不能与[> `A ]您从中获得的输入类型统一(function `A -> 1 | _ -> 0)

幸运的是,多态变体不仅仅依赖于(行)多态性。您还可以在某些情况下使用子类型,例如,您想要扩大封闭类型:[ `B ]是的子类型,例如,[`A | `B]它是 的实例[> `A ]。子类型转换在 OCaml中是显式的,使用语法(expr :> ty)(转换为某种类型),或者(expr : ty :> ty)在无法推断出正确的域类型的情况下。

因此,您可以编写:

let b = (fun x -> (match x with `B -> ()); x) `B in
(function `A -> 1 | _ -> 0) (b :> [ `A | `B ])

这是很好的类型。

于 2012-05-27T06:34:30.823 回答