松浦 知也 Matsuura Tomoya
5300c253a6
All checks were successful
Build / build (push) Successful in 7m40s
510 B
510 B
date |
---|
2025-01-12 09:13 |
#type-system
変数やリソースが一度だけ使用されることをコンパイル時に確定できる仕組み。
CleanやIdrisなどで使用される(Rustのムーブセマンティクスも基本はこれ)。
Uniqueness Types — Idris 1.3.3 documentation
1回だけから任意のn回だけ使用できる、にすると線形型(Linear Type/Affine Type)になる