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 -> xhas 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

Jeffrey が説明したように、の型付け(function `A -> 1 | _ -> 0)は合理的です。その理由

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

私の意見では、式の後半部分で型チェックに失敗することを説明する必要があります。実際、関数(fun x -> (match x with `B -> ()); x)には入力タイプ[< `B]があり、パラメーター`Bには type があり[> `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 に答える