状態遷移機械を型で安全にし、合成し、実用する。Idrisの作者がそんな人類の夢に果敢に挑み、ついに到達した抽象化とその利用法を解説します。なお、利用言語は依存型を持つIdrisですが、Scalaでどこまで真似ができるのかにも注目してみます。
解説の対象はControl.STライブラリです。( http://docs.idris-lang.org/en/latest/st/ ) 論文”State Machines All The Way Down”も参考になります。( https://www.idris-lang.org/drafts/sms.pdf )
票中 票投票済み