2004-11-01 [長年日記]
λ. Re: 正格性解析
sum' = foldl (+) 0
がInt
やI
だと余計なメモリを食わず、Integer
だと余計なメモリを食ってしまう理由ですが、原因はfoldl
がインライン展開されるかどうかの違いですね(GHC 6.2.1 で確認)。Int
やI
だとfoldl
がインライン展開されて、(+)
の正格性に基づいた最適化がされてます。それにしても、なんでInteger
だとfoldl
がインライン展開されないんだろう……
それはそうと、以下の3つの型は領域(domain)が同型なので、add (I x) (I y) = I (x + y)
とかは(少なくとも理論的には)無意味だと思います。
data I = I !Integer
newtype I = I Integer
Integer
[追記] あうぅ。領域が同型であっても、newtype
とdata
ではパターンマッチの方のセマンティクスが違うのを忘れてました(Haskellはややこしいなぁ)。(+)
がもし仮に非正格でも、この方法で定義したadd
は正格になるので、意味はありますね。すんまそん。
λ. 風邪
先週末から少し調子悪いなと思ってたら、風邪をひいてしまった。今日が慶早戦による休講で助かった。
2004-11-03 [長年日記]
λ. ghc の新しい機能 Generalized Algebraic Data Types (GADT)
かなり今更だが、Inemuri nezumi diary (2004-10-08) よりメモ。言うまでもないけど、これがあると Phantom Types とか普通に使えるようになるし、色々と嬉しそうだ。
詳しくは、"Wobbly types: type inference for generalised algebraic data types" を見ればよさそうか。
あと、モデルとしては dependent types の場合と同じようなものを考えればよいのかな……
λ. James Cheney 氏
Phantom Types の James Cheney 氏って AlphaProlog の人でもあったのか。ちょっとビックリ。
λ. アメリカ大統領選
個人的にはどっちかと言えば民主党よりも共和党に勝ってほしいと思ってるけど、さてどうなるやら。それにしてもアメリカの選挙は面白いなぁ。
ψ ささだ [日記とは関係ないんですが、RHG いくー? 前借りた奴そのまんまだから。]
ψ さかい [行きまーす。多分。]
ψ shelarcy [参照されている The Fun of Programming の章を読んだ目から見ると、なるほど結局こういう形の s..]
ψ ささだ [りょーかい。]
ψ さかい [syntax suger としてではなく、ダイレクトに実装したものだと思ってました。syntax suger という..]
ψ trad [desugarされたのを見た限り(-ddump-ds)、type equalityの追加はしていないと思われます。 ..]
ψ shelarcy [(日記のリンク先の本のページなどの)ソースを見れば分かる通り Haskell98 + 拡張環境下での Phantom..]
ψ さかい [tradさん。ありがとうございます。 やっぱりそうですよね。 shelarcy さん。 GADTが「Haskell..]
ψ shelarcy [ふむ、そうですか。分かりました。]
ψ shelarcy [あっ、ポインタありがとうございます。]
ψ さかい [そういえば、The Fun of Programming のページの Chapter 12 のTerm.hsはapp..]
2004-11-05 [長年日記]
λ. Super Mario Hopscotch
ラブ・ファミコン より。ちとはまってしまった。2つ目のステージのパーフェクトを取るのが難しかった。
λ. A206 峠の村
4日目にヤコブが人狼COしてオットーを狂人と言ったのだが、これは変だなぁと思った。仮にオットーが狂人なら、オットーがカタリナに人間判定を出した理由が理解出来ないのだ。狂人オットーはヤコブが最後の人狼だと知っていることになるので、ヤコブが人狼確定してしまうカタリナ人間判定よりも、ヤコブが人狼確定せずに済むカタリナ人狼判定を出すべきだからだ。
ニコラス (占い師CO,襲撃された) | ヤコブ (占い師CO) | ジムゾン (村人CO,処刑された) | オットー (霊能者CO) | カタリナ (霊能者CO,処刑された) | オットーの カタリナ人間判定 | オットーの カタリナ人狼判定 |
---|---|---|---|---|---|---|
占い師 | 人狼 | 人狼 | 霊能者 | 狂人 | ○ | |
占い師 | 人狼 | 人狼 | 狂人 | 人狼 | ○ | ○ |
占い師 | 狂人 | 人狼 | 霊能者 | 人狼 | ○ | |
占い師 | 人狼 | 人狼 | 霊能者 | 人狼 | ○ | |
狂人 | 占い師 | 人狼 | 霊能者 | 人狼 | ○ | |
狂人 | 人狼 | ? | 人狼 | 霊能者 | ○ | ○ |
狂人 | 人狼 | 人間 | 人狼 | 人狼 | ○ | ○ |
λ. (β→γ)→(α→β)→α→γ
First Steps in Modal Logic について雑談してるときに「(β→γ)→(α→β)→α→γ」をヒルベルト流(ただし論理公理は (s) (α→β→γ)→(α→β)→α→γ と (k) α→β→α のみ)でとっさに証明できなくてちょっと悔しかった。λ式で書くなら λf.λg.λx. f (g x)
でおしまいだし、自然演繹やシーケント計算でもそれは同じだけど、ヒルベルト流だとすぐには思いつかんよ。
後でこのλ式をSKIコンビネータの式に機械的に変換してみると「S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))(S(KK)(KS)))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))(S(KK)(KK)))))(S(S(KS)(S(KK)(KK)))(KI))))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))(S(KK)(KS)))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))(S(KK)(KK)))))(S(KK)(KI))))))(S(S(KS)(S(KK)(KK)))(S(KK)(KI))))」になった。もっと短く出来そうではあるけど、流石にこれは思いつけないよなぁ……
というか、アレだ。演繹定理(Deduction Theorem, 「Γ,α⊢β ⇔ Γ⊢α→β」)を使ってしまえば良かったのか。そりゃそうだ。
2004-11-06 [長年日記]
λ. 238 盆地の村
ヴァルターとカタリナのペアを疑ってはいたんだけど、結局正解にたどり着くことは出来なかった。参加者じゃないけど、ちょっと悔しい。
λ. RHG読書会::東京 Reloaded
先月は行けなかったので、久しぶり。
2004-11-07 [長年日記]
λ. Fireman vs Bass
ラブ・ファミコン より。ロックマン懐かしいなぁ。「Pest Exterminator」というランクにちと笑った。スクリーンショット
λ. 圏論勉強会開催予定が決定
[haskell-jp:471] 圏論勉強会開催(第一回)によると、圏論勉強会の日取りが決まったそうですよ。
2004-11-08 [長年日記]
λ. ニューラルコンピューティング
なんか武藤先生がいつもと違ーうと思ったら、教室間違えてた。orz
グラフの平面化問題。頂点のどっち側にエッジがあるかを表すために、|V|×|E|×2のニューロンを割り当てればいいと考えてたのだけど、2次元から1次元に還元してしまうというのには気付かなかった。そうすれば問題がシンプルになるし、必要なニューロンの数も少なくなるもんなぁ。なるほど、なるほど。
ところで、n-Queenや4色問題を解くためのニューラルネットの motion equation を自分でも考えてみたけど、結局のところ俺は motion equation がいまいち分ってないんだよなぁ。「発火によって制約条件に近づくなら正に、そうでない時に負になるように組み立てる」というのは自明だし、これまでの例ではそれは簡単だった。だけど、制約条件の複数の表現方法の内でどれが優れているのか、また複数の制約条件をどのように組み合わせるかとった点がピンとこない。また hill-climbing の項をどう選択するのかもピンとこない。このあたりって結局ヒューリステックでしかないのだろうか?
それはそうと、NP問題のNPをNon-Polynomialと説明するのはどうかと思った。
λ. 『風の大陸 氷の島1』, 竹河 聖
読んだ。
2004-11-10 [長年日記]
λ. Method#to_proc
lambda{|&f| f.call }.call{ p :ok } #=> ok def foo(&f) f.call end method(:foo).to_proc.call{ p :ok } #=> undefined method `call' for nil:NilClass (NoMethodError)
Method#to_procで作ったProcにはブロックが渡らないのかな。(ruby 1.9.0 (2004-11-10) [i386-cygwin])
[追記] [ruby-dev:25031]
[追記] eval.c (rev 1.742) で修正された。
2004-11-11 [長年日記]
λ. 自己嫌悪。
λ. すりかえられたselfにCからアクセスするには?
instance_evalやdefine_methodを使うとselfがすりかえられた状態でブロックが実行される。rb_iterate()やrb_proc_new()を使ってCの関数をブロックとして与えた場合、Cの関数からこのselfにアクセスするにはどうしたら良いか?
まず思いつくのは ruby_frame->prev->self
だけど……
って、よく見たら第三引数としてselfが渡されてるか。これもUndocumentedっぽいから大差ないかもしれないけど。
2004-11-12 [長年日記]
λ. 数学への想像力と情熱
『The Dot and the Line: A Romance in Lower Mathematics』の感想をIRCから転載)
For Euclid, no matter what they say.
Once upon a time there was as sensible straight line who was
hopelessly in love with a dot.
という書き出しで始まるこの絵本は、なんと「直線」と「点」の恋愛物語だ。
見た目も心もまっすぐな the line、 完璧な美しさを備えながらも軽薄な the dot、 ワイルドでだらしない the squiggle。 the line は the dot に恋するが、彼女は the squiggle に夢中で……
ストーリーについて書くのは気恥ずかしいのでこの辺りにしておくが、 図形という抽象的なキャラクタを主人公とすることで、 普遍性のある寓話になっているように感じられる。 またオチもニヤリとさせられるものであった。
とかく、数学というのは無味乾燥で非人間的と思われがちだが、 ただの図形達からここまで想像することの出来る想像力、 そして茶目っ気たっぷりのお遊びには心が躍った。 また、著者が自分で描いたという挿絵もとても魅力的で、この物語にあっている。 これを読めば数学が無味乾燥だなんて二度と思わないはず。
- Quotation
- “Freedom is not a license for chaos,”
- Excellent Translation
- 「自由は無秩序の専売特許じゃない」
- Explanation
- 情熱を表現するために「自由」になろうとし、 努力の果てにそれを手に入れた the line のセリフ。
λ. どんな境遇にあっても、頭脳さえあれば
("A Genius in a Wheelchair Stephen Hawking" の感想をIRCから転載)
ホーキングの名を知らない人はいないだろう。 本書はスティーブン・ホーキングの足跡と研究について、専門用語等を用いず に、一般向けに書かれている。
この文を読んでいる人の中には情報理論について勉強/研究している人も多い と思う。そういった人たちの中には、熱力学のエントロピーと情報理論のエン トロピーが実は等しいという話に関連して、彼の名前を知っている人が多いの ではないだろうか。
それはさておき、ホーキングは、筋肉と末端の神経が機能しなくなっていき、 やがては呼吸すらも出来なくなる難病ALS(筋萎縮性側索硬化症)というハンディ キャップを背負いながら、研究を続け、今や現代を代表する科学者となってし まった人物である。
頭脳さえあれば研究できる宇宙論という領域を選んでいたという幸運もあった だろう。ホーキング自身も“My handicap does not interfere with studying cosmology”と語っている。だが、彼の成功は「どんな境遇にあっても、頭脳 さえあればクールなことは出来る」ということを実証しているに思われる。我々 の多くはホーキングの様な過酷な境遇にはないだろうが、少しは見習いたいも のである。
また、彼の陽気さ、社交性、ユーモアについても惹かれるものがある。 The power of his energy for life might be slowing down the progress of ALS disease. と書かれているが、そうであって欲しいものである。
それにしても、我々人間の様な小さな存在が、この広大な宇宙について理解し ようとし、そしてこれだけの理論を組み立ててしまったことは、全く驚くべき ことである。だが、その行き着く果てであるはずの万物の理論はいまだ見えな い。ホーキングらの超ひも理論やM理論の先にあるのか、VSL(光速変動理論) の先にあるのか、それとも……
- Quotation
- “Why? Why? Why” This is the word and the message Dr. Hawking is giving to us all.
- Excellent Translation
-
「何故? 何故? 何故?」
これはホーキング博士のの言葉であり我々へのメッセージです。 - Explanation
- ホーキング博士は既存の理論等に囚われず、 子供のように「何故? 何故? 何故?」という疑問を捨てなかった。
2004-11-13 [長年日記]
λ. AVL木でGADTを試してみる
Programming in Haskell の Programming:玉手箱:その他 で花谷さんが書いていたAVL木のコードをたまたま見て、GADT を試すいい機会と思い、GADT で「左右の木の高さの差が高々1以下」という制約を表現するように書きかえてみた。AVL.hs
花谷さんのコードではbalance関数を挿入用と削除用で共有するようになったが、このコードだと(処理は同じなのに)型が違うために共有出来ていない。型をうまく定義すれば共有できる?
AVL木でGADTを試してみる(2) に続く...
2004-11-14 [長年日記]
λ. RTDSC.hsc
module RDTSC (rdtsc) where import Foreign #def inline unsigned long long exec_rdtsc(void){ asm(" rdtsc"); } foreign import ccall unsafe "exec_rdtsc" rdtsc :: IO Word64
そういえば、以前にこんなモジュールを書いたことがあったのだけど、GHC 6.2.1 だと何故か常に0が返ってきて、inline
を消さないと期待通りの動きをしなかった。これは何でだろう?
2004-11-15 [長年日記]
λ. Concurrent Haskell と FFI
次のようなプログラムをGHCでコンパイルして実行するとプロセスが暴走するっぽい(Windows版とLinux版のGHC 6.2.1 で確認)。原因は良くわからないが、Concurrent Haskell と FFI の組み合わせには気をつけようと思った。
import Control.Concurrent import Foreign foreign import ccall foo :: FunPtr (IO ()) -> IO () foreign import ccall "wrapper" mkCallback :: IO () -> IO (FunPtr (IO ())) main :: IO () main = do mvar <- newEmptyMVar callback <- mkCallback $ mapM_ (putMVar mvar) [0..2] forkIO $ foo callback takeMVar mvar return ()
void foo(void (*bar)(void)) { bar(); }
まだ良く理解してないのだけど、ひょっとして次のようなことが起こっている? foo
を実行するOSスレッドA(Worker Threadではない)は mapM_ (putMVar mvar) [0..]
を実行するためのCHスレッドαを生成し、その終了を待つために眠る。その間に別のOSスレッド(Worker Thread)によってメインのCHスレッドの処理が進んで終了し、他の全てのCHスレッドも殺されてしまう。αに先に死なれてしまったAが変なことになってる?
2004-11-16 [長年日記]
λ. Making a fast curry: push/enter vs. eval/apply for higher-order languages, Simon Marlow and Simon Peyton Jones
を読んだ。カレーを速く作るためにはどうしたらよいかという論文……ではない。push/enterの方が速いと思ってたけどeval/applyの方が速いのか。へぇ。読んで納得。GHCも6.0からはeval/applyになってますね。
2004-11-17 [長年日記]
λ. Lazy Depth-First Search and Linear Graph Algorithms in Haskell, David J. King and John Launchbury
を読んだ。scc :: Graph -> Forest Vertex; scc g = dfs (transposeG g) (reverse (postOrd g))
で強連結成分を計算出来たりしてカッコイイ!
2004-11-19 [長年日記]
λ. 今日の夢
「イタイ人、イタイ人、飛んでけー」というフレーズだけが頭に残ってる。
λ. AVL木でGADTを試してみる (2)
AVL木でGADTを試してみる の続き。
ちょっと工夫して挿入時と削除時のバランス用の処理を共有してみた。高さnでバランスしている状態から右(左)のサブツリーが高くなった状態は、高さn+1でバランスしている状態から左(右)のサブツリーが低くなった状態と同じであることを利用した(高さに下限があるからその逆には出来ないので注意)。AVL2.hs
2004-11-20 [長年日記]
λ. 第一回圏論勉強会
- CategoryTheory:圏論勉強会 (sampou.org, Programming in Haskell)
λ. CPLのHaskell版を公開
公開するのを忘れてたのを思い出したので、とりあえず公開しておこう。やる気のないパーサとか、あとトレースを有効にしたときのメモリ使用量とか、色々と気に入らないところはあって恥ずかしいけど。
2004-11-21 [長年日記]
λ. hyperset
以前にRubyで実装したコードを、最近Haskellで書き直すために見返していたのだけど、自分がとんでもなく愚かだったことに気付いてしまった。コンセプトを反映していない識別子名とかアルゴリズムの効率の悪さは置いておくとしても、bisimilarかどうかの判定を誤っているってのは致命的。こんなんで正しく判定できるわけないじゃん。しかも、それを一年近く気付いてなかったとは……俺のバカバカバカ。恥ずかしすぎる。ああ、多分今年一番の恥ずかしさじゃなかろうか。orz
2004-11-22 [長年日記]
λ. RegEx Tシャツ
「軽量言語の次はこれ!」らしいですよ。
http://explanation-guide.info/image/180px-Airkz_20040617_jon_regular_expression.jpg.html
λ. Bisimulation Algorithm
このままじゃ恥ずかしすぎるので、hyperset.rb(と未公開のHaskell版実装)を直そうと思いたったのだけど、また自分で考えると何か間違えそうなので、既存のアルゴリズムを探すことに。そこでGoogle先生に尋ねると A. Dovier, C. Piazza, and A. Policriti. A fast bisimulation algorithm. TR UDMI/14/00/RR, Udine, 2000. というのがあったので、これを使わせてもらおう。Non-Wellfounded な場合にはそうやってrankを定義できるのかぁ。なるほど、なるほど。
で、Haskellで試しにコードを書いてみようとしたのだけど、Paige-Tarjan の手続きを呼ぶとしか書かれてない部分があって困ってしまった。R. Paige and R. E. Tarjan. Three partition refinement algorithms. SIAM Journal on Computing, 16(6):973-989, 1987. に書いてるらしいのだが、この論文Web上にはないし、調べるの面倒なので、試しにこれ抜きでやってみる。幾つかの例を試すとこれでも正しく動作しているように見えるが……ダメな例を早速発見。Ω={Ω} として、α = {Ω,φ} と β = {Ω,φ,{Ω,φ}} が区別できないな。この二つは共にrankが1で、rankがこれより小さいのはrankが−∞のΩとrankが0のφ。α,βは共にΩとφを含んでいるので、Ωとφによる分割だけではα,βは区別できない。同じrank内でさらに分割する必要があるけど、それにはどうしたら良いのかなぁ。うーむ。
何が足りないのかとしばし悩んで(足りないのは Paige-Tarjan の手続きに決まってるけど)、{{Ω},{φ},{α,β}} という分割(によって定義される同値関係)はstableでないことに気付く。
ちなみに、関係R⊆N×Nが与えられたとき、Nの分割Pの任意のブロックB1,B2に対して、B1⊆R-1(B2)とB1∩R-1(B2)=φのいずれかが成り立つとき、Pは関係Rに関してstableだという。あるいは、分割Pによって定義される同値関係を≡Pとして、(∀a,a',b∈N)((a≡Pa' ∧ a R b) ⇒ (∃b'∈N)(b≡Pb' ∧ a' R b')) という定義の方が直観的かな。
閑話休題。さっきの例だと N = {Ω,φ,α,β}, R = ∋ なので、P = {{Ω},{φ},{α,β}} だと、B1 = B2 = {α,β} としたとき、R-1(B2) = {y | x∈{α,β}, y∈N, y ∋ x} = {β} となってしまい、Pはstableな分割ではないことがわかる。maximal bisimulation はstableであるはずなので、この同値関係は大きすぎる(i.e. 分割が粗過ぎる)ことが判定できる。試しにstabilizationの処理を素朴に実装して見たら、αとβは区別できるようになったし、試した限りでは他の例でも正しく動いているように見える。
ということは、Paige-Tarjan の手続きってのはstabilizationのための効率的なアルゴリズムのことなのかな? (ぉぃ
……とか書いてたら、バークレイ大のCS 294-1: Model Checking, EE 219C: Computer-Aided Verificationという授業の講義資料に Graph Minimization というのを発見。まだ読んでないけどとても良さそう。
あと、A fast bisimulation algorithm の著者のサイト にC++のコードがあるのも発見。
2004-11-23 [長年日記]
λ. cpoとか
らくがきえんじん(2004-11-13) でcpoの話を見かけて、cpoという単語は複数の意味で使われていて紛らわしかったのを思い出した。私の知ってるのだとこんな感じだったかな。
- 有向集合 (directed set)
- ≦を集合X上の擬順序(preorder)とする。部分集合S⊆Xは、任意の有限部分集合T⊆SがS内に上限を持つ(∨T ∈ S)とき有向集合。(空集合の上限が存在するのでSは空集合ではない)
- dcpo (directed complete poset)
- 任意の有向な部分集合が上限を持つ半順序集合。この上限は ∨↑ S 等と書かれる事もある。
- cpo (complete poset), ipo (inductive partial order)
- 最小元⊥を持つdcpo。下のcpoと区別するためにipoと呼ばれることも。
- cpo (complete poset), pointed cpo
- 最小元⊥を持ち、任意の無限上昇列(ω-chain)が上限を持つ半順序集合。ω-chainの上限は ∨i=0∞xi 等と書かれる事もある。下の最小元⊥を持たないやつをcpoと呼ぶ場合にはこっちは pointed cpo と呼ぶ。
- cpo (complete poset)
- 任意の無限上昇列(ω-chain)が上限を持つ半順序集合。最小元⊥は持たなくてもよい。
- ω-algebraic dcpo
- 任意の有向な部分集合がω-chainを含んでいて、有向集合の上限とω-chainの上限が一致する algebraic dcpo。
2004-11-24 [長年日記]
λ. hyperset
一昨日書いた最初の実装だと、Ω= {Ω}, A = {0..9}, ℘(X)をXの冪集合として、℘({℘3(Ω), ℘4(φ), {{A}}} ∪ A) を計算するのに一分以上かかっていたので、プロファイラの結果を見ながら色々とチューニング。約4秒まで縮まった。まだ不満はあるけど、とりあえずこんなもんか。
λ. 『新・土曜ワイド殺人事件—京都藁人形殺人事件』, とり みき, ゆうき まさみ
を読んだ。
2004-11-27 [長年日記]
λ. hyperset
urelementの存在を許しているので、member関数の型はtype UrelemOrSet u = Either u (Set u)
として、(Ord u) => UrelemOrSet u -> Set u -> Bool
という型になってしまっていて、少し扱いにくい。もしHaskellがスーパータイピングをサポートしていたら、UrelemOrSet u
をSet u
のスーパータイプとして定義することで少しはすっきりしそうだが……
とりあえず現在のスナップショットを公開しておこう。
2004-11-28 [長年日記]
λ. "top-downのmemoization" と histomorphism
"top-downのmemoization" の一引数の場合というのは、V. Vene. Categorical programming with inductive and coinductive types.(2004-06-29の日記参照) の histomorphism に非常に近いなぁと思った。
まず、yts氏による定義は以下のようなものだった。
fib :: Int -> Int fib = memo1 ( xs -> case n of 0 -> 0 1 -> 1 _ -> xs !! 1 + xs !! 2) memo1 :: (Int -> [a] -> a) -> Int -> a memo1 f n = head $ memos1 f n memos1 :: (Int -> [a] -> a) -> Int -> [a] memos1 f n = rs where rs = m n rs m n ~xxs@(x:xs) = (f n xxs):m (n - 1) xs
これは少し複雑なので単純化する。
memos1
の f n xxs
に注目すると、
xxs
の先頭要素はf n xxs
自身になっているが、この先頭要素は普通使われないので、xxs
の代わりにxs
を渡すことにしよう。- 負の定義域を考慮しているためか、
xs
は無限リストになっている。定義域を自然数に限定してxs
を有限のリストにしてしまおう。 - そうすると、
xs
の長さからn
の情報が復元できるので、n
もパラメータとして渡す必要はない。
そうして単純化して少し書き換えると、以下の様な定義が得られる。
fib :: Int -> Int fib = histo phi where phi [] = 0 phi [_] = 1 phi (a:b:_) = a+b histo :: ([a] -> a) -> (Int -> a) histo phi = head . f where f 0 = phi [] : [] f (n+1) = phi xs : xs where xs = f n
正確な定義は省くが、このfib
のように定義されている関数はhistomorphismと呼ばれる。これは(Intで表現された)自然数に関するhistomorphismだけど、histomorphismの概念はリストや木といった帰納的なデータ型一般に適用することが出来る。前述の V. Vene. Categorical programming with inductive and coinductive types. ではpolytypicなhisto
を使ってfib
を以下のように定義していた。これも詳細は省くけど、対応しているのが分かると思う。
fib :: Nat -> Int fib = histo phi where phi Z = 0 phi (S x) = case tlCV x of Z -> 1 S y -> hdCV x + hdCV y
(2005-09-04 追記) ちなみに、Category extras パッケージ を用いると以下のようになる。やっていることは同じなのだけど、histoの型が「Fixpoint f t => (f (Strf f a) -> a) -> t -> a」になっていて、また「instance Fixpoint Maybe Int」と定義されているので、引数の型がNatではなくIntになっている。
import Control.Recursion import Data.BranchingStream fib :: Int -> Int fib = histo phi where phi Nothing = 0 phi (Just x) = case tlf x of Nothing -> 1 Just y -> hdf x + hdf y