Files
quartz-research-note/content/一意型.md

407 B

date
date
2025-01-12 09:13

#type-system

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

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

Uniqueness Types — Idris 1.3.3 documentation