日々の流転

λ. 課題などが一段落ついて、久しぶりにピアノを引き、読書し、溜ったメールを読み、コードを書き、有意義な一日であった。

λ. Be afraid! It's shiny, it's new, it's unstable, it's b0rken, it's The GIMP 1.3 !!

いぇーい。つーわけで、1.3.0っす。

λ. マルチバイトキャラクタを扱う決定性有限状態オートマトンの構成法

むむ。なんとなく面白そうだったので情報数学Ⅰのメーリングリストで紹介してみる。そーいや、Rubyの正規表現エンジンはNFAだったよね。

λ. mlterm-1.9.42

を入れてみた。TODO.pubに「中東アラブ系言語(BIDI) xtermの実装を調べる」とあるから、BIDIってのはやはりターミナルレベルで処理されるものなのか。

あと、「ISO2022の、ESC % / 指示に対応(...したくない)」ってのを見て、やっぱ苦労するもんなんだなぁと思った。

λ. 情報数学Ⅰ

SAの仕事として頼まれていた授業ページに手をつけはじめた。とりあえず、メーリングリストアーカイブを検索できるようにしただけ。

λ. 今日のパッチ

[ruby-list 32331]

PStore#transactionでファイルのオープンに失敗した場合にNameErrorになってしまっていたので

[ruby-ext 1669]

wstringへの細かなパッチ3つ

λ. 萩野服部研

進捗報告。まー、いーじゃんJenaで。僕にとってもJavaに触ってみるいい機会かも知れないしね。

λ. 日本で配布されているRSS/RSS # 独自生成

に、私が遊びで提供していたRSSが登録されているのを清水さんが見つけてきて、ビックリした。証拠写真

λ. 東方紅魔郷

ノーコンテニューで4面ボスまで到達。

λ. 久野君の極悪さを目の当たりに

久野君の極悪さを目の当たりにした。背筋が凍る。「敵には回したくない」と本気で思ってしまった。気を付けろ!! ヤツは羊の皮をかぶった狼だ……

λ. ブレスオブファイアⅤ ドラゴンクォーター

発売か。とても興味はあるのだけど、多分買わないと思う。プレイする時間が無いというのもあるけど、以下のフレーズから想像するストーリィは、僕にはとても恐ろしく感じられるから。

この世界で 生きるしかない としても
このまま 生きる方が 楽だとしても
その先に 何があるか 分からなくても
知らない方が 幸せ だとしても
たとえ 世界を壊してしまう としても

このストーリィの一つの原型は、やはりⅢのストーリィだと思うのだ。リュウは自らの運命に出会い、自らの道を選択し、そして結果として世界の庇護者を滅ぼしてしまう。彼が、自らの選択の帰結を理解していなかったはずは無い。庇護者である女神を失った世界がどうなるかも、その世界に生きる力無き者がどうなるかも……、それを全て理解した上で、自らを曲げず、しかも後悔しない。その精神がただ純粋に畏ろしい。その自己肯定と運命愛が……

それと、今回の「後悔はない」と執拗に繰り返し、最後に「そうだろう?」と問いかけるムービー(「東京ゲームショウ 2002 スポット 後悔はない編」)には「運命を愛し肯定しても、なお癒せない渇き」のようなものを感じてしまい、それもまた恐ろしいのだ。

λ. GCCでインラインアセンブリを使用する方法と留意点等 for x86

.

λ. 帰り

に珍しく石川さんに会う。

ふと、上遠野浩平の文体を模写しようとする人っていないのだろうかと思った。

λ. Rubyの話題が無くてすんまそん

最近、Rubyの話題が全然無くてすんまそん。

λ. 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を消さないと期待通りの動きをしなかった。これは何でだろう?

λ. Haskell Bowling by Ron Jeffries

<URL:http://d.hatena.ne.jp/machi_pon/20061104> より。 実はこれまでボーリングのスコアの定義を知らなかったのだけど、こういう風に定義されているのか。

λ. 強い直和?

強い直和(strong sum)とCCに関して混乱中。

強い直和と弱い直和

