ミュータブルはイミュータブルのサブタイプになれないのはなぜか、あるいはその逆も然りか?
Why isn't mutable a subtype of immutable, or vice versa? (crumbles.blog)
要約
この記事は、プログラミング言語においてミュータブル(変更可能)なデータ構造とイミュータブル(不変)なデータ構造が、なぜ互いのサブタイプ(下位型)になれないのかを解説しています。リスコフの置換原則に基づき、操作の可用性だけでなく、値が変更されないという暗黙の契約の違いが、サブタイプ関係を成立させない根本的な理由であることを説明しています。この問題を解決するために、型クラスやインターフェースのようなアドホックポリモーフィズムのメカニズムがどのように役立つかについても触れています。
全文翻訳
FAQ: ミュータブル型はイミュータブル型のサブタイプになれない、あるいはその逆もしかりなのはなぜか?
イミュータビリティについて学んだ時のことを覚えています。それはすべてを変えました。
様々なプログラミング言語のフォーラムで、ある言語がデータ構造のイミュータブル版とミュータブル版を互いのサブタイプまたはスーパタイプとして提供しないのはなぜか、という議論が定期的に持ち上がります。これは不可能ではありませんが、正式には正しくなく、そうすることで言語が通常提供できる型チェックの保証の少なくとも一部を失うことになります。
これがなぜ機能しないのかを理解するには、サブタイプの定義を覚えておく必要があります。すなわち、Liskovの置換原則です。型 S は型 T のサブタイプであるとは、型 S の値が型 T が期待されるあらゆるコンテキストで使用できる場合を指します。
形式的な事柄を扱う際、この定義は厳密に解釈されます。「あらゆる」は「ほとんど」ではなく、文字通り「あらゆる」を意味します。(置換原則をOOクラスのための単なる推奨デザインパターンとして学んだかもしれませんが、形式的には真のサブタイプはこの基準を満たさなければなりません。)サブタイピングをサポートする静的型システムは、プログラムを型チェッカーに通すために、これを証明する必要があります。
これを説明するために、想像できる最も単純な複合データ構造、つまり素朴なペアを取り上げましょう。以下は、イミュータブルバージョンの操作です。
(cons a d) | a と d を含む新しいペアを構築して返す |
(car p) | ペア p が構築されたときに提供された a の値を返す |
(cdr p) | ペア p が構築されたときに提供された d の値を返す |
これだけです!
ミュータブルバリアントは、さらに2つの新しい操作を追加します。
(set-car! p a) | ペア p 内の a の値を変更する |
(set-cdr! p d) | ペア p 内の d の値を変更する |
(そして新しいコンストラクタもありますが、それは後で扱います。)
さて、イミュータブルペアがミュータブルペアが期待される場所で提供されることはないはずです。ミュータブルペアを必要とする場所は、おそらくこれらの2つの操作のいずれかをそれに使用しようとするでしょうが、これらはイミュータブルペアでは定義されていません。そのため、型エラーが発生します。
しかし、なぜ逆はだめなのでしょうか?イミュータブルペアによって提供されるすべての操作は、ミュータブルペアによっても提供されます。そのため、イミュータブルペアが期待されるあらゆる場所でミュータブルペアを使用できるはずのように思えます。
その理由はより微妙です。置換原則は、型が提供する操作(メソッド)のセットを超えて、それらの操作に伴う暗黙の契約にまで拡張されます。
イミュータブルペアの car または cdr を取得するとき、その結果がそのペアに対して呼び出すたびに常に同じであるという契約に依存できます。この契約は、例えば、その内容に基づいてペアのハッシュ値を安全に計算し、別のデータ構造に保存し、後で取得しようとして再計算するときに値が変わらないことを知ることができることを意味します。(言い換えれば、イミュータビリティはハッシュコンシングの前提条件です!)
このため、イミュータブルペアとミュータブルペアは完全に異なる型でなければなりません。
(icons a d) | a と d を含む新しいイミュータブルペアを構築して返す |
(icar i) | イミュータブルペア i が構築されたときに提供された a の値を返す |
(icdr i) | イミュータブルペア i が構築されたときに提供された d の値を返す |
(mcons a d) | a と d を含む新しいミュータブルペアを構築して返す |
(mcar m) | ミュータブルペア m が構築されたときに提供された a の値を返す |
(mcdr m) | ミュータブルペア m が構築されたときに提供された d の値を返す |
(set-mcar! m a) | ミュータブルペア m 内の a の値を変更する |
(set-mcdr! m d) | ミュータブルペア m 内の d の値を変更する |
i がミュータブルペアであったり、m がイミュータブルペアであったりすると、型エラーになります。
反論: しかし、私はそれをミューテートしていませんし、私のユースケースではイミュータビリティの契約をまったく気にかけていません
2種類のペアはサブタイプ階層を形成しないため、完全に別個の型でなければならず、それぞれに別個の操作セットが定義されます。
幸いなことに、多くの言語はアドホック多相性のメカニズムのいずれかを提供しており、それにより、階層を形成していなくても、複数の型に対して同じ操作を定義できます。Schemerとしては、動的型付けのコンテキストではこれは悪い考えだと思います。なぜなら、データ型の流れについて行う推論をはるかに複雑にし、したがって正しく行うことをより困難にするからです。実際には、ほとんどの言語は、動的型付けか静的型付けかに関わらず、このための何らかのメカニズムを提供しています。
まず静的型付けの場合を考えてみましょう。WadlerとBlottは、アドホック多相性について形式的に推論し、型チェッカーがそれを実際に健全に証明できることを保証するメカニズムを導入しました。彼らの用語では、ミュータブルペアとイミュータブルペアは異なる型ですが、どちらも元の car と cdr を操作として定義する共通のペア型クラスに属することができます。ミュータブルペアでは、これらは基になる mcar および mcdr 操作を参照し、イミュータブルペアでは icar および icdr 操作を参照します。
これは依然として形式的に健全です。なぜなら、ペア型クラスは、ミュータビリティについて何も言わない新しい契約を定義するからです。型クラスの適切な実装では、型システムは、入力型の最も一般的な定義が何らかのペア(ミュータブルまたはイミュータブル)であるメソッドで、ミューテータを使用しようとするのを阻止します。これは、car および cdr 操作を、それらがイミュータブルではない可能性があることを期待して使用することを阻止するものではありませんが、両方向の粒度を明示的に選択することを可能にします。関数の入力型を、関数の契約が実際に期待するものに応じて、ミュータブルペア、イミュータブルペア、またはその両方として宣言できます。サブタイプ関係は一方の方向のみを許可しますが、もう一方は許可しません。関数の型をイミュータブルペアを許可するように宣言できますが、誤ってミュータブルペアを暗黙的に含める可能性があります。あるいは、その逆であれば、ミュータブルペアを許可するが、誤ってイミュータブルペアを含める可能性があります。しかし、どちらの型も(置換原則に違反することなく)一貫して除外することはできません。
型クラスに類似したものは、いくつかの静的型付け言語で利用可能であり、それらはしばしばインターフェース、トレイト、またはロールと呼ばれます。しかし、実際の型システムは、チェックをどれだけ厳密に強制するかにおいて大きく異なります。
動的型付けのオブジェクト指向言語では、これは通常、ダックタイピングの形式で現れます。ここでは、単に異なる複数の型に同じ名前のメソッドを定義し、実行時の型ディスパッチに作業を行わせます。ミューテーション操作の存在または不在を明示的にチェックすることで、関数を呼び出すことを許可する前に、利点を得ることができます。実際には、これはほとんど行われません(特にミューテータの不在をチェックすることは)。そして、これが動的型付け言語におけるアドホック多相性が問題を引き起こしやすい理由です。