Imaginantia

思ったことを書きます

structとlinear type

ある大きなデータ構造 T を考える。T のメンバとなっている変数 a の値についての操作を考えたい。

a を書き換える」ということをしたい場合、純粋世界では必ず構造 T を再構築せざるを得ない。 これでは明らかに負荷が入るため、そこで「他で使われていないこと」という意味での線形性を満たすときに「実際に書き換える」ということがしたい。 利用者が居ない場合は純粋世界から見たときに「T 全体が再構築されたのか」「a の部分だけ書き換わったのか」を区別できない。よってこれは正当な操作である。

さて、この上で「異なる変数 b を参照する」という操作を考える。このとき明らかに T を「他で使っている」ため、先の操作は正当ではなくなる。 しかし本質的にこれは問題ない操作であるはずである。書き換えによって b の値は変化しない。 つまり先程課した条件「他で使われていない」が強すぎたということになる。もっと厳密な言明を用意する必要がある。

そうすると出てくるのが「後に元の構造の a を参照していない」という条件である。つまり線形性の要求はメンバ毎に分離されたわけである。


ところで書き換えをするときはtensor、読み出しをするときにはwithな気がする。