■

静的型情報を効果的に使うことで簡潔に書けるケースがあることを示したかったのです。

型付けについてのまつもとさんとみずしまさんのやりとり - Togetterまとめ

これ、リアルタイムでiPhoneから眺めてたときは気づかなかったんだけど（外だったし）、要するに水島さんが言ってるのの簡単な例としてはオーバーローディング（ad-hoc polymorhismだっけ）でいいんじゃないかと思った。あ、Matzが言ってた。

あと、Haskellのreturnは型がないとできないよって言われたので、その辺もう少し勉強すべきだと思った。Haskell書くか。

個人的には、型システムってMLくらい単純なやつで、明らかに変なプログラムをrejectするためだけに使うくらいしか使い道がないんじゃないかと思ってる。ad-hoc polymorphismとかもっとできることをできるからってやる方向はあるだろうけど、やったらやったですごい複雑になるかすごいad-hocになるかのどちらかだと思ってて、つまりそんなもんはいらんという。MLくらい単純なやつだと窮屈すぎるっていう話はあるかもしれないけど、そこでもっとがんばってみても、結局、行き着く先はCoqかAgdaかIsabelleで、それで幸せなのかというとよくわからない。

なんていうか、私には型システムにたいしてそういう絶望があります。その一歩手前には、なんかよくわからない人もよくわからないなりに便利に楽しくプログラミングできる世界があるんでしょうけど、その世界を探すのはすごく楽しいんですけど、今はそこまで行く気力がありません。

あと、かたしすてむって言うとMLのやつを連想するので、なんかJavaみたいのとかよく知らないけど、別枠だと思ってるので。なんだっけ？ふろーかいせきとか言うやつ？そっちはがんばって複雑怪奇だけど便利なものを作ると面白いと思います。