「型を付けないほうが自由?」抽象化と型の関係について

型モヒカンは今日も戦う 読みやすさのため順番を少し前後させています。
6
m2ym @m2ym

すごく素朴な疑問だけど、型を付けない方が自由に考えられて良くないかな

2014-12-08 23:21:17
m2ym @m2ym

抽象化と型を付けることはあまり関係なかったりして

2014-12-08 23:24:31
ちゅーん @its_out_of_tune

寝ようと思ったけど興味深い意見だと思ったのでちょいと

2014-12-09 02:30:36
ちゅーん @its_out_of_tune

我々、静的型クラスタはわりと簡単に、型の設計は難しいという事を忘れてしまうと思うのですよ!!

2014-12-09 02:33:42
ちゅーん @its_out_of_tune

「型の設計が難しい」と「プログラミングは難しい」ってのはほぼほぼ同義なんだが、この辺の感覚はあるていど型をぺろぺろした人じゃないと分からない。

2014-12-09 02:35:14
ちゅーん @its_out_of_tune

まぁ、そもそもこの方は「型が付いていない」のと「静的に型検査されない」の違いが分かっていない可能性があるので、どのへんから説明したら良いかわりともにょもにょする感はあるのだが・・・

2014-12-09 02:38:54
ちゅーん @its_out_of_tune

で、静的型システムのほうが経験上、深刻なバグや設計上のミスに悩まされる事が多いというのは・・・

2014-12-09 02:43:07
ちゅーん @its_out_of_tune

実行時エラーの話なのかコンパイルエラーの話なのかわからんのでなんとも言えん。

2014-12-09 02:43:35
ちゅーん @its_out_of_tune

以前から言ってるのだけど、そもそも従来の手続きOOPLと型システムの親和性はそれほど高く無い上に、それすら十分扱えてる人ってあんま多くないと思うので、この辺の底上げはどうすれば出来るんだろうとはいつも思ってる。

2014-12-09 02:48:03
m2ym @m2ym

正確に主旨を伝えるのは難しいですが、早とちりしてはいけないですよ。

2014-12-09 02:52:06
m2ym @m2ym

静的型付きプログラミング言語が悪いとは一言も言ってないですし、静的型検査が悪いとも言ってないです。素朴な疑問として、プログラムに静的な型を付けていくことが、どの程度抽象化に繋がるか興味があるというのと、個人的な経験ではそれは低水準に留まる、ということです。

2014-12-09 02:54:50
ちゅーん @its_out_of_tune

@m2ym 失礼ですが、HaskellかOCamlあたりの言語のご経験は?

2014-12-09 02:56:10
m2ym @m2ym

例えば、リソースリークがないことや、状態に一貫性があることを型で表現するのはなかなか難しいです

2014-12-09 02:56:12
m2ym @m2ym

@its_out_of_tune Haskell は趣味程度です。 OCaml はまあそこそこ実用していますが、とても大規模とは言えません。

2014-12-09 02:57:47
ちゅーん @its_out_of_tune

@m2ym 失礼しました、Web見たらそのへんについて触れられていましたね・・・。静的型システムがどの程度抽象化に繋がるかという疑問については、この辺の静的型付け関数型言語の手法が参考になると思ったのです。FunctorやMonad等は使われていますよね?

2014-12-09 03:00:43
ちゅーん @its_out_of_tune

以前盛り上がった「変数に型がないということの利点」の人と同じレベルの話かと思ったらそういうわけでは無いらしい。

2014-12-09 03:04:47
m2ym @m2ym

@its_out_of_tune はい、並程度に。ちなみに、圏論的・代数的な抽象化は基本的に賛成です。

2014-12-09 03:07:31
ちゅーん @its_out_of_tune

@m2ym なるほど、色々と誤解していたようです。その上で、m2ym氏が問題にされているのは、型に現れない値レベルの問題という事で良いですよね?リソースリークはどうしようも無いとして、状態の一貫性というのはどういう事でしょうか?

2014-12-09 03:09:28
ちゅーん @its_out_of_tune

この展開、マサカリ投げた相手を間違えたパターンが往々にしてありえるからマサカリマンはやめられない。

2014-12-09 03:10:33
m2ym @m2ym

@its_out_of_tune 例えば、キャッシュクリアはよくある話だと思います。キャッシュの導出に用いた元データは更新されたが、キャッシュの方は更新されないのは困りますよね。

2014-12-09 03:13:21
m2ym @m2ym

適当なことを書いてしまって申し訳ない。まあ、Twitter とはこういうものだと思って了承いただければと思います。

2014-12-09 03:16:04
ちゅーん @its_out_of_tune

@m2ym 確かにそれは型で直接表現するのは難しい問題ですね。それこそ、のぶかず氏のこの辺(twitter.com/nobkz/status/5…)が解決案という事になりますが、これは値レベルの話ですし・・・

2014-12-09 03:18:01
はなだ☆のぶかず@lisp &ボドゲ勢ボドゲプレイヤー) @nobkz

@m2ym @takeoka 良いDSLやDSMLを設計できればバグは少いと思いますね。そして個人的な経験上そうしたシステムはバグが少ないとは思います。

2014-12-09 02:23:30
m2ym @m2ym

@its_out_of_tune 型によって異常な状態遷移を制約する、といったことは可能だと思いますが、どの程度、強力な型システムが必要か不明ですし、制約に必要な情報(型)を保ったまま状態の合成なども考えなくてはならないため、

2014-12-09 03:24:06
m2ym @m2ym

@its_out_of_tune それはそれで面白いと思いますが、非常に難解で時間がかかると思います。それなら型のことは忘れて、もっと直球なアプローチも考えられるだろう、ということになります。そういった背景をこちらが共有していなかったために誤解されたのだと思います。

2014-12-09 03:26:33
ちゅーん @its_out_of_tune

@m2ym つまり、最終的に必要な制約や状態の範囲が開発時には想定し切れないため、誤った制約が深刻な問題に繋がる事が多い、という解釈であってますか?状態の合成についてはlensとかEffでいくぶんか解決されてるかもですね。こちらこそ、読み違い申し訳ない。

2014-12-09 03:29:22