以下の推論規則からなる型を「強い直和」と呼ぶ。

Γ, a : A ├ B : *
──────────
Γ ├ (Σa:A. B) : *

Γ ├ t : A   Γ ├ u : B[a := t]
─────────────────
Γ ├ (t,u) : Σa:A. B

Γ ├ t : (Σa:A. B)
───────────
Γ ├ fst t : A

Γ ├ t : (Σa:A. B)
──────────────
Γ ├ snd t : B[a := fst t]

それに対して、この推論規則の最後の二つを以下の推論規則で置き換えたものを「弱い直和」と呼ぶ。

Γ ├ t : (Σa:A. B)  Γ ├ C : *  Γ ├ e : (Πa:A. B→C)
─────────────────────────────
Γ ├ elimSum t e : C

CCと強い直和

CCには強い直和は含まれないが、弱い直和は以下のようにCC内で定義できる。

Σa:A. B = ΠX:*. (Πa:A. B → X) → X
(t,u) = λX:*. λe:(Πa:A. B → X). e t u
elimSum t e = t C e

そして、CCに強い直和を追加するとGiraldの逆説が成り立つことになっている。

が

しかし、強い直和も以下のようにCC内で定義できる気が……間違っているのはどこだ?

fst t = t A (λa:A. λb:B. a)
snd t = t ((λa:A. B) (fst t)) (λa:A. λb:B. b)

まとめ

sumiiさんの指摘でようやく理解できたが、(λa:A. λb:B. b) の型付けに問題があるのが原因だった。実際、Agdaで以下のように書いてみても、最後のゴールがrefine出来ない。AgdaはCCのようなimpredicativeな言語ではないけど、この例が型付けできないことを示すには十分だろう。

Sum :: (A::Set) -> (A->Set) -> Type
Sum A B = (X::Set) -> ((a::A) -> B a -> X) -> X

pair (|A::Set) (|B::A->Set) :: (a::A) -> B a -> Sum A B
pair a b = \(X::Set) -> \(f::(a'::A) -> B a' -> X) -> f a b

elimSum (|A::Set) (|B::A->Set) (|X::Set)
    :: Sum A B -> ((a::A) -> B a -> X) -> X
elimSum t f = t X f

fst (|A::Set) (|B::A->Set) :: Sum A B -> A
fst t = t A (\(a::A) -> \(b::B a) -> a)

snd (|A::Set) (|B::A->Set) :: (t::Sum A B) -> B (fst t)
snd t = t (B (fst t)) (\(a::A) -> \(b::B a) -> {! b !})

ちなみに、The Theory of Parametricity in Lambda Cube でも同じ間違いをしていた。

関連

• ECC, an Extended Calculus of Constructions - ECCはCCを拡張して強い直和を導入した型理論

λ. HaskellのDynamicはあまり使えない

現在のHaskell(GHC)のDynamicは言語的なサポートがないため、Cleanのそれに比べると記述能力の点で非常に貧弱で、ユーザー定義の型を例外として投げるとかそのくらいの用途にしか使えない。

例えば、dynFst (toDyn (a,b)) = Just (toDyn a) を満たすような関数 dynFst :: Dynamic → Maybe Dynamic すら a, b の型を予め特定の型に決めないと記述することが出来ない。fromDyn等によって値を取り出す際には、Typeableのインスタンスとして型を取り出すわけだけど、これはTypeRepで型を指定していることに等しく、TypeRepは型変数を含まないため。 言語拡張にしてしまえば、このような関数を(安全に)記述できるようにすることはそう難しくはないはずなんだけど。

λ. 「プログラムの安全性を高めるために—今注目を集める関数型言語に迫る—」

『圏論の基礎』の翻訳等で有名な三好先生による関数型言語の紹介。 三好先生の写真初めて見た。

λ. HIMA #2 「Typeclassopedia」

今回は The Typeclassopedia の話。

関連

• ログ
• The Monad.Reader Issue 13 (The Typeclassopedia 原文)
• The Typeclassopedia 日本語訳
• 自分で作る Num の instance - あどけない話 (2009-11-16)