線形型とは？

線形型（せんけいがた、Linear Types）とは、型理論・プログラミング言語理論の概念で、変数やリソースが「厳密に1回だけ使用される」ことをコンパイル時に型システムが保証する仕組みのことです。線形論理（Linear Logic）を計算・プログラミングに適用した成果であり、リソースの二重解放・メモリリーク・競合状態といったバグを静的に防ぐ手段として注目されています。

通常のプログラムでは変数を何度でも参照・コピーできますが、線形型システムでは「使った値は消費される」という制約が課されます。これにより以下のことが保証されます。

• 同じファイルハンドルやソケットを2回閉じる（二重解放）ができない
• 一度送ったメッセージを再送するコードをコンパイル時に検出できる
• メモリの所有権が明確になり、GCなしでも安全なメモリ管理が実現できる

線形型の考え方は、実用的なプログラミング言語にも影響を与えています。RustはBorrow Checkerという仕組みで所有権・借用・ライフタイムを管理しており、これは線形型・アフィン型（最大1回使用）の考えに基づいています。Haskellの拡張やIdrisなど研究用言語でも線形型が実装されています。

線形型はリソース管理・並行プログラミング・セキュリティ上重要な資源（暗号鍵など）の扱いに特に有効です。型システムが「リソースの寿命と使用回数」を管理することで、実行時エラーではなくコンパイル時にバグを検出できる点が大きなメリットです。