2009-11-07 [長年日記]
λ. “A semantics for imprecise exceptions” by Simon Peyton Jones, Alastair Reid, Tony Hoare, Simon Marlow and Fergus Henderson
こないだのPLDIr#3で稲葉さんが簡単に紹介していた論文。
CPUによってはアウトオブオーダー実行によって、単純に逐次実行する場合とは発生するエラーが異なってしまう場合がある。同様にHaskellのような純粋関数型言語でも、プログラム変換によって発生するエラーが異なってしまう場合がある。これがタイトルの imprecise exception の意味。
アウトオブオーダー実行やプログラム変換のような最適化によって意味が変わってしまうのは問題だけど、だからといってこれらを諦めるたり制限することは最適化のための大きな機会を逃すことになる。そこで、そのような変換によって意味が変わらないような意味論をかんがえるというのがこの論文。
まず、ゼロ除算エラーのような、起こる原因と場所がわかっているような例外(同期的例外)は、Haskellでは(手続き型言語における例外とは異なり)浮動少数点数のNaNのように式の値として伝播される(概念的には)。 そこで、式の表示的意味を通常の値もしくは起こり得る(同期的)例外の集合とする。その上で、例外の観察はIOアクションの中でしか出来なくして、この例外の集合から非決定的に一個取り出すという解釈をする。IOアクションの実行の意味論は神託を用いることを許しているので、これは問題ない。
このようにすることで、意味論上の問題もほぼ解決できて、かつ実装上も起こり得る例外を実際に全部集めたりする必要がなく効率的に実装できる。
起こり得る例外の集合を考える際の領域は Smyth Powerdomain の構成を利用しているのだけど、普通の関数型言語の意味論だとPowerdomainはなかなか見かけないので、「おーっ」と思った。
それから、Conclusion が As usual, implementation is ahead of theory: で始まっていて 笑った。
