sumiiの日記 このページをアンテナに追加 RSSフィード

2006-08-24

Haskellの「代数的」データ型は代数的か?

という(という言い方も合っているのかどうか定かではありませんが)。他力本願の本領を発揮して、別の話のついでに、知り合い(www.cl.cam.ac.uk/~amp12/)にちょっと聞いてみました。

The denotational semantics of datatypes, be it in a non-strict language like Haskell, or a strict one like ML, involves solutions of domain equations. It's just that the domain constructions are different in each case (to take account of the different evaluation strategies). The surprising thing is that in all cases these solutions are both initial _and_ final simultaneously (they are what Freyd termed free bialgebras) in a suitable category of domains and strict continous functions. In that sense the dataypes in Haskell are "algebraic" (but one could equally say they are "coalgebraic", or better "bialgebraic"). The terminology is an historical accident. In pure strict functional programming, the values (as opposed to all expressions, including ones that may diverge) of an algebraic datatype really do correspond to what one would expect: eg finite lists of values for a list datatype. When lazy functional programming got going, the very same form of datatype declaration was used, so people carried on calling it algebraic, even though its semantics, because of the non-strict eval strategy, is much more complicated. I find it ironic that one of the early selling points of lazy functional programming is that its programs satisfy familiar mathematical "laws" (like beta conversion---in the strict world one only has beta-value conversion), whereas in reality its semantics is much more complicated than for strict functional programming.

だそうで。自分がちゃんと理解していないのでコメントできませんが…

追記:恥の上塗りを承知でナイーブな質問なのですが、Haskellにはstrictでない関数もあるわけで、もし「strictな連続関数に制限したCPOでは始代数」と理解してしまうと、「Haskell代数的データ型は始代数」という話とズレているようにも(私のように何も知らない者には)聞こえてしまうのですが、どう考えれば良いのでしょうか?

追記の追記:っていうか、読み直したら何となくわかった(ような気がする)。strictじゃないといけないのは酒井先生:-)のいうF(f)であって、「Haskell関数がstrictでない」こととはまったく別の話、ということか。

ちなみに、しつこいようですが、圏論の話題については、自分は「自然変換関手 = List.map」という程度のデタラメな理解しかない人間なので*1、私のいうことを信じてはいけません。

*1:YK先生の圏論の授業は最初の2回ぐらいで脱落しました…。なぜか単位はもらえた記憶もありますが。スミマセン。

いがいが 2006/08/25 10:38 自然変換 = List.rev くらいがいい例なんじゃなかったかしら。List.map f は、List functor を f に適用したもの? とか、知ったかぶってみる。

sumiisumii 2006/08/25 16:16 あー、そうですね…。本当にデタラメであることを証明してしまいました(笑)。

酒井酒井 2006/08/27 13:18 これは私のF(f)の話とは別で、まさに「strictな連続関数に制限したCPOでは始代数」という意味で言っていると思います。
例えば、M.M. Fokkinga and E. Meijer. Program calculation properties of continuous algebras. Technical Report CS-R9104, CWI, January 1991. http://citeseer.ist.psu.edu/fokkinga91program.html には、CPOでは始代数になっていない場合があるということが書いてあって、以降の論文ではよく「strictな連続関数に制限したCPOで始代数」のような書き方がしてあります。
# Haskellにはnon-strictな関数もあるので、ズレてるとは思いますが。

それに対して私の話は、誤解を招く書き方だったのですが、
* ある条件を満たせばCPOでも始代数になっている
* Haskellの代数的データ型は特殊なもの以外はその条件を満たす
という話です。

sumiisumii 2006/08/28 14:57 おお、なるほど(実はググったらその論文を発見したせいで、最初の追記のように考えてしまったのでした)。そうすると、いよいよ酒井さんのお話が既出なのかどうか気になってきますね…

投稿したコメントは管理者が承認するまで公開されません。

スパム対策のためのダミーです。もし見えても何も入力しないでください
ゲスト


画像認証

トラックバック - http://d.hatena.ne.jp/sumii/20060824/1156403303