OCaml で型等式証明子を駆使して「防衛されたメソッド」を実装する

1. 問題の背景と動機

防衛されたメソッドとは？

受信側（self）に対して制約を特定のメソッドだけに適用する機能です。つまり、以下の条件を満たす場合にのみメソッドが呼び出されます：

• 受信側の型が制約（ガード条件）を満たしている場合
• 条件を満たさない場合、コンパイルエラーになる

OCaml は現在、構文的にこの機能を直接定義できませんが、型等式の証明子（witnesses） を用いて実現可能です。

パラメトリック多態性と型制約の問題

Java や OCaml のように実行前に型チェックを行う言語では、クラス全体に型変数への制約を課すことは一般的です。

// 例：T は必ず S のサブタイプであるとする
class MyClass<T extends S> { ... }

問題点：

• この制約はクラス全体に適用されてしまう。
• メソッド単位で柔軟な制約をかけたい場合がある（例：

  flatten

  など）。

具体的な使用例：

MyList

クラス

リスト要素を保存するクラス

MyList<A>

class MyList<A> extends ArrayList<A> {
   public int length() { return this.size(); }
}

ここで、

[[1, 2, 3], [4, 5]]

[1, 2, 3, 4, 5]

flatten

• クラスレベルでの制約の問題：
  • クラス自体に

    <A extends List<A>>

    と設定すると、「常にリストのリストである」と強制されてしまいます。
  • これは非常に制限的で、柔軟性がないためです。

理論的な解決策の 3 つのアプローチ

1. クラスの外へメソッドを移動させる（静的コンテキスト）

   class MyList<A> extends ArrayList<A> {
      public static <A> MyList<A> flatten(MyList<MyList<A>> list) { ... }
      public int length() { return this.size(); }
   }
   

   • 長所： シンプルで特別な儀式が必要ない。
   • 短所： クラス本体と静的メソッドを別々に管理する手間が発生する。オブジェクト指向の「メッセージ送信の体系的アプローチ」が損なわれる。

2. 拡張メソッド（Extension Methods） Kotlin や C# が提供する機能です。

   fun <A> MyList<MyList<A>>.flatten() = ...
   

   • 長所： 既存のクラスへの振る舞い追加が容易で、柔軟性が高い。
   • 短所： メソッド定義をクラス外に置く必要があるため、抽象化の漏洩（leaky abstractions）を招く可能性がある。

3. 防衛されたメソッド（Guarded Methods）

   class MyList<A> : ArrayList<A>() {
      fun length() = size
      // 受信側の型が 'a が list のリストであることを保証する
      fun <B> MyList<MyList<B>>.flatten() = ... 
   }
   

   • 特徴： メソッド定義をクラス内に保持し、抽象化を脱出させない。
   • 利点：
     • 受信側の制約が正確に表現される。
     • メッセージ送りの体系的アプローチが保たれる。
     • クラスメンバーとしての恩恵を受けつつ使える。

2. OOP と FP の対称性

理論と実践の統合

Gabriel Scherer 氏のプレゼンテーション「The Object-Oriented/Functional-Programming symmetry」で示唆されている通り、静的型付け関数型プログラミング（OCaml など）とオブジェクト指向プログラミングには対称性が存在します。

この対称性を理解するために、以下の点を確認します：

• 関数型スタイルの実装（古典的）

  type 'a list = ...
  let rec length : 'a list -> int = ...
  let rec concat : 'a list -> 'a list -> 'a list = ...
  
  let rec flatten : 'a list list -> 'a list = function
    | [] -> []
    | x::xs -> x @ flatten xs
  

