#「定義」という言葉の用法が食い違っているようです。
ご回答は、要約すると、仕様と実装は違う／定義は
実装である／従って仕様が定義になってないのは当然
である、ということだと理解しました。
定義という言葉をそのよに使うなら、おっしゃること
はその通りですが、私の言う「定義」はそういう意味
ではありませんでした。
私の質問は、仕様記述は意図の定義である（front
とは何かなど）／代数的記述は（その意味での）定義
の適合性が見えにくいのではないか、ということでし
た。
#仕様記述の妥当性がわかりにくいということでしょうか．仕様記述間で矛盾がないことを確かめないと
#仕様記述の妥当性は確認できません．
#仕様記述は実装がもつべき性質を記述しているだけであって，実装方法を記述するものではありません．
#あれなんだかJuppaさんの質問を勘違いしている気がしてきた．ちょっ考えなおしてから書きます．
#モナドに関しては、以下2つを読んで、さらに知りたいなら「すごいHaskell」を読むといいでしょう。
###モナモナの方は、手元では改訂しているのですが、公開は次のスタートHaskellまで待って下さい。
#性質の件ですが、例えばある符号化に対する encode と decode という関数を考えてみて下さい。
#encode と decode がちゃんと逆関数になっている場合にのみ、
#encode (decode x) == x
#あるいは
#decode (encode x) == x
#が成り立ちます。
#ただし、これは逆関数であるという性質を保証しているだけです。
#encode 自体が仕様に沿っているかは、また別の性質を使ってテストする必要があります。
#(たとえば、encode したら長さが 33% 増えるとか。)
#満たすべき性質を全部挙げられなければ、やはりバグは残ると思います。
#また一般的にテストではバグの不在は証明できません。
#QuickCheck で性質テストを実施しても、バグが残る可能性があります。
#コストをかけていいのなら Coq などで、性質を証明すべきです。
#繰り返しになりますが、Coq を使ったところで、満たすべき性質を全部列挙できているとは限りません。
#すこし補足をさせてください > Juppaさん
補足：
「定義しているわけではないので，この感覚は自体はまっとうだとおもいます．」
といったのは，定義ということばを不用意に使ってしまっています．
仕様は実装の定義の仕方（実装方法）を示すものではなくて，定義がもつべき
性質を示しているだけです．したがって，仕様を実装の定義方法を示すものだ
と（まちがって）みなしてしまうと，それで実装の定義方法を示したものには
ならないんじゃないかという感覚になること自体は，納得できるという意味で
した．単に定義といったのは舌足らず誤解を生むいいかたでした．実装の方針，
あるいは，実装の方法と読みかえてください．
代数的仕様は実装方法を導くには弱いのはたしかですが，実装が正しく行われ
ているかを確認するには強力なツールにはなります．
#sqrt (x*x) = |x| は sqrt の仕様です．この仕様は sqrt の実装方法を導くには弱いですが，実装した sqrt の確認にはつかえます．
#nobsunさんが「代数仕様は実装が満たすべき性質を示
すものである」とおっしゃっているのは理解していま
す。しかし、私の疑問は、代数仕様は，（実装が満た
すべき）その性質をすべて記述し尽くしているという
ことが見えにくいのではないかということでした。
たとえば御本の中のQueueの代数仕様は、まずQueueに
はjoinやfrontやbackなどの操作があることを書いて
います。
そしてその公理部では、そのjoinとfrontが満たすべき
関係／joinとbackが満たすべき関係をそれぞれ2行づつ
書いています。つまり、各2行で、joinとfront、join
とbackを相互規定しています（あえて定義という言葉
は避けて規定という言葉を使いました）。
このとき、私などは、「joinとfront（あるいはback)
の関係はこの2つで尽くされているのだろうか」／
「frontとbackの間の関係を何か書かなくてよいのだ
ろうか」等々の疑問をもってしまいます。代数仕様
を書かれている方はそんな感覚をお持ちではないのか
なというのが私の質問でした。
代数的仕様が全体として「（いくつかの）操作の間の
相互関係を書く」というインプリシットな形式である
のでそうなりがちではないかと想像するのですが。
kazuさんからのコメントは、「満たすべき性質を全て
列挙することは（難しいし）必要ではない」というこ
とをおっしゃっているのでしょうか。もしそうなら
私は賛同できません。
encode と decodeの例はおもしろいですね。
型も付記されているのでしょうから、あの2つの公理
で結構符号化仕様の本質を書けていると感じました。
Queue仕様の場合に感じた、これで尽くされているか
という疑問は不思議に感じませんでした。操作が
この2つだけだからでしょうか。
sqrt (x*x) = |x| は、sqrtの仕様として完璧だと
思います。ただ「これで書き尽くしている」と主張
している記述ではないと感じます。
長文ですみません。
#kazuさん モナドのよい資料のご紹介ありがとうご
ざいます。勉強します。
#「満たすべき性質を全て列挙することは必要だが難しい」と言いたかったのです。
#Juppaさんが「これで書き尽くしていると主張している記述」だと思う sqrt の仕様はどういうものですか。
#たとえば、sqrt = ... あるいは sqrt (x) = ...
のような形で書かれていれば安心します。
#それはsqrtの実装ですよね。> Juppa さん
#ああ。↑とは言えないですね。撤回します。
haskell-ja > Archives > 2012/11/07