ユニーク性タイプ

コンピューティングでは、一意の型によって、オブジェクトがシングルスレッド方式で使用され、最大でも 1 つの参照しか行われないことが保証されます。値が一意の型である場合、その値に適用される関数は、オブジェクト コード内で値をその場で更新するように最適化できます。このようなインプレース更新により、参照の透明性を維持しながら関数型言語の効率が向上します。一意の型は、関数型プログラミングと命令型プログラミングを統合するためにも使用できます。

一意性型付けは、例を使用して説明するのが最適です。readLine指定されたファイルから次のテキスト行を読み取る関数を考えてみましょう。

関数readLine(File f)は文字列を返す
    戻り行
        文字列行 = doImperativeReadLineSystemCall(f)
    終わり
終わり

ここで、 はOSレベルのシステム コールdoImperativeReadLineSystemCallを使用してファイルから次の行を読み取りますが、この副作用によりファイル内の現在位置が変更されます。しかし、同じ引数でこれを複数回呼び出すと、ファイル内の現在位置が移動するたびに異なる結果が返されるため、参照の透過性に違反します。これにより、が を呼び出すため、参照の透過性に違反します。 readLinedoImperativeReadLineSystemCall

readLineただし、一意性型付けを使用すると、参照透過性のない関数上に構築されていても、参照透過性のある の新しいバージョンを構築できます。

関数 readLine2(unique File f) は (unique File, String) を返します。
    （differentF、行）を返す。
        文字列行 = doImperativeReadLineSystemCall(f)
        ファイルが異なるF = newFileFromExistingFile(f)
    終わり
終わり

宣言uniqueでは、 の型がf一意であることを指定します。つまり、 が戻った後f、 の呼び出し元によって が再度参照されることはなく、この制限は型システムによって強制されます。また、 はそれ自身ではなく、新しい異なるファイル オブジェクト を返すため、 を引数として再度呼び出すことは不可能であり、参照の透明性が維持される一方で副作用が発生する可能性が高くなります。 readLine2readLine2readLine2fdifferentFreadLine2f

一意性型は、 Clean、Mercury、SAC、Idrisなどの関数型プログラミング言語で実装されています。関数型言語では、モナドの代わりにI/O操作を実行するために使用されることがあります。

Scalaプログラミング言語用のコンパイラ拡張が開発されており、アクター間のメッセージ受け渡しのコンテキストにおける一意性を処理するためにアノテーションを使用しています。^[1]

ユニーク型は線形型と非常によく似ており、これらの用語はしばしば互換的に使用されますが、実際には違いがあります。実際の線形型付けでは、非線形値を線形形式に型変換しながら、複数の参照を保持することができます。ユニーク性は、値に他の参照がないことを保証しますが、線形性は、値への参照がこれ以上行われないことを保証します。^[2]

線形性と一意性は、非線形性と非一意性の様相と関連して特に明確に区別されるが、単一の型システムに統合することもできる。^[3]

• リニアタイプ
• 線形論理

• 線形論理に関する参考文献
• 一意性の型付けの簡略化