なぜmutableはimmutableのサブタイプになれないのか
Why isn't mutable a subtype of immutable, or vice versa?
immutableとmutableのデータ構造がサブタイプ関係になれない理由を、Liskovの置換原則とpairを例に解説。immutable pairのcar/cdrには「常に同じ値を返す」という暗黙の契約があり、mutable pairはそれを保証できない。そのため両者は別の型として扱う必要があり、型クラスやduck typingによるアドホック多相が代替となる。
immutable pairのcarやcdrを取るとき、そのpairに対して呼び出すたびに結果が常に同じになるという契約に依存できる。この契約のおかげで、例えばpairの内容に基づいてハッシュ値を安全に計算し、別のデータ構造に保存しておき、後で取り出そうと再計算しても値が変わらないと確信できる。(言い換えれば、immutabilityはhash consingの前提条件なのだ!)
HNでの議論
55- js8
説明が過剰に複雑化されている気がする。型は値の性質であり、変数の性質ではない。可変性は変数の性質であり、値の性質ではない。
つまり、これは一種のカテゴリーエラーだ。(ここで、すべてのカテゴリーエラーは圏論における型エラーにすぎない、と冗談を言いたい。)「変数の型」と言うとき、その変数には特定の型の値しか代入(束縛)できないという意味だ。これは、再代入可能かどうか(つまり可変性)とは何の関係もない。
だから、これを説明するのにサブタイピングの概念すら必要ない。
また、変数をその型上のモナドとして定義することもできるだろう。
- bruce343434
つまり、本当に2つの直交する軸がある:
- A: 値を変更できるか
- B: 他の何かが値を変更できるか(予測可能で安定した値に依存できるか)
軸が直交しているため、階層ベースのサブタイピング(継承)は破綻するが、型クラス(インターフェース)、アドホック多相なら機能する。
Cでは、constがAに答える
Rustでは、ポインタエイリアシングの制限(1つのmutポインタ XOR 任意数の読み取り専用ポインタ)により、mutの(欠如が)AとBの両方に答える
- BlackFly
可変性と排他的アクセスを組み合わせれば、ここで提起された(過度に厳格だと一部が言うかもしれない)サブタイピングの定義による反論と、その反論に対する反論の試みの両方を処理できる。不変インスタンスを要求するコードは、不変参照の要求が排他的であるため、可変性を決して観察しない。したがって、可変参照を渡すことはできるが、誰かがその参照を保持している限り、可変性は他のコードにはもはや利用できない。
つまり、可変性 XOR エイリアシングがこの厳格なサブタイピング関係を提供する。もちろん、そのような契約なしでオブジェクトを提供することでこれを緩和する方法も必要になり、内部可変性の世界に入る。そこでは、可変メソッドはサブタイプの一部として理解できる。なぜなら、可変メソッドを持たない参照の保持者は、オブジェクトが変化しないという保証はないと明示的に告げられているからだ。
- Sharlin
全くの余談だが、「head」と「tail」に対する`car`と`cdr`という名前は、率直に言ってコンピューティング全体の中で最も不可解な歴史的遺物の一つだ。
- anankaie
consの例は、実装の詳細(consに渡された値を返す)と意味論(consによってインスタンス化されたこのペアの左側を返す)を混同している。前者の場合、可変性について考えるのはカテゴリーエラーだ。後者では可変性は完全に理にかなっている。
さらに、型をLiskov置換できることを静的に証明するようなインターフェースを構築することは、停止性問題を決定することと等価である可能性が高いと思う。必要なのは、型システムにおける外延的意味論だけだ。