日々の流転

λ. 年末年始

今回の年末年始は非常に日本人らしい過ごし方をした。 31日はコミケに行き、夜は紅白歌合戦を見て、除夜の鐘をつきに行った。 そして、年が明けた後は、(家からだけど)初日の出を見て、それから初詣にも行ってきた。 たまにはこういう季節感のある正月もいいなと思う。 ちなみに、おみくじは大吉だった。 今年は良い事がありそうだ。

λ. PLDIr #5

PLDIの論文を読む PLDIr の第五回に参加。 今回はPLDI2001の論文が対象で、私は以下の3本の論文を紹介した。

• Design and Implementation of Generics for the .NET Common Language Runtime (著者版)
• Automatic Predicate Abstraction of C Programs (著者版)
• The Pointer Assertion Logic Engine (著者版)

Design and Implementation of Generics for the .NET Common Language Runtime は、文字通り.NETのCLRにパラメトリック多相を実装する話。 JVMや当時のCLRは多相をサポートしてないので、多相をコンパイルしようとすると性能、プリミティブ型の扱い、コンパイルの複雑さなどの問題がでる。 なので、CLRレベルでちゃんとサポートしようという話。 伝統的なコンパイル・リンク・実行というモデルではなく、CLRの動的なコード生成やJITを活用した設計になっていて、実行時にコードのspecializeを行う。 厳密な実行時型もサポートし、またプリミティブ型によるインスタンス化も性能を低下させずに実現。 vtable内に型パラメータとオープンな型のスロットを用意する点などが面白かった。

Automatic Predicate Abstraction of C Programs はソフトウェア向けモデル検査器SLAMで抽象化を行っているツールC2BPの詳しい話。 C2BPは、CプログラムPと述語の集合Eから、述語抽象化した Boolean program B(P,E) を生成する。 この Boolean program の生成は自明な話だと思っていたけど、元のプログラムのコードに対応して、どの述語の真偽がどう変化するかを判定するのは結構工夫が必要で、面白かった。

The Pointer Assertion Logic Engine は、PALE(the Pointer Assertion Logic Engine)というツールについて。 PALEは、ヒープの構造に関する性質を Pointer Assertion Logic というロジックで、アノテーション(事前条件・事後条件・不変条件)として記述し、プログラムとアノテーションを、WS2S(weak monadic second-order theory of 2 successors)に変換してMONAで検証する。 記述可能な性質は Graph types と呼ばれているもの。

以前にMONAで正規表現にマッチする例を生成したりしたけど、MONAってこんなことも出来るのか、と驚いた。 そういえば、計算機言語で定理証明 (Proof Party.JP) - ヒビルテ(2009-10-24)のときに触ってみたJahobも、決定手続きの一つとしてMONAが利用可能だったけど、同じような感じで使ってるのかなぁ。

発表資料 (PDF):

関連

• Asynchronous Exceptions in Haskell - ヒビルテ(2009-11-08)

λ. Real World Haskell読書会 2010-01

9章 入出力事例研究: ファイルシステム検索ライブラリ

p.236 の foldTree の walk は末尾再帰的ではないと思った。

エディタで行を折り返さない場合のことは何と呼ぶのが普通なのかな。

蓄積しつつ，畳み込む． - HaHaHa!。 mapAccumとかで頭の爆発する私にはこれを使いこなすのは無理だw

「ひょっとして白石さん」bot。

関連

• RWH 読書会 2010-01 - 日曜プログラマがダラダラ書く

λ. 第六十回圏論勉強会

今日は圏論勉強会。 某氏のD論の話を紹介してもらう。

関連

• 圏論勉強会 一旦終了のお知らせ - たけをの日記＠天竺から帰ってきたよ

λ. HIMA #4: Functional Reactive Programming

Haskellプログラミングに興味をもつ人が、とりとめなく、おしゃべりをするという会である、HIMA(Haskell Internet Meeting Anytime)の第4回を開催した。 今回のお題は Functional Reactive Programming (FRP) で、maoeさんの素晴らしいReactive紹介記事をネタにおしゃべり。

