Skip to content

Latest commit

 

History

History
22 lines (19 loc) · 1.85 KB

effects.md

File metadata and controls

22 lines (19 loc) · 1.85 KB

関数は様々な作用を持つことができます。この作用は型検査器によって追跡されます [1]。この作用は関数定義中の : 直後に配置します。(また ':' と '<>' の間にスペースを入れてはいけないことに注意してください。) :<> は純粋であることを意味し、('<>' のない) : はどのような作用も起きうることを意味します。'<>' の間にはその他の様々な作用を配置できます。

  • !exn - その関数が例外を発生させる可能性がある
  • !ntm - その関数が停止しない可能性がある
  • !ref - その関数が共有メモリを更新する可能性がある
  • 0 - その関数は純粋である (作用を持たない)
  • 1 - その関数は全ての作用を持つことができる
  • fun - その関数は通常のクロージャではない関数である
  • clo - その関数はスタックに確保されたクロージャである
  • cloptr - その関数は明示的に解放されるべき線形クロージャである
  • cloref - その関数はガベージコレクタによって解放される永続的なクロージャである
  • lin - その関数は線形で、一度だけ呼び出すことができる
  • prf - その関数は証明関数である
  • !wrt - その関数はそれが所有する場所に書き込みを行なう可能性がある。例えば ptr_set はそのような作用を持つ
  • !ref - その関数は存在を知っているが所有していない場所に対して読み込みもしくは書き込みを行なう可能性がある

これらは <lincloptr1> のように結合させることができます。全ての関数の作用は eff です。