Idris 0.9.10

idris-0.9.10 がリリースされたのでちょっと触ってみた。http://www.idris-lang.org/idris-0-9-10-released/

証明付き型クラス

以前の idris では下のツイートのようなことはできなかったのですが、できるようになっていました。

例えば、

class MySemigroup a where
  (<+>) : a -> a -> a
  mySemigroupOplsAssociative : (x, y, z : a) -> x <+> (y <+> z) = (x <+> y) <+> z

のように、型クラスの実装に性質の証明を要請することができるようになりました。0.9.9以前でこのクラス定義のようなことをしようとすると、 <+> が見つからないとかで型チェックが通らなかった(はず。よく覚えてない)。

でも Prelude.Algebra モジュール が未だに性質の部分を Vierified なんちゃら型クラスとして分離させているのはなぜだろう。

他の変更点としては、とうとう OS X 向けのバイナリが出たりとか、この前書いたようにサーバ・クライアントで動くようになったりとか、llvm, gmp, ffi がデフォルトでは無効になったりとか。あまりちゃんと調べていないけどこんなところかなあ。