日々の流転

λ. 1+1=2って本当?

久野君に会ったので、昨日から疑問だったこの文章の事を聞いてみたが、どうも要を得ない。ちなみに、僕が思っていたのは以下のような事。

λ. 「+」という記号の意味するのは、加群をなすとかcoproductになる等といった適当な形式的性質をその体系で満たすバイナリオペレータであるという事に過ぎないように思える。

λ. つまり、集合の直和とベクトルの加算が共に「+」で表記されるからといって、これらは単にたまたま「+」という記号で表すのに都合の良い性質を両者が持っていたから「+」という記号で表記されているだけで、それ以上の意味を「+」に求めるのは、数学的に意味のあることとは思えない。

λ. 仮にそれ以上の意味を考えて「+」が複数の意味が混用されていると考えても、それらは言わば ad-hoc polymorphism に過ぎないわけで、意味に応じて関数名を変更してやれば(機能を損なわずに)「混用」は解消できるのでは?

λ. 睡眠不足。

λ. Squeak

豊田さんが使っているのを見て面白そうだったので試してみる。なかなか楽しい。

λ. 研究室

慶應の他のキャンパスの事は知りませんが、SFCに限っていえば学年の制限は一応無いので、B1から研究室に入っている変な人もいますよん(あるいは大学に入る前から研究室に入り浸っているもっと変な人とかも)。でも、研究室に入らなくても、卒論を書かなくても卒業できるんで、そういう意味では全然すごくないですよー

λ. ファイルのロック

Cygwinのファイルロック関係って何だか微妙ですよね。今GConfのファイルロックに悩まされていたり。

λ. 読書

『さくらの唄』

安達 哲 [著]

λ. Announce: 圏論勉強会(第六回) は延期

会場が使用できなくなり、参加者も少数なので、今週末の勉強会は延期になったそうです。延期先はゴールデンウィークらしいのだけど、どうなることやら……

λ. Randomly Generated Paper Accepted to Conference

addieに教えてもらった。ウヒヒ

λ. Programming with Static Invariants in Ωmega - Nathan Linger and Tim Sheard

Ωmega の話。

Obligations と Assumptions による型チェックは "Wobbly types: type inference for generalised algebraic data types" のものよりも随分単純に見える……

不変量(invariant)を表現する方法としての、GADT と Nested types (non-regular types) の関係はどう考えるべきだろうか。

λ. RHG読書会::東京 Revolution::ふつうのLinuxプログラミング 第八回

RHGは Ruby・Haskell・Gauche の略だそうです。

λ. length xs + length ys = length (xs ++ ys) の証明

RHG読書会の飲み会で即興で書いた証明。

--#include "Hedberg/SET.alfa"
--#include "Hedberg/Op/Nat.alfa"
open SET use Id, refId, mapId, Nat
open OpNat use zero, succ, (+)

(++) (|X::Set) (xs::List X) (ys::List X) :: List X
  = case xs of 
    (Nil    )-> ys
    (x : xs')-> x : (xs' ++ ys)

length (|X::Set) (xs::List X) :: Nat
  = case xs of 
    (Nil    )-> zero
    (x : xs')-> succ (length xs')

prop (|X::Set) (xs::List X) (ys::List X)
  :: Id (length xs + length ys) (length (xs ++ ys))
  = case xs of 
    (Nil    )-> refId (length ys)
    (x : xs')-> mapId succ (prop xs' ys)

λ. Trampolined Style by Steven E. Ganz, Daniel P. Friedman and Mitchell Wand

• <URL:http://www.cs.indiana.edu/~sganz/publications/icfp99/paper.pdf>
• <URL:http://citeseer.ist.psu.edu/ganz99trampolined.html>

昨日のRHG読書会のjsthreadの話に出てきていたので、読んでみた。 control operator 系(?)の話は苦手で、読んでもあまり分かった気がしない。

Trampolined style で書かれた階乗のコードは以下。 基本的には末尾呼び出しの形式で、末尾で値を返す部分をreturn関数を介するように、末尾呼び出し部分をbounce関数を介するようにしてある。

(define fact-acc
  (lambda (n acc)
    (if (zero? n)
        (return acc)
        (bounce
         (lambda ()
           (fact-acc
            (sub1 n)
            (* acc n)))))))

