松浦 知也 Matsuura Tomoya 5300c253a6
All checks were successful
Build / build (push) Successful in 7m40s
[obsidian] vault backup: 2025-01-12 10:27:53[
2025-01-12 10:27:53 +09:00

510 B
Raw Blame History

date
2025-01-12 09:13

#type-system

変数やリソースが一度だけ使用されることをコンパイル時に確定できる仕組み。

CleanIdrisなどで使用される(Rustのムーブセマンティクスも基本はこれ)。

Uniqueness Types — Idris 1.3.3 documentation

1回だけから任意のn回だけ使用できる、にすると線形型Linear Type/Affine Typeになる