静的型付け vs. 動的型付け(変数の型無し)

[id:lethevert:20051224:p1]に型について、思っていることを書いたのですが、その続きというか、なんと言うか。

      • -

LispSmalltalkといった変数の型がない言語があるのですが、僕は、これらの言語を使って、大規模なプログラミングを型エラーなしに作り上げる自信がありません。
また、普通の静的型付け言語では、JavaやらDelphiを使うことが多いのですが、この辺の言語を使っていると「キャスト」を多用するコードを避ける方法がありません。しかし、キャストをするコードを書くたびに、今、正しいキャストを書いているのか、将来、変更が起こったときに、このコードがバグを生み出すことがないのかと心配になります。

      • -

それとは別に、JavaDelphiでは、高レベルの汎用的な処理を書こうとした時に、型エラーで代入ができなくて、困ることがあります。そういうときは、Lispなど変数の型がない言語の便利さを思います。(Lispは、変数に対してどんな型のデータでも代入(束縛)できますが、Delphiを使っていると、これがそんなに「普通」のことではないことは分かります)

      • -

JavaGenericsの現実的な制限を見ていても思うのですが、万能な型付けというのは、まだないのかなと。そういう点を考えると、Lispのような型チェックをしないという選択が、不完全な型チェックに悩まされるよりましだという考えがありうるのだろうなと思ったりもするのです。

      • -

Concurrent Cleanは、Javaなどよりもずっと柔軟な型システムを持っているのですが、それでも、型システム上の制限に悩むことがあります。ランクN多相性([id:lethevert:20051229:p4])なんか。「キャスト」がないので、抜け道を抜けることができません。
それから、型エラーの表示が分かりづらいですが、これも静的な型チェックというのが結構複雑な概念であることを示しているのだと思います。

      • -

Ocamlは、Concurrent Cleanよりもより複雑な型を扱えるような型システムを持っているという印象があるのですが、あまりよく理解していません。
ocaml ランク 多相」で検索していたら、下のスライドが引っかかってきた。後で見ておこう。
http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/ocaml-ng.pdf