「静的型付け関数型プログラミングだとOOよりもTDD(BDD)がしやすい(もしくはいらない)」?

はなだ☆のぶかず@lisp &ボドゲ勢ボドゲプレイヤー) @nobkz

@kyon_mm @katzchang (僕も気をつけなきゃな......)

Kazunori Otani @katzchang

@kyon_mm ついでに私の意見を言うと、型付けチェックが強い環境では低いカバレッジでもリファクタリングがしやすいのはある。IDEのサポートも確実で不安が少ない。

Shozaburo Nakamura @shownakamura

横から失礼します。業界に昔からある大きな夢は、仕様からの自動プログラミング。RT @kazu_yamamoto: .@kyon_mm @tomooda 型レベルの検査は、証明であって、テスト以上の質があります。

Shozaburo Nakamura @shownakamura

@kazu_yamamoto @kyon_mm @tomooda 仕様を書けば証明系が正しさを検査し、正しいことがわかれば、それが高効率で実行できるプログラムに自動変換される。できたプログラムはバグなし。よって、正しい仕様を定義すれば設計も実装も終わりテストも不要。というもの。

Shozaburo Nakamura @shownakamura

@kazu_yamamoto @kyon_mm @tomooda この流れの直系が、Formal Methods(形式手法。形式的仕様記述)。仕様のチェックはできるようになっているが、高効率の実装への自動変換はできておらず、実装は人間が書かないといけない。

Shozaburo Nakamura @shownakamura

@kazu_yamamoto @kyon_mm @tomooda Formal Methodsは、仕様と実装の断絶が大きいが、実装言語が選べると思えば、それはメリットだ、仕様だけでも正しさが保証されているものがあるメリットは大きいという意見もある。

Shozaburo Nakamura @shownakamura

@kazu_yamamoto @kyon_mm @tomooda 静的型付け関数型言語は、前述の大きな夢を頭の隅におきながら、実装に重きを置いて、型注釈、型推論などを使って、Formal Methods的要素を取り入れたもの。型注釈は、TBB/BDDに比べ、数学的、宣言的な記述。

ぐるぐる系SQL @bleis

OOP的なTDDってのは、「どう動くべきか」を中心に考えるとTDDとマッチしやすい。でも静的型付き関数プログラミングでは、「どういう型で表現するか」ってのが先に来ることが多いので、TDDとはマッチしにくい。

ぐるぐる系SQL @bleis

もちろん、静的型付き関数プログラミング言語で「どう動くべきか」を中心に考えてTDDに合わせることもできるけど、利点があるかどうかはあやしい(というか、ない気がする)

ぐるぐる系SQL @bleis

逆に、OOPLで「どういう型で表現するか」を考えるようになると、その部分はTDDしにくい

Shozaburo Nakamura @shownakamura

@kazu_yamamoto @kyon_mm @tomooda TDD/BDDは、既存の命令型言語の上で、仕様を付加的に書いてテストによってバグなしプログラムを目指す。仕様は、その言語で非数学的、非宣言的に書くので証明系によって正しさを証明できず、テストを繰り返すしかない。

Shozaburo Nakamura @shownakamura

@kazu_yamamoto @kyon_mm @tomooda というのが、現状の私の理解。 Formal Methods関係ちょろっと。 http://t.co/95RrGIZN5h http://t.co/6EtXtq5Q8h http://t.co/aU6A7AJq0w

極端流形式仕様 初代𝕍𝕚𝕖𝕟𝕟𝕒𝕋𝕒𝕝𝕜𝕖𝕣 @tomooda

一方、Formal MethodsもVDMなど実行可能仕様での継続的単体テストを取り入れたりなど、お互い影響を与えあっていて楽しいですね。 @shownakamura @kazu_yamamoto @kyon_mm

はなだ☆のぶかず@lisp &ボドゲ勢ボドゲプレイヤー) @nobkz

@kyon_mm どういたしまして! 会話の抜けとか結構あるみたいなので、追加、修正を随時やっていますー。追加したいツイートがあればぜひ。

山本和彦 @kazu_yamamoto

.@shownakamura @kyon_mm @tomooda 関数型言語が何を目指しているかは、 @camloeba さまのこの記事が秀逸です。 http://t.co/7huS5EIcN8

山本和彦 @kazu_yamamoto

.@m_seki @kyon_mm @tomooda 僕も今 C を使うと、Haskell でやっていることのまねごとぐらいはできるのですが、いかんせん型システムが弱く、暗黙に型変換されたりして、Haskell のようにはいきません。

きょん＠アジャイルコーチ、システムアーキテクト @kyon_mm

@tomooda @shownakamura @kazu_yamamoto 中村さん、小田さんありがとうございます。形式仕様記述についてまた少し理解が進みました。繰り返しになりますが、TDD/BDDというのはバグを無くすことが大義ではないです。（続く

山本和彦 @kazu_yamamoto

.@kyon_mm @tomooda なるほど、by example はそういう意味なんですね。

きょん＠アジャイルコーチ、システムアーキテクト @kyon_mm

@tomooda @shownakamura @kazu_yamamoto もちろんTDD/BDDは「実行可能で繰り返し可能な分析,設計結果の記述」であることから実際にはバグを減らすことにつながっていますし、それを効果として言うのも問題ありませんが、目的は異なります。

山本和彦 @kazu_yamamoto

.@kyon_mm @tomooda 一般的な技量のHaskellerがQuickCheckで検査できるのは純粋関数です。たとえば、実践で使う例としては、encodeとdecodeが逆関数であることを示すために、decode (encode x) == xと書いたりします。

山本和彦 @kazu_yamamoto

.@kyon_mm @tomooda QuickCheckでもIOを扱えますが、僕は使いこなせません。使いこなしたのを見たことがあるのは、QuickCheckの作者であるHughesだけです。Hughesは、Haskellでは食えないといって、Erlangに行きました。

Takashi Miyamoto @tmiya_

ところで @kyon_mm さんは、Design-by-Contract については何故語らないのだろうかとも思ったり。あれは型の有無とはまた直行した概念で、quickcheck的な自動テスト生成とも直行した概念。でもDbCは形式的検証には関係してくる話だと思うが。

山本和彦 @kazu_yamamoto

.@kyon_mm @tomooda Erlangで書かれたRiakには一年に一回落ちるバグがあって、HughesはQuickCheckでそのレースコンディションを見つけました。ついでに、他にも4つレースを見つけたそうです。

きょん＠アジャイルコーチ、システムアーキテクト @kyon_mm

@tmiya_ 勉強しているのですが、まだまだ理解が足りていないのです。すいません。。。いままでやったことはTouch of Classを読んだりKrakatoaを少しいじったりしている程度です。DbCすごく好きなのですがまだ発言できる段階にいないのです。

山本和彦 @kazu_yamamoto

.@kyon_mm @tomooda 一般的に、HaskellのIOに対するテストは、命令型のそれと何ら変わりないです。ひたすらテストケースを書きます。