(後で書くかも)

モナド等と違って T, return, bounce の満たすべき代数法則が与えられていないのが、何だか不思議。

λ. 風邪気味

先週の疲れが出たのか、体調が悪い。 今日は携帯の機種変更をしに行こうと思っていたが、ゆっくり休むことにする。

λ. 研究室ページがリニューアル

萩野・服部研のトップページがリニューアルされていた。 何かかっこいいぞ。 SilverStripeかぁ。

ちなみに、このスクリーンショットの撮影にはFireShotを使用。

λ. 萩野・服部研の新歓

萩野・服部研の新歓に参加してきた。

λ. Ruby とプロセス: spawn について

akrさんのspawnの話を聴きにいった。 Ruby関係の参加者が沢山いるだろうと予想して行ったら、参加者はすごく少なかった。勿体無いなぁ。 私の知識は、想定される聴衆 level 2 「fork と exec なら大学で習った (shell を作る実習とか)」程度なので、「ほえー」という感じだったが、面白かった。

• 天泣記 (2009-04-15)

以下はメモ。

• Rubyのプロセス起動のAPIは、帯に短しタスキに長し、というか短いものしかない。
• fork/exec
  • 当時のシステムコールのデザイン。カーネルはアトミックなものを提供し、複雑なものはライブラリが提供する。
• ruby 1.9 のタイマースレッド
  • スレッドの切り替え
  • シグナルはタイマースレッドが受ける
• spawnで十分なのか?
  • コマンド実行にforkを使わなくていいじゃん、というのが今回の話。fork後execしないようなものはまた別の話。
• 最終的なFDのマッピングを実現するために、一時的なFDが必要になる事があるので、FDの空きが足らないと動かない。ただ、Rubyは子プロセスでのエラーを通知するためにパイプを使っていて、そういう意味ではもともとダメなので気にしない。「もうだめなんで」「毒を喰らわば皿まで」
• 余計なFDを閉じないとまずいことになる例
  • sortを呼び出してソートを行う場合、sortが(知らずに)書き込み側のFDを持ってると、読み込み側のFDをEOFまで読めない
• popen4, popen5
  • pythonでもpopen5まで提案されたが、さすがにsubprocessという名前になった。
• systemの実行中にinterruptを受けたら、子プロセスが死ぬだけで親は死なない
• いつも使っているようなものでも、abstractionを変えるべきという一つの例
• Windowsの実装はCreateProcessでうまくいくかと思ったら、親プロセスの属性を一時的にちょっと変えた状態でCreateProcessして、親プロセスを戻すという風になっている。
• 親で属性を変えたときに安全に復帰できるか?
  • 例えばカレントディレクトリに戻れるか? (fchdirがあれば安全に戻れる)
  • 「race condition だから、バレなければOK」
• 設定可能な属性は実は取捨選択してる。uid, gid周りは意図して避けた。特権のところはruby使うな。あと、シグナルのマスクとか。
• 子プロセス側での属性設定、Windowsでも止まった状態で起動して、スレッドを注入して...とかやると出来る。
• Windows ではFDは3番目以降は継承されない。カーネルオブジェクトは継承できるが、カーネルオブジェクトからFDへの対応が継承できない。前述のテクニックで、無理やり初期化すれば出来るらしい。しかし、WindowsにはFDを外から受け取るようなコマンド(e.g. valgrind)はそもそも無いので継承しても無意味。
• 色々なプラットフォーム
  • MacOS : 複数のスレッドが動いているとexecがENOTSUPで失敗する。
  • FreeBSD 7 : スレッドを使っていると、forkだかexecだかが動からないらしい。
  • NetBSD 4 : fork したプロセスでスレッドが動かない。n:m のスレッド管理情報がメモリマップで管理されていて、共有されてまずいらしいとか。
  • NetBSD 5 : 動くらしい。
  • 動かないっていってくれる方がありがたいのでは?
• 想定している前提
  • fork → exec ではどのOSでもサポートするであろう。
  • マルチスレッドの時にfork出来るか? さすがにシステム関数は使いたいから、動くだろう。
  • spawnはそこに毛が生えた程度をサポート
• setenvはasyncsafeではないので、環境変数の設定は本当は親でやる必要があるかも。