2025-01-12 09:27:53 +09:00
|
|
|
|
---
|
|
|
|
|
|
date: 2025-01-12 09:13
|
|
|
|
|
|
---
|
|
|
|
|
|
#type-system
|
|
|
|
|
|
|
|
|
|
|
|
変数やリソースが一度だけ使用されることをコンパイル時に確定できる仕組み。
|
|
|
|
|
|
|
2025-01-12 10:27:53 +09:00
|
|
|
|
[[Clean]]や[[Idris]]などで使用される（[[Rust]]のムーブセマンティクスも基本はこれ）。
|
2025-01-12 09:27:53 +09:00
|
|
|
|
|
|
|
|
|
|
[Uniqueness Types — Idris 1.3.3 documentation](https://docs.idris-lang.org/en/latest/reference/uniqueness-types.html)
|
|
|
|
|
|
|
2025-01-12 10:27:53 +09:00
|
|
|
|
1回だけから任意のn回だけ使用できる、にすると[[線形型]]（Linear Type/Affine Type）になる
|
2025-01-12 09:27:53 +09:00
|
|
|
|
|
