型レベル関数の inverse

元ネタ
http://twitter.com/keigoi/status/7828062396
http://okmij.org/ftp/Haskell/PeanoArithm.lhs


ようするにこの Inv は何をやっているのかというと,init から limit まで x をイテレートして,x と a に関数 clas を適用したの値と b が等しくなるようなものを返す,ということを型レベルで行っているようなかんじ.
当然与えられた範囲に見つからないときもあるので,そのときは NLE x limit に失敗してエラーとなる.
このような操作をすることで,自然数上の逆関数のようなものが可能になる.
個人的には Inv も面白いなぁとは思ったけれど,Sum2 の使い方もうまいなぁと思った.
これをもうちょっと俺にとってわかりやすく書き直してみたのがこれ.
http://gist.github.com/279174
あと Registry がちょっとかっこわるくて外せないかなぁとも思うんだけど,ちょっといろいろ考えてみます.


おまけ.
PeanoArithm.lhs の最後に

The practical outcome of this exercise is the creation of a benchmark
suite for Haskell typecheckers, e.g., computing the inverse factorial
of 720. Perhaps there should be a shoot-out entry for the speed of
typechecking.

The implementation of RSA on type level is left for future work.

とあって,なんか考えていることが違うなぁと思いました.