Linear is Uniqueness ?

幾つかの言語では線形型システム(Linear type system)を採用することによって、線形型を持つオブジェクトを正確に一度だけ使用するということを型システム上で検査している。 それらの型情報は、メモリ管理、ファイルIOなどの資源に対するアクセスを制限するのに役立つ。 具体的には、破壊的変更による副作用の隠蔽や、静的にメモリを解放することが可能になったりする。 また、似たような概念として、たびたび一意型(Uniqueness type)という存在が提示されるときがある。 この一意型も線形型と同じく、オブジェクトを正確に一度だけ使用するということを保証している。

線形型・一意型はそれぞれ部分構造型システム(Substructural type system)の一種である。 部分構造型システムは、部分構造論理という計算規則に制限を加えた論理体系上で計算される型システムの呼称で、いくらかの言語の型システムには線形型のなどが採用されている*1。 他にも、Affine type system(アフィン型システム)はRustが採用しているなどの理由でよく聞くようになった。*2

これらはそれぞれどういう違いがあるのか、ある程度まとまったので日本語にして書き出してみた。 結果から述べると、オブジェクトがただ一つ存在しているという事実の証明にはどちらを用いても変わりはない。しかし、これらが保証する性能は実行時の計算に役立つことがある。

まず言葉の定義として、オブジェクトが線形性を持つということを、この記事では型システムによって線形型が付けられたこととし、 オブジェクトが一意性を持つということを、この記事では型システムによって一意型が付けられたこととする。 このとき、線形性・一意性は以下のような意味を持つ。

線形性

オブジェクトに対して線形性が認められるとき、"以降にオブジェクトは複製(参照)されない" ということが保証される。つまり、全てのオブジェクトに対して線形性が示された場合、各オブジェクトは一度の使用で破棄をしても問題はないことが保証される。また、非線型のオブジェクトの存在を認めたとき、"以降にオブジェクトは複製(参照)されない" という事実はそのオブジェクトの未来に対する再利用可能性を示す。

一意性

オブジェクトに対して一意性が認められるとき、"以前にオブジェクトは複製(参照)されていない" ということが保証される。つまり、全てのオブジェクトに対して一意性が示された場合、各オブジェクトは一度の使用で破棄をしても問題はないことが保証される。また、非一意のオブジェクトを認めたとき、"以前にオブジェクトは複製(参照)されていない" という事実はそのオブジェクトの過去に対する再利用可能性を示す。


これらの解釈は参考文献*3を基に独自に解釈した部分が混ざっているため、必ずしも正確であることは言えない。もし明らかに異なる言葉の用途や定義などが存在している、または見当違いのことを書いているのを発見した場合はコメント等で指摘してほしい。

*1:ATS2では線形型、Cleanでは一意型によって参照がただ一つということを型システム上で検査している

*2:正しくはRustの前身であるCycloneにおけるRegionにてAffine typeを採用している[要出典]。Rustコミュニティが使っていると示唆する文献は無い

*3:De Vries, Edsko, Rinus Plasmeijer, and David M. Abrahamson. ”Uniqueness typing simplified.” Symposium on Implementation and Application of Functional Languages. Springer Berlin Heidel- berg, 2007.