ATS2の観が整理出来た

κeenです。ATS2には3つの世界があります。動的な世界、静的な世界、証明の世界。 前回の記事では静的な世界を色々扱ってみました。 今回は証明の世界である観について少し。

2016-1-2: いくつか誤植を直しました(用語で言えば、 注観→駐観 が正解でした)。

観(view)は、線形型によるリソース管理をするための仕組みです。 静的な世界と同様コンパイル時に検査されたらバイナリには現われませんが関数の引数として渡したり観を扱う関数(証明関数)を定義出来たり 動的な世界と似た部分があります。

駐観

at-viewの和訳だそうです。これは観の中でも特に特定のアドレスにデータが存在することの証明を表わす観です。 線形型の主な管理対象がメモリなので特別扱いされているのでしょう。

抽象観

任意のリソース管理に使っていい観。これ自体は実体を持たないので後述のデータ観などで実体を与える必要があります。 ドキュメントではロックの管理だとかに使う例が載っていました。

観型

ただ単に観と型をくっつけたものです。「あると便利なのは分かるけど…」と思ってましたが、だんだん理解が追いついてきました。

1つには観と型を1つの記法で表わせるので記述が楽になる。もう1つにはある型に対して必ず線形型によるリスース管理がされることを保証出来る。

もう1つの用途が思い浮かんだらなるほど、となりました。

こちらは駐観に限らず任意の観と任意の型を組み合わせれるようです。

データ観

動的な世界でのデータ型のように、静的な世界でのデータ種のように、証明の世界にもデータ観というものがあります。

例えば、あるかもしれないしないかもしれないリソースを表わすのにオプショナル観が使えそうだ、など。

これ自体は新しい観を作るためのものです。

データ観型

これは動的な世界と証明の世界両方に跨るものです。おおざっぱにはデータ型とデータ観を組み合わせたものです。 つまり、データ型であり、データ観であり、両方合わさってるので観型でもあります。

「データ型を観で管理しようとしたら同じようなデータ観を作ることになるしまとめて作れたら嬉しいよね」が一番分かりやすい説明でしょうか。

データ観型専用のシンタックスなどもあるようなので単なるシンタックスシュガーではなさそうです。

こちらは駐観というかメモリ管理の観が割り当てられるみたいです。


Rustと比べると随分リッチなリソース管理が出来ますね。

まだ良く分かってない部分

ATS2にはprop(命題)というものもあります。「観はpropの線形バージョン」と書いてあるのですがどう分けられているのでしょうか。 例えば観型にpropは渡せなそうな気がしますが、証明関数には命題も観も渡せそうな気がします。

微妙に命題と観が共存していたり排他的であったりします。動的な世界のdatatyp, 静的な世界のdatasort, 証明の世界のdataviewという理解でいるとdatapropの居場所がなくなります。

今のところ、証明の世界も普通の命題であるpropと線形の命題であるviewに分かれていて、 それらはsortが違うので一部では排他的であり、どちらのsortに対しても対応しているものもあるので共存してるようにも見えるという仮説を立てています。

ドキュメントにも種viewや種propという記述があるので種がsortが違うのは正しそうです。

しかしそうするとdatasortとかで新しく作った種はどこの世界に住むことになるんでしょうか。静的な世界?証明の世界に住む新しい種を定義出来ない?

ビルトインの種viewと種propの静的な項(の静的な項)だけが証明の世界の住人になれる?

datasortとかで作った新しい種は依存型や依存命題(?)、依存観(?)で使うためにある?

分からないことが多いですね。もう少しATS2の世界の整理をつけたい。

Written by κeen