• 会場(Google Wave)
• ログ (ミラー)
• ログ(PDF) (ミラー)
• ログ＠Walkaround
• maoeさんのReactive紹介記事:
  • やさしいFunctional reactive programming（概要編）
  • やさしいFunctional reactive programming（Event編）
  • やさしいFunctional reactive programming（Behavior編）

λ. 継続操作を持つEDSLをHaskell上で実装する

ranhaさんが Yet Another Ranha (2010-01-01), Yet Another Ranha (2010-01-04) あたりで悩んでいた話を言語雑談会で少し聞いた。 何をやりたかったのかイマイチ良くわかっていないけど、とりあえず↓みたいな感じだろうか。しかし、継続モナドでいいじゃんという気も。

{-# LANGUAGE EmptyDataDecls, GADTs, TypeFamilies #-}

data Void
type Not a = a -> Void
type T a = Not (Not a)

data Exp t where
   Lam :: (Exp a -> Exp b) -> Exp (a -> b)
   App :: Exp (a -> b) -> Exp a -> Exp b
   A :: Exp Void -> Exp a
   C :: Exp (T a) -> Exp a
   Wrap :: Star a -> Exp a

type family Star t
type instance Star Void = Void
type instance Star Int = Int
type instance Star (a -> b) = Star a -> T (Star b)

cps :: Exp t -> T (Star t)
cps (Lam f) k = k (\a -> cps (f (Wrap a)))
cps (App e1 e2) k = cps e1 (\f -> cps e2 (\a -> f a k))
cps (A e) k = cps e id
cps (C e) k = cps e (\f -> f (\v _ -> k v) id)
cps (Wrap v) k = k v

限定継続なし版 - Yet Another Ranha (2010-01-27) に続く。

追記

しかし、これが型付けできるってのには結構驚いた。

これと同じようなことを class Star t t' | t -> t' みたいな型クラスを使ってやろうとすると、App構成子に文脈をつける必要があるはず。 でないと、e1 :: Exp (a -> b), e2 :: Exp a としたときに、cps関数のAppの場合の定義で、Star b b' の文脈だけからは Star a a' を導けなくて困ったことになってしまう。

型クラス+関数従属性で表現できるのは型上の部分関数であって、インスタンス宣言しているところにだけ定義されるのに対して、型族は型上の全域関数であって、インスタンス宣言は具体的な表現に触るときにだけ必要ということか。 型族は型クラスの関数従属性の置き換えとして紹介されることが多いけど、実際の使い方はずいぶん違うように感じるなぁ。

関連

• @keigoi
  • <URL:http://twitter.com/keigoi/status/8329484270>
  • <URL:http://twitter.com/keigoi/status/8341823894>
  • <URL:http://twitter.com/keigoi/status/8342082624>
  • <URL:http://twitter.com/keigoi/status/8342427877>
  • <URL:http://twitter.com/keigoi/status/8342751070>
• @ranha
  • <URL:http://twitter.com/ranha/status/8353039440>
  • <URL:http://twitter.com/ranha/status/8353067468>
  • <URL:http://twitter.com/ranha/status/8353102433>

λ. 結合的でない二項演算

言語雑談会で、圏の公理から射の合成の結合律を取り除いたらという話が出たのだけど、例を考えるのに苦労していたので、Alloyで結合的でない二項演算を適当にでっち上げてみた。

• (2・1)・2 = 1・2 = 0
• 2・(1・2) = 2・0 = 2

モノイドは対象が一個だけの圏なので、この例も対象が一個だけだと思えば、射の合成の結合律を除く圏の公理は満たす。 まあ、特に面白い例ではないけど。

λ. “Runtime support for multicore Haskell” by Simon Marlow, Simon P. Jones, Satnam Singh

In ICFP '09: Proceedings of the 14th ACM SIGPLAN international conference on Functional programming (2009), pp. 65-78.

• <URL:http://dx.doi.org/10.1145/1596550.1596563>
• 著者版
• 著者版

を読んだ。 Parallel Haskell に着目してGHCのランタイムのデザインを見直したという話。 Haskell忘年会のときのmaoeさんの発表で面白そうだったので読んでみた。 色々な改善点があるのだけど、GC周りの話とかは色々面白かった。

通常の並列のコピーGC(copying GC)では、重複してコピーしないためにHEC(Haskell Execution Context, ≒CPU)間で同期を行う。 だけど、実際に重複してコピーされるのはまれだし、Haskellの場合そもそも大多数のイミュータブルなオブジェクトは重複してコピーされても別に問題ないので、ミュータブルなオブジェクトのコピー時にしか同期をとらないようにしたというのは、「おおぉ」と思った。

それから、並列GCのHEC間のロードバランシングを無効にしたほうが速いという話も驚いた。これはその方が局所性が高くなるから。他にもかなり局所性は意識していて、ナイーブにロードバランシングしてるだけじゃだめなんだなぁ、と思った。

Strategiesの話はよく知らなかったので勉強になった。 spark pool のGCとStrategiesの話は悩ましそうだ。

他の、CPU間のsparkのロードバランシングに bounded workstealing queue を使うようにしたとか、spark毎にHaskellスレッドを生成するのではなくバッチ処理するようにしたとかは、地道に改善しているなという感じ。

関連

• Haskell on a Shared-Memory Multiprocessor - ヒビルテ(2006-04-24)

λ. “Stream fusion: from lists to streams to nothing at all” by Duncan Coutts, Roman Leshchinskiy, Don Stewart

• <URL:http://dx.doi.org/10.1145/1291220.1291199>
• 著者版

リスト処理を、以下のようなストリーム型*1に対する処理に置き換えることによって、foldl等の最終的にリストを消費する関数以外は非再帰的な定義にする。そして、通常の最適化によって、中間データ構造を削除する。

data Stream a = ∃s. Stream (s -> Step a s) s
data Step a s = Done
              | Yield a s
              | Skip s

例えば、sum (xs ++ ys) は、 sumの定義の展開と書き換え規則の適用によって foldl_s (+) 0 (append_s (stream xs) (stream ys)) となり、 定義を展開することで以下のようになる。

let next_stream xs =
      case xs of
        [] -> Done
        x : xs' -> Yield x xs'
    next_append (Left xs) =
      case next_stream xs of
        Done -> Skip (Right ys)
        Skip xs' -> Skip (Left xs')
        Yield x xs' -> Yield x (Left xs')
    next_append (Right ys) =
      case next_stream ys of
        Done -> Done
        Skip ys' -> Skip (Right ys')
        Yield y ys' -> Yield (Right ys')
    go z s =
      case next_append s of
        Done -> z
        Skip s' -> go z s'
        Yield x s' -> go (z + x) s'
