サブ構造型システム

部分構造型システムは、部分構造論理に類似した型システムのファミリーであり、1つ以上の構造ルールが存在しないか、制御された状況下でのみ許可されます。このようなシステムは、状態の変化を追跡し、無効な状態を禁止することで、ファイル、ロック、メモリなどのシステムリソースへのアクセスを制限できます。 ^{[1] : 4}

交換、弱化、縮小の 構造ルールの一部を破棄することで、いくつかの型システムが出現しました。

• 順序付き型システム(交換、弱化、および縮小を破棄): すべての変数は、導入された順序で正確に 1 回使用されます。
• 線形型システム(交換は許可するが、弱化や縮小は許可しない): すべての変数は 1 回だけ使用されます。
• アフィン型システム(交換と弱化は許可するが、縮小は許可しない): すべての変数は最大 1 回使用されます。
• 関連する型システム(交換と縮小は許可するが、弱化は許可しない): すべての変数は少なくとも 1 回は使用されます。
• 通常の型システム(交換、弱化、縮小を許可): すべての変数を任意に使用できます。

アフィン型システムの説明は、「変数の 各出現は最大で 1 回使用される」と言い換えると最もよく理解できます。

順序付き型は、交換、縮小、弱化が破棄される非可換論理に対応します。これは、スタックベースのメモリ割り当てをモデル化するために使用できます（ヒープベースのメモリ割り当てをモデル化するために使用できる線形型とは対照的です）。^{[1] ：30〜31}交換プロパティがない場合、オブジェクトはモデル化されたスタックの先頭にある場合にのみ使用でき、その後はポップオフされるため、すべての変数は導入された順序で正確に1回使用されます。

線形型は線形ロジックに対応し、オブジェクトが正確に一度だけ使用されることを保証します。これにより、システムはオブジェクトの使用後に安全に解放することができます。 ^{[1] : 6}また、リソースが閉じられたり、別の状態に移行したりすると使用できなくなることを保証するソフトウェアインターフェイスを設計することもできます。^[2]

Cleanプログラミング言語は、一意性型（線形型の変形）を利用して、同時実行性、入出力、配列のインプレース更新をサポートします。^{[1] : 43}

線形型システムでは参照は許可されますが、エイリアスは許可されません。これを強制するために、参照は代入の右側に現れた後はスコープ外となり、一度に 1 つのオブジェクトへの参照のみが存在することが保証されます。関数への引数として参照を渡すことは代入の一種であり、関数パラメータには関数内で値が割り当てられるため、このような参照の使用もスコープ外となることに注意してください。

単一参照特性は、量子状態の複製不可定理を反映しているため、線形型システムを量子コンピューティングのプログラミング言語として適したものにしている。圏論の観点からは、複製不可定理とは、状態を複製できる対角関数が存在しないという主張である。同様に、組合せ論理の観点からは、状態を破壊できるKコンビネータは存在しない。ラムダ計算の観点からは、変数は項に1回だけ出現することができる。^[3]x

線形型システムは閉じた対称モノイド圏の内部言語であり、単純型付きラムダ計算がデカルト閉圏の言語であるのとよく似ています。より正確には、線形型システムのカテゴリと閉じた対称モノイド圏のカテゴリの間に関数を構築することができます。 ^[4]

アフィン型は、アフィン論理に対応する、リソースを破棄する（つまり、使用しない）ことを可能にする線形型のバージョンです。アフィン リソースは最大1 回使用できますが、線形リソースは正確に1 回使用する必要があります。

関連する型は、交換と縮小は許可するが弱化は許可しない関連するロジックに対応し、すべての変数が少なくとも 1 回使用されることを意味します。

サブ構造型システムが提供する命名法は、言語のリソース管理の側面を特徴付けるのに役立ちます。リソース管理は、割り当てられた各リソースが正確に 1 回だけ割り当て解除されることを保証する言語の安全性の側面です。したがって、リソースの解釈は、所有権を転送する使用、つまり移動にのみ関係します。この場合、所有権はリソースを解放する責任です。

所有権を譲渡しない使用 (借用) はこの解釈の範囲外ですが、有効期間のセマンティクスにより、これらの使用は割り当てと割り当て解除の間にさらに制限されます。

リソース解釈では、アフィン型を複数回使用することはできません。

例として、Hoare の自動販売機の同じ変種を英語、論理、 Rustで表現できます。

この例では、 Coinがアフィン型である ( Copy特性を実装していない限りはアフィン型です)ということは、同じコインを 2 回使用しようとすることは無効なプログラムであり、コンパイラが拒否する権利があることを意味します。

let coin = Coin {}; let candy = buy_candy ( coin ); // coin 変数の有効期間はここで終了します。let drink = buy_drink ( coin ); // コンパイル エラー: Copy 特性を持たない移動された変数の使用。   
    
    

言い換えると、アフィン型システムはtypestate パターンを表現できます。関数はさまざまな型でラップされたオブジェクトを消費して返すことができ、呼び出し元のコンテキストに型として状態を保存する状態マシンの状態遷移のように動作します ( typestate )。APIはこれを利用して、関数が正しい順序で呼び出されることを静的に強制できます。

ただし、これは、変数を使い切らないと使用できないという意味ではありません。

// この関数はコインを借りるだけです。アンパサンドは借りることを意味します。
fn  valid ( _ : & Coin )  -> Result < (), () > { Ok (()) }    

// 同じコイン変数は、移動されない限り、無限に使用できます
。let coin 
= Coin { }; loop { validate ( & coin ) ? ; }   
 
    

Rust が表現できないのは、スコープ外になることができないコイン型です。これは線形型を必要とします。

リソース解釈では、線形型はアフィン型のように移動できるだけでなく、移動する必要があります。スコープ外になると無効なプログラムになります。

{ 
// 渡す必要があり、ドロップされません。let token = HotPotato { };    
       

    // すべてのブランチがこれを廃止するわけではないと仮定します: 
if ( ! queue . is_full ()) { queue . push ( token ); }      
        
    

    // コンパイル エラー: スコープの終了時にドロップできないオブジェクトを保持しています。
}

線形型の魅力は、デストラクタが引数を取ったり失敗したりできる通常の関数になることです。^[5]これにより、たとえば、破棄のためだけに使用される状態を保持する必要がなくなります。関数の依存関係を明示的に渡す一般的な利点は、関数呼び出しの順序 (破棄順序) が引数の有効期間の観点から静的に検証可能になることです。内部参照と比較すると、Rust のように有効期間の注釈は必要ありません。

手動リソース管理と同様に、実際の問題は、エラー処理に典型的な早期復帰でも同じクリーンアップを達成しなければならないことです。これは、すべての関数呼び出しが潜在的な早期復帰であるスタックアンワインドを持つ言語では、細かいことにこだわったものになります。しかし、よく似た例として、暗黙的に挿入されたデストラクタ呼び出しのセマンティクスは、遅延関数呼び出しで復元できます。^[6]

リソース解釈では、通常の型では変数を移動できる回数を制限しません。C ++ (特に非破壊的な移動セマンティクス) はこのカテゴリに分類されます。

auto coin = std :: unique_ptr < Coin > (); auto candy = buy_candy ( std :: move ( coin )); auto drink = buy_drink ( std :: move ( coin )); // これは有効な C++ です。   
   
    

以下のプログラミング言語は線形型またはアフィン型をサポートしています^{[引用が必要]}。

• エフェクトシステム
• 線形論理
• アフィン論理