2004-07-31 [長年日記]
λ. 今日から一応夏休みか。
λ. お昼
純広東家庭料理「嘉賔(KAHIN)」。
λ. Haskellの代数的データ型は始代数ではない
Haskellマラソンで「Haskell の普通の代数的データ型は始代数(initial algebra)になっていないと話したが、例がちょっと間違っていたので、とりあえずここに書き直しておく。
たとえば、「data N = Z | S N」という代数的データ型と、以下のようなダイアグラムを考える。
Z S
1 ──→ N ──→ N
│ │ │
│ │ │
│ ↓ ↓
└──→ N ──→ N
Z id
これを可換にするような N→N は複数存在し、ユニークには決まらない。例えば以下のh,h'は共にこのダイアグラムを可換にするが、hが正格であるのに対してh'は非正格なので等しくない。
h, h' :: N -> N
h Z = Z
h (S x) = id (h x)
h' _ = Z
一般に、pointedなCPO と正格なものに制限されない連続関数からなる圏には、始代数は存在しなかったと思う。(Haskellにはpointedでないようなデータ型もあるけど、それはそれ)
λ. Haskellの代数的データ型は始代数ではない? (2)
2005-02-25に追記。上記の議論は正しくなかった。代数的データ型の領域を構成するときに使う separated sum A+B は圏論の意味での直和(coproduct)ではないので、h'が上記のダイアグラムを可換にすることからは、下記のダイアグラムを可換にすることは言えない。実際 h' ([Z,S] ⊥) = h' ⊥ = Z は [Z,id] ((1+h') ⊥) = [Z,id] ⊥ = ⊥ と等しくない。したがって、これは反例になっていない。
[Z,S]
1+N ───→ N
│ │
1+h'│ │h'
↓ ↓
1+N ───→ N
[Z,id]
λ. Haskellの代数的データ型は始代数ではない? (3)
2005-02-26 に追記。横山さんの日記で言及されたのをきっかけに色々と考えてみたのだけど、考えていてだんだん分からなくなってきた。とりあえず、自分が理解していることだけを簡単に書いておこうと思う。
pointed CPOと任意の連続関数からなる圏では、関手F*1の終余代数のinverseは弱始代数(weak initial algebra)ではあるけれど、本物の始代数になっていないことがある。ただし、正格な連続関数だけに制限した部分圏の始代数にはなっている。
簡単な具体例としては恒等関手や(圏論の意味での)直積の場合がある。恒等関手については、対応する型構築子とその不動点となるデータ型をHaskellで実際に定義することが出来る(e.g. newtype I x = I x; type T = Fix I)。一方、(圏論の意味での)直積はCPOとしては存在してもHaskellで定義することは出来ない*2。
それにしても大げさなタイトルをつけてしまったもんだ。例は間違ってるし、タイトルは大げさすぎるしで、恥ずかしいなあ、もう。
λ. Haskellの代数的データ型は始代数ではない? (4)
2005-02-28 追記。もう少しすっきり理解できた。
- 定理1 (Recursive Types Reduced to Inductive Typesより)
- (X,φ) が正格な連続関数だけに制限した部分圏の始代数 ⇔ (X,φ-1) が終余代数。
- 定理2 (自分で証明)
-
任意の A, B, f:A→B について Ff: FA→FB が正格とする。
このとき、(X,φ) が始代数 ⇔ (X,φ-1) が終余代数。
でも、これじゃ定理2よりHaskellのほとんどのデータ型は始代数と考えて問題なくなっちゃうじゃないか。う〜ん、残念(ぉぃ。