in go 0 (Left xs)

そして、ここからGHCのごく普通の最適化によって以下と同等のプログラムになる。

let go z (Left xs) =
      case xs of
        [] -> go z (Right ys)
        x:xs' -> go (z+x) (Left xs')
    go z (Right ys) =
      case ys of
        [] -> z
        y:ys' -> go (z+y) (Right ys')
in go 0 (Left xs)

さらに、Constructor Specialization (Call-pattern specialisation) と呼ばれる最適化を用いると、以下と同等になる。

let go1 z xs =
      case xs of
        [] -> go2 z ys
        x:xs' -> go1 (z+x) xs'
    go2 z ys =
      case ys of
        [] -> z
        y:ys' -> go2 (z+y) ys'
in go1 0 xs

簡単な書き換え規則とごく普通の最適化機能だけで、中間データ構造を除去できているのが素晴らしい。 また、foldr/build の short-cut fusion と比べても、zipWithのような複数引数のものや、concatMapのようなネストしたリスト構造を扱うものも融合出来ると。

λ. 2009年振り返り

ずいぶん遅くなったが、2009年を振り返っている。 とりあえず、月毎の印象的な出来事を列挙してみる。

1月

圏論勉強会で S. Abramsky "Temperley-Lieb algebra: From knot theory to logic and computation via quantum mechanics"を終えた。 ヒビルテ(2009-01-11)

