まだHaskellをはじめて間もないころ、「bindの度に何かするモナド」を考えた。例えば、 action = do putStrLn "one." putStrLn "two." putStrLn "three." というコードを実行すると one Hello! two Hello! threeと出力するような。応用すれば、「定期的に yi…
Firefoxにおいて、HTML5のアプリケーションキャッシュ(オフラインキャッシュ)をクリアするには、メニューの環境設定→詳細→ネットワークを開き、「今すぐ消去」をクリックする。しかしHTML5アプリの開発で毎回この画面を開くのは面倒である。この操作をショー…
(追記：アドオンを作った。) HTML5 には オフラインでwebアプリケーションを動作させるためにファイルをキャッシュする手段が指定されている． cache manifest というファイル に，「どのファイルをキャッシュするか」を記述しておき、htmlタグの manifest …
追記：「東京Node学園#1「非同期プログラミングの改善」のエッセンス」というスライドで、似たようなテクニックが使われているのを見た(p.32-)。 そんなにスジは悪くないのかもしれない。 JavaScriptでは非同期的に関数を呼ぶことが多い。例えばimgタグのロ…
名古屋でのOCaml meeting 2010が近いけれど、何かと忙しくて内容にcontributeできそうにない…。OCamlJSを使って何かやるつもりだったけど間に合わない…。 などといいつつ、気分転換にJavaScriptをポチポチ書いた。
今日は関数型言語の型で副作用(入出力)の制約を表現する、というお話を書きます。 (勢いで書いたので、わかりやすいかどうか不明です。) Safeio in OCaml ガリグ先生による Caml-list への投稿に Safeio というお話があります。 任意個のチャネルへの入出力…
multi-promptな限定継続の方が型がわかりやすい件について。なんだかshift/resetの型付けはむつかしいなーと思っていた。 限定継続のOCaml実装を見てみたくて、Olegさんのdelimccライブラリとその論文を眺めていた。 こちらはmulti-promptな限定継続といい、…
前回の例はちょっと意味不明だった。単にshiftをmap関数に渡してみたかったのだけど…もっとわかりやすく、shift/reset を使って map 関数をひっくり返したものを作ってみた。 が、やっぱりモナドなので普通のSchemeの例より読みにくいような気もする。まあし…
この記事の続きはこちら三次会では Olegさんによる限定継続モナド を触っていた。 これまで皆が使っているのを指をくわえて見ていたけど、自分でもやっと使いこなせるようになってきた気がする。うれしくなったのでこの記事を書く。説明では疑似Haskellっぽ…
第三回ProofCafeが開催されました。CPDTの Inductive Types の前半を読みました。個人的には injective タクティックを使ったことがなかったので次から積極的に使おうと思いました。
ProofCafe の第二回が名古屋・栄の「どえりゃあ」で開催されました。 前回の記事はこちら 私は今回は出席できず。残念です。 資料とか http://coq.g.hatena.ne.jp/yoshihiro503/20100517/p1 より転載。 資料(HTML): http://adam.chlipala.net/cpdt/html/toc.…
いきなり何を言い出すのかと思われるかもしれないが、最近はCやJavaのソースコードを解析してカバレッジテストを自動化する方法を調べている。 私、この分野に関しては全くの素人なので、何か知っている人はぜひコメント欄や twitter (@keigoi) で教えて欲し…
名古屋・栄のお洒落レストラン「どえりゃあ」で、第一回 ProofCafe が開催されました。 ProofCafe は、コンピュータプログラムの安全性に関する定理証明に興味を持つ方々の集いです。 記念すべき 第一回目は Coqという定理証明支援系について id:yoshihiro50…
下の記事の続き。 hintは意外に私の欲しい機能がなく、たとえば「あるレコード型のフィールド名をすべて取得」みたいなことができない。Template Haskell の reify 関数なら、任意の識別子について reify が使えるののに… というわけで、 ややアクロバティッ…
GHC API のラッパー hint を使えばHaskellでも手軽にリフレクションっぽいことができる。例えば動的にHaskellのソースをロードして関数を呼び出す、といったことが数行で書ける。 ところでリフレクション周りで色々やろうとすると、すぐに関数の型を解析した…
参考：http://d.hatena.ne.jp/yoshihiro503/20100119#p1証明すげー。 あと、幅優先探索で見つけたパスを無限ストリームで並べているのを見てこれは面白いと思った。枝刈り付きBFSとゴールの発見手続きを独立に書けているのか。なるほど！ ストリームを使った…
無限ストリームの型はCoInductiveという構文で宣言された余帰納的な型である。 無限ストリームはCoFixpointという余帰納的な関数(?)を作る構文で定義する。Fixpointは最小不動点(Coqなら「いつか必ず止まる」)だがCoFixpointは最大不動点(止まらない、無限?)…
Windows Server 2003 を使っているのですが、 ドメインメンバーだからか コントロールパネルの「日付と時刻」では NTPクライアントのタブがなく、GUIで設定できなくなっていました。 次のコマンドラインで、NTPクライアントを設定しました： w32tm /config /…
fixタクティックについて。 ふつう、Coqの証明モードで構造帰納法を回したい場合は inductionタクティックを使いますが、 fix は、帰納法のためのよりプリミティブなタクティックのようです(項の場合分けをやらない)． This tactic is a primitive tactic to…
下の記事では， Definition dual_dec : forall (u1:sesstyp) (u2:sesstyp), {dual u1 u2}+{~dual u1 u2}. という関数を，Coqの証明モードで作りました．ところが証明モードで作ったプログラムは極めて複雑でイマイチ効率のほどがよくわかりません (Coqで Pri…
すごくどうでもいい証明です．．Coqを触るのは2年ぶりくらいだろうか… めちゃくちゃ非効率なことをやっていそうなので，皆さんのツッコミをお待ちしています． 前提 セッション型の双対とは，受信の双対が送信，送信の双対が受信という感じで決まっています…
full-sessionsの新バージョン 0.6.1 を HackageDBにアップロード しました。 full-sessions は、Haskellにおけるマルチスレッド/ネットワークプログラミングのライブラリです。 Sessionモナドという新しいモナドを使ってプログラムを書きます。 チャネルの型…
TAPLのiso-recursive type の説明でfoldとunfoldというのが出てきたけど、それっぽいことをする。 単に再帰型っぽく展開したりたたんだりできるだけで、実際に再帰型を作っているわけではない。 -- 再帰させたい型 data A x = A x deriving Show data B x = …
昨日の記事に関連するのだけど、 fundeps と type families で一見 同じように見えるが 微妙に異なる挙動を見つけた。ずいぶん込み入った例だけれど、さしあたりの理解のためにこの記事を書く。 ストーリー 例のごとく、私は full-sessionsにおいて 繰り返し…
忘れた頃に full-sessions の開発をやっている。 これまでセッション型の再帰を扱いづらかったので、もっとイージーに使えるようにした。unwind という関数で、再帰の開始点を表すことにした*1。 例えば、 {-# LANGUAGE NoMonomorphismRestriction #-} impor…
full abstraction ... λ計算とかπ計算とか表示的意味論のお話ではよく出てくる概念なんですが、未だによくわからないなーとつぶやいていたら id:sumii さんに教えていただいた。 もったいないのでここに残しておきます。 full abstraction の私的な説明 計算…
東京には PLDIの論文を読む PLDIr という会があるらしい。 ちくしょー楽しそう！ http://blog.deadbeaf.org/2009/08/22/pldir/ http://www.tom.sfc.keio.ac.jp/~sakai/d/?date=20090930#p01さておき、似たようなことを名古屋でやるとしたら誰か乗り気な人は…
Hibernateはパフォーマンス向上のため遅延初期化の機能をもっています。 が、必ず アクセスされるオブジェクトについては遅延初期化は不要です。 .hbm.xml では 該当するクラスやプロパティに lazy="false" と書きます。一方 hibernate-annotationsでは, @Pr…
pthread のスケジューリングがイマイチ公平でないように見えたので各環境での振る舞いについてざっと調べた． (あんまりOCamlと関係ない) 動機 前回のコードは 私の環境(MacOSX 10.5.8)では コンテキストスイッチがなかなか起こらず しばらく片方のスレッド…
マルチスレッドでOCamlからCを呼ぶ場合、または CからOCamlにコールバックする場合、 C側からOCaml のデータを触るとき C側からOCaml のコードを呼ぶとき は、その部分を (OCamlを触らないコード) leave_blocking_section(); (OCamlを触るコード) enter_bloc…
