HN 日本語サマリー

← 一覧へ戻る
プログラミング

OCamlにおけるガード付きメソッド

Guarded Methods in OCaml (xvw.lol)

72 pointsby birdculture7 コメント

要約

OCamlでは、特定のメソッドに対してレシーバー(self)に制約を課す「ガード付きメソッド」を直接定義することは構文上できません。この記事では、型等価性証拠(type equality witness)を用いてこれをエンコードする方法を解説します。ガード付きメソッドは、メソッド呼び出し時にレシーバーが特定の制約を満たす場合にのみ実行可能にする機能であり、型安全性を高める上で有用です。

全文翻訳

ガード付きメソッドは、特定のメソッドに対してのみレシーバー(self)に制約を付与することを可能にし、それによってレシーバーがこれらの制約(これらのガード)を満たす場合にのみ、これらのメソッドを呼び出すことができます。 OCamlは、構文的に、この種のメソッドを直接定義することを許可していません。この記事では、型等価性証拠(type equality witness)を使用して、それらをエンコードする方法を見ていきます。 ガード付きメソッドは、特定のメソッドに対してのみレシーバー(self)に制約を付与することを可能にし、レシーバーがそれらの制約(これらのガード)を満たす場合にのみ、それらのメソッドを呼び出すことができることを意味します。 OCamlは、構文的に、この種のメソッドを直接定義することを許可していません。この記事では、型等価性証拠(type equality witness)を使用して、それらをエンコードする方法を見ていきます。 問題提起 プログラムが実行される前に型チェックが行われる言語(JavaやOCamlなど)が、パラメトリック多相性(Javaのジェネリクス)を導入する場合、型変数を制約することが可能な場合があります。 例えば: class MyClass<T extends S> { ... } ここで、型変数TがSのサブタイプであると仮定して、MyClassをジェネリックにします。 問題は、その制約がクラス全体に適用されることです。 しかし、時には、制約が特定のメソッドにのみ適用されるようにしたい場合があります。 例えば、リストを表すMyListクラスがあるとしましょう: class MyList<A> extends ArrayList<A> { public int length() { return this.size(); } } [[1, 2, 3], [4, 5]]のようなリストを[1, 2, 3, 4, 5]にするflattenメソッドを定義するにはどうすればよいでしょうか? クラスレベルに制約を置くと、リストが「常にリストのリスト」であることを強制することになり、非常に制限的です。 このようなメソッドを実装するには、理論的に3つのアプローチがあります。 メソッドをクラスの外に移動する 最初のアプローチは最も明白です:メソッドをクラス本体の外(例えば、静的コンテキストやコンパニオンオブジェクト)に移動して「ずるをする」ことです: class MyList<A> extends ArrayList<A> { public static <A> MyList<A> flatten(MyList<MyList<A>> list) { // Flattenの実装 } public int length() { return this.size(); } } このアプローチは機能し、特別な儀式を必要としません。 しかし、開発者はどのメソッドがクラス本体にあり、どのメソッドが静的コンテキストにあるかを追跡する必要があります。 さらに、オブジェクト指向プログラミングを支持する主要な議論の1つとしてしばしば提示される、インスタンスにメッセージを送信するという体系的なアプローチを壊します。 拡張メソッド Kotlin(およびC#など)は、拡張メソッドを提供しています。これは、既存のクラスを拡張することを可能にするだけでなく(JavaではfinalであるStringクラスに動作を追加するのに非常に役立ちます)、レシーバーの定義により柔軟性を提供します。 例えば、Kotlinでflattenを次のように書くことができます: class MyList<A> : ArrayList<A> { ... } fun <A> MyList<MyList<A>>.flatten() = ... このソリューションはほぼ完璧に見えますが、メソッドはクラスの外に定義する必要があり、拡張からアクセスできるようにするために、クラスの特定のメンバーをpublicにする必要がある可能性があります(潜在的なリーク抽象のように見えます)。 しかし、それは依然として体系的なメッセージ送信アプローチを維持しながら、レシーバーのより詳細な修飾を可能にします。 ガード付きメソッド 最終的なアプローチは、おそらく最もイデオロギー的です。なぜなら、メソッド定義をクラス内に保持するからです。 それは、エスケープした抽象を強制しません。 これはガード付きメソッドのアイデア、つまりメソッド定義レベルでジェネリックパラメータに制約を追加する機能です。 想像上の構文では(このコードは構文的に無効ではないためコンパイルされますが、意図した効果は得られません): class MyList<A> : ArrayList<A>() { fun length() = size fun <B> MyList<MyList<B>>.flatten() = // Implémentation de flatten } これはクラシックな拡張メソッドと大きく異ならないように見えますが(クラス本体内の構文が十分であることからわかるように)、以前に提起されたすべての問題に対処します: 通常のメソッドよりもレシーバーをより正確に特徴付けることができます 通常のメッセージ送信を壊しません 利用可能なメンバーから引き続き恩恵を受けます(そのため、表現をエスケープしません) ガード付きメソッドは必要であるように思われますが、残念ながら、主流の言語でその定義を許可しているものを私は知りません。 それは非常に残念です。 幸いなことに、OCamlでは、それらをエンコードすることが可能です。 OOP/FP対称性:理論と実践 ガード付きメソッドは一般的なプログラミング言語ではかなり珍しいため、Gabriel Schererによるプレゼンテーション「The Object-Oriented/Functional-Programming symmetry: theory and practice」のスライドを読んでいるときに、その存在をかなり最近発見しました。 このプレゼンテーションは、静的型付き関数型プログラミングとオブジェクト指向プログラミングのツールの間の対称性を示しており、お勧めします。 この対称性は何度も観察および研究されていますが、このプレゼンテーションは包括的でアクセスしやすく(両方の方法論の長所と短所を議論しており、比較的偏りがありません)。 残念ながら、プレゼンテーション中にはカバーされませんでしたが(時間はしばしばプレゼンターの敵です)、ガード付きメソッドに関するセクション全体がスライドに含まれています。 元の例は、古典的な関数型スタイルでのflatten関数の実装との対称的な観察を提供しています: 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 そして、オブジェクト指向の世界にいる場合のflattenメソッドの実装は、このノートで紹介された問題を正確に提示します。 問題は:flattenの型は何であるべきか? class type ['a] olist = object method length : int method concat : 'a olist -> 'a olist method flatten : ??? end 彼はこの構文を提案しています。これはflattenメソッドにガードを意味します: method flatten : 'b olist with 'a = 'b olist この構文はガード付きメソッドを記述することを可能にし、次のように一般化できます: method method_name : return_type with generic_type = other_type. モジュールにおける代入と同様に、andを使用して複数のジェネリックの制約を指定できます。 例えば: method foo : string with 'a = string and b = int 2つの型でパラメータ化されたクラスの場合: class ['a, 'b] t. さらに、この構文は、特定の動作をエレガントに定義することも可能にします。 例えば、私たちのolist型の場合、リストの要素が整数の場合はsumメソッドを提供できます: class type ['a] olist = object method length : int method concat : 'a olist -> 'a olist method flatten : 'b olist with 'a = 'b olist method sum : int with 'a = int end これらすべては驚異的に聞こえますが、残念ながら、この構文はOCamlでは利用できません。 それは腹立たしいです! 心配しないでください、いくつかの小さなツールを使用してそれをエンコードすることが可能です。 OCamlにおけるガード付きメソッド ガード付きメソッドをエンコードするために使用すべきツールについてはかなり明確な考えを持っていましたが、いくつかのコーナーケースに遭遇した後、質問をせず、常に広範に答えるOCamlコミュニティの誰かに電話することにしました:Florian Angeletti、別名Octachron。 (面白い豆知識:octachronはMIDIドラムシーケンサーの名前なので、彼のニックネームをGoogleで検索したところ、提案にはすぐにoctachron ocamlが含まれていました)。 私たちの目標は、特定のメソッドに制約を追加できるようにすることです。これにより、レシーバーの型がそれを満たす場合にのみアクセス可能になります。 言語構文を変更せずに、制約をモデル化することは、追加のパラメータを提供することによってそれを強制することから成ります。 言い換えれば、証拠を提供したいのです。 型等価性証拠を提供する 言語に一般化代数的データ型が導入されて以来、型等価性証拠を定義するためのかなり簡単な方法があります: type (_, _) eq = | Refl : ('a, 'a) eq 唯一のコンストラクタReflを持つeq型は、型チェッカーが知らない型等価性を表現することを可能にします。 Refl値のみを構築できるため、2つの等しい型を関連付けることができます。