2月

圏論勉強会で、新しいテキストとして Peter Selinger による絵算のサーベイ論文“A survey of graphical languages for monoidal categories”を読み始めた。ヒビルテ (2009-02-08)

3月の海外行きに備えて、英会話学校のgabaに通い始める。 2008年末辺りからいくつか英会話学校を検討してたけど、悩んでいて始めるのが遅れた。

3月

圏論勉強会で、量子情報の研究者を迎えて、量子情報のセミナー。 量子コンピュータ向けの関数型プログラミング言語QMLについて紹介するなどしてみる。

PPL2009に参加、発表。

単身で初の海外出張に。 初の海外でかつ一人だったので、無事生きて帰れるか不安ではあったけれど、本当に良い経験だった。

4月

海外出張の勢いもあり、ninjavaやTLUGに参加してみる。 これはこの後継続出来ていなくて勿体無いなかった。

iPhoneを購入。 これは生活が変わったし、本当に良い決断だった。

型レベルプログラミングの会 このころから頭おかしいイベントが増えてきたような気がする。

5月

『本物のプログラマはHaskellを使う』読者の集い

Pure Prolog Implementation...なんか (PPIM) Prolog実装Hackason

6月

数学基礎論の考え方・学び方。 田中一之先生に初めて会った。

数学基礎論を巡るつぶやき

ICFP Programming Contest 2009 に参加。これは毎年参加したい。

7月

Shibuya.lisp テクニカルトーク#3 に参加。 そこで知り合ったJohn Fremlinさんとはその後何度かメシを食いに行くなどした。

日本Ruby会議2009に参加

Project Euler に参加開始。 途中からはなかなか解けなくなってしまったけど、最初は毎日解いていた。

8月

夏らしく、花火を見に行ったり、ぼんぼり祭りに行ったり。

数学基礎論サマースクール 2009 に参加。Twitterでの実況に挑戦してみた。

GabaでLevel 6のLPAを受けた。

LLTVに参加。

FLTVでAlloyについて紹介する発表をした。

9月

Google Code Jam 2009 にエントリーし損なう。 エントリーしててもそんなに上には行けなかっただろうけど、こういうのには積極的に挑戦したかった。

池上さん主催の、Haskell Annual Meeting Autumn.jp 2009 (Hama.jp 2009) で、Categorical Programming の紹介をした。

PLDIの論文を読むPLDIrに、PLDIr#2から参加し始める。

10月

内輪の人狼で久しぶりに人狼をやった。

計算機言語で定理証明 (Proof Party.JP)というイベントに参加。

数学基礎論講演会 「ゲーデルの不完全性定理」に参加。 田中先生の講演第二弾。

11月

山本さんの翻訳した『プログラミングHaskell』 が出版。 読書会という以外で翻訳のレビューに参加させて頂いていたのは初めてで、良い経験になった。

コナミスポーツクラブに会員登録。時々行きだす。 ついでに、勧誘に負けてスキューバダイビングにも手を出す。

Haskellナイトの Lightning Talk “Haskell Gong”で『自然言語をラムダ式で解釈する体系PTQのHaskell実装』という発表をする。

True Intensionality in Higher Order Logic に参加。

ORFに初参加。

祖父が亡くなり葬儀を行った。

12月

Haskell 2009年末の集い(忘年会前哨戦) で、Haskell 2010 に入ることになった RelaxedDependencyAnalysis について簡単に紹介した。

スキューバダイビングの海洋実習に参加し、オープンウォーター・ダイバー・コース修了。

まとめ

こうして振り返ってみると色々やってはいるなぁ。 あまりハック出来ていないことや、あまり本を読んでいない点とかは気になるなので、その辺りはなんとかしたいが、いい傾向だとは思う。 また、持続したこととしては、腹筋とsmart.fmをほぼ毎日続けられたのと、英会話に定期的に通い続けたこと、途中から随分減ってしまったけど定期的に泳ぎにいけたのと、Project Euler を解き続けたこと、辺りは良かったな。