部分構造型システム

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

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

Cleanプログラミング言語は、並行処理、入出力、配列のインプレース更新をサポートするために、一意性型（線形型の変種）を利用しています。^{[ 1 ]： 43}

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

単一参照特性により、線形型システムは量子コンピューティングのプログラミング言語として適しています。これは、量子状態のクローン禁止定理を反映しているためです。圏論の観点から見ると、クローン禁止とは、状態を複製できる対角ファンクターが存在しないという記述です。同様に、組み合わせ論理の観点から見ると、状態を破壊できるKコンビネータは存在しません。ラムダ計算の観点から見ると、変数はx項にちょうど1回だけ出現することができます。^{[ 3 ]}

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

アフィン型は、アフィン論理に対応し、リソースを破棄（つまり使用しない）できる線形型の一種です。アフィン型リソースは最大で1回使用できますが、線形型リソースは必ず1回使用する必要があります。

関連する型は関連する論理に対応しており、交換や縮約は可能だが、弱化は不可能である。つまり、すべての変数が少なくとも一度は使用されることになる。

リソース解釈によれば、アフィン型は一度しか使用できない。

例えば、ホーアの自動販売機の同じ変種は、英語、論理、そしてRustで表現できる。

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

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

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

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

// この関数はコインを借りるだけです。アンパサンドは借りることを意味します。fn validate ( _ : & Coin ) -> Result < (), () > { Ok (()) }// 同じ coin 変数は、移動しない限り、無限に使用できます。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++ です。