• オブジェクト指向スタイルのインターフェース

  class type ['a] olist = object
    method length : int
    method concat : 'a olist -> 'a olist
    method flatten : ??? (* ここをどう定義すべきか？ *)
  end
  

Gabriel Scherer の提案構文

オブジェクト指向の世界で

flatten

method flatten : 'b olist with 'a = 'b olist

• 意味：

  'a

  という型の要素は、実際にはリストのリスト（

  'b olist

  ）である必要がある。
• 一般化：

  method name : ret_type with param1 = val1 and param2 = val2

  のように複数個制約できます。

  // ['a, 'b] t クラスに対し、foo メソッドで a=string, b=int を強制
  method foo : string with 'a = string and 'b = int 
  

OCaml では標準構文として未実装ですが、型等式の証明子を介してこれをコード化することが可能です。

3. OCaml における防衛されたメソッドの実装

基本概念：型等式の証明子（Witnesses）

ジェネラライズされた代数データ型の導入以来、以下のような型等式を示すための直感的な方法が存在します：

type (_, _) eq = 
  | Refl : ('a, 'a) eq

• Refl

  コンストラクタ：

  • (type1, type2)

    という 2 つの型のペアに対して定義できます。
  • しかし、値を構築するには必ず

    type1

    と

    type2

    が型等しい必要があります。
  • 例：

    int

    と別名

    other_int

    を関連付ける際、

    Refl

    を使うことで「実は等しい」という証明を得ます。

    type other_int = int
    let _ : (int, other_int) eq = Refl 
    (* ここに証明が入った *)
    

• 重要なポイント：

  • コンパイル時に型等式が確認できない場合（ランタイム情報や隠された型など）でも有効です。

  • Refl

    をインスタンス化できたということは、構文上は異なる 2 つの型が実際には等しいことを保証しています。

インターフェース定義と制約の適用

リスト向けのオブジェクト API を定義し、

flatten

class type ['a] obj_list = 
  object ('self)
    method length : int
    method append : 'a list -> 'a obj_list
    method uncons : ('a * 'self) option
    method flatten : ??? (* 'a がリストであることを要求したい *)
  end

flatten

'b list

('a, 'b list) eq

method flatten : ('a, 'b list) eq -> 'b list

これで、制約付きのインターフェースが完成しました。次に具体実装を見ていきましょう。

インターフェース

obj_list

の実装

基本メソッドの実装はシンプルです：

let my_list (list : 'a list) = 
  object (self : 'a obj_list)
    val l = list
    method length = List.length l
    method append x = {<l = List.append l x>}
    method uncons = match l with 
      | [] -> None 
      | x :: xs -> Some (x, {<l = xs>})

    method flatten = ???
  end

flatten

メソッドの具体的な実装

リストを再帰的に反復し、要素同士を連結します。ここで重要なのは、

witness

'a = 'b list

method flatten : 'b. ('a, 'b list) eq -> 'b list = 
  let rec aux : type a b. a #obj_list -> (a, b list) eq -> b list =
    fun list witness -> 
      match list#uncons with
      | None -> []
      | Some (head_list, xs) ->
          let flatten_list : b list =
            (* Refl を分解して型等式 'a = 'b list を得る *)
            let () = assert (match witness with 
                | Refl -> true 
              ) in (* ここで型等式が成立すると保証される *)
            head_list
          in flatten_list @ aux xs witness
  in aux self

注釈：

witness

を

Refl

に展開することで、OCaml の型推論が

'a

と

'b list

が同じと判断します。

追加機能：

sum

メソッドの例（整数リスト限定）

特定のメソッド（ここではリストの総和）は、要素が必ず整数であることを制約したい場合があります：

class type ['a] obj_list = 
  object ('self)
    method length : int
    method append : 'a list -> 'a obj_list
    method uncons : ('a * 'self) option
    method flatten : ('a, 'b list) eq -> 'b list
    method sum : ('a, int) eq -> int  (* 'a が int であることを要求 *)
  end

実装は

flatten

('a, int) eq

method sum : ('a, int) eq -> int = 
  let aux : type a. a list -> (a, int) eq -> int = fun list Refl -> 
    List.fold_left (fun acc x -> acc + x) 0 list
  in aux l

テストと型安全性の確認

以下のように呼び出すと正常動作します：

let a = my_list [ [ 1 ]; [ 2 ]; [ 3 ] ] 
(* flatten を呼び出す *)
let _ = assert ([ 1; 2; 3 ] = a#flatten Refl)

let b = my_list [ 1; 2; 3; 4 ] 
(* sum を呼び出す。要素が int であることが保証される *)
let _ = assert (10 = b#sum Refl)

コンパイルエラーになる例：

a

sum

(* これはコンパイルエラーとなる *)
let _ = a#sum Refl 
                  ^^^^
Error: This expression has type (int list, int list) eq
       but an expression was expected of type (int list, int) eq
       Type int list is not compatible with type int

このエラーは期待通りで、制約を無視してメソッドを呼び出そうとしているためです。

4. まとめと考察

防衛されたメソッドの意義

• 問題： オブジェクト指向言語において、メッセージ送信のセマンティクスを保ちつつ、柔軟な型制約をかけることが難しい。
• 解決策： OCaml では標準構文は使えないが、型等式の証明子（witnesses） を介して実装可能である。
• メリット：
  • インターフェース内で受信側の型を厳密に定義できる。
  • 抽象化の漏洩を防ぎつつ、特定の実装（整数リストのみ可算和など）を提供できる。

他言語との比較：Scala のアプローチ

Nicolas Rinaudo 氏が指摘する通り、Scala は類似の機能を実現していますが、型等式の証明子を暗黙的に提供します：

// Scala: 明示的な Refl の書かずに呼び出せる
a.sum // 自動的に型制約が検証される

• OCaml は明示的な

  Refl

  の提供が必要でコードが冗長になりがちですが、その分透明性と制御性があります。
• コードの簡素化とネイティブな言語サポートの両立が理想ですが、現行の OCaml では証明子の操作による実装が有効な手段となります。

結論

OCaml はオブジェクト指向プログラミングを公式には推奨していませんが、型等式の概念を活用することで、防衛されたメソッドを実現できます。これは具体的で実用的なユースケースであり、静的型付け言語における柔軟性と安全性のバランスを取るための興味深いアプローチです。