松浦 知也 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

14 lines
510 B
Markdown
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

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