osiire’s blog

ふしぎなそふとやさん

多相バリアントを使いこなそう(3)

多相バリアント

さて、今日は多相バリアントの「三つの型」について紹介しようと思います。この「三つのの型」をうまく活用する事で、安全さと柔軟さと再利用性を同時に手に入れることができます。

三つの型

同じ`Aと`Bというタグを使っても、宣言できる多相バリアント型には三種類あります。一気に紹介しちゃいましょう。

# type t1 = [ `A | `B ];; (* 固定 *)
type t1 = [ `A | `B ]
# type 'a t2 = 'a constraint 'a = [> `A | `B ];; (* 開いている *)
type 'a t2 = 'a constraint 'a = [> `A | `B ]
# type 'a t3 = 'a constraint 'a = [< `A | `B ];; (* 閉じている *)
type 'a t3 = 'a constraint 'a = [< `A | `B ]

出ました、今までにも幾度か隠れキャラ(古い?)的に登場していましたが説明を保留していた、>記号や<記号です。それぞれの型の正確な意味を自然言語で表現するとこんな感じです。

  • t1の意味
    • `Aと`Bというタグを必ず持ち、それ以外のタグは一切持っていない多相バリアント型。
  • 'a t2の'aの意味
    • 多相バリアント型ならなんでもいいのだけど、列挙されている`Aと`Bというタグは必ず持っていなければならない型。
  • 'a t3の'aの意味
    • 多相バリアント型ならなんでもいいのだけど、列挙されている`Aと`B以外のタグを持っていてはいけない型。

ちょっとややこしいですね。実例をみながら意味を確認してみましょう。まず開いている型から。

# let get_a = function
  `A -> 1
 | _ -> 0;;
val get_a : [> `A ] -> int = <fun>

get_a関数の引数には開いている型[> `A]が推論されました。つまり、get_a関数の引数には、とにかく`Aは必ず持ってなきゃいけないけど、あとはどんなタグがある多相バリアント型でも許容される訳です。例えば、[ `A | `B ]型の値とかはOKです。

# let get_ab = function
  `A -> 1
| `B -> 0;;
val get_ab : [< `A | `B ] -> int = <fun>

get_ab関数の引数には、閉じている型[< `A | `B ]が推論されました。つまり、get_ab関数の引数には、`A,`B以外のタグが含まれる多相バリアント型は、パターンマッチが失敗してしまうので、許されない訳です。例えば、[> `C ]は許されません。

# get_ab `C;;
Error: This expression has type [> `C ] but is here used with type
         [< `A | `B ]
       The second variant type does not allow tag(s) `C

このように、普通のバリアントではとても表現できなかった柔軟な表現が多相バリアント型では可能なのです。

型の大小関係

固定された型、開いている型、閉じている型という三つの型を紹介しました。このような宣言を見ると、だんだん`Aとか`Bとかいうタグが、集合の要素に思えてきませんか？もしそう直観された方がいたら、とても鋭い。実は、固定された型[ `A | `B ]から見ると、要素が必ず等しいか多くなるのが開いた型[> `A | `B ]、要素が等しいか必ず少なくなるのが閉じた型[< `A | `B ]なのです。もし集合の要素が多い方を「大きい」、少ない方を「小さい」と言うのであれば、

閉じた型 <= 固定された型 <= 開いた型

という大小関係が成り立つ事になります。あれ？型の大小関係と言えば？そうです、構造的部分型ですね。閉じた型は固定された型に、固定された型は開いた型にコアーションできます。

# (`A :  [< `A | `B ] :>  [ `A | `B ]);; (* 閉じている -> 固定 *)
- : [ `A | `B ] = `A
#  (`A : [ `A | `B ] :> [> `A | `B ]);;  (* 固定 -> 開いている *)
- : [> `A | `B ] = `A

要点

  • 多相バリアント型には、固定、開いた、閉じたという三種類の型があります。
  • 「閉じた型 <= 固定された型 <= 開いた型」という型の大小関係があります。
  • 大は小を兼ねます。

次回は今回学んだ型の柔軟さを応用して、より安全な多相バリアント型の応用方法を紹介します。

[おまけ]
多相バリアントの閉じた型には、さらにマニアックな指定があります。

# type 'a t4 = 'a constraint 'a = [< `A | `B > `A ];;
type 'a t4 = 'a constraint 'a = [< `A | `B > `A ]

この型の意味は、「多相バリアント型ならなんでもいいのだけど、列挙されている`Aと`B以外のタグを持っていてはいけない上に、`Aというタグは必ず持っている型」となります。いや、もうマニアック過ぎて私も意識して使ったことはないくらいですが、知っていれば立派なオカムラーでしょう。