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 回答