下の記事では， 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…

OCamlのコンテキストスイッチのタイミングを調べた。OCaml では OSネイティブのスレッド (pthread) を使える。 しかし、OCamlのランタイム内で同時に走るネイティブスレッドは1本だけ、という制限がある。OCamlはスレッドセーフなGCを備えていないためだ。 …

最新版はこちら (2010/12/8)OCaml を Android に移植しました。具体的には OCaml のバイトコードを Android で実行できるようになった OCaml のソースから Androidのネイティブコードを生成できるようになった という感じです。 caml-listにもポストしたよ。…

某Webアプリに飽きたのでさくっとお気に入りのデモを作ってみた。 たぶんこれ以上は作らない。 動画 ソース http://sites.google.com/site/koyamakannon/Home/android-plasma.zip

apply (undefined :: n -> Succ (Succ n)) Zero :: Succ (Succ Zero) 型レベルのλ (System FのΛ)があったらいいのにーという風に理解したのですがそりゃ難しそうに思えます． 難しくありませんでした．何かそれっぽいのができました．知りもしないのに適当な…

MacPorts から F# を入れて触ってみました． インストール sudo port install fsharp インタプリタの起動 fsi しばらく待つと mono がむっくりと起き上がって，プロンプトがでます。 もし起動しない場合は, bashrc に export DYLD_FALLBACK_LIBRARY_PATH=/us…

id:eagletmt さんが Haskell の型レをやっているのでコメントをポチポチ書いています ただ，これだとちょっと残念なことがあって，例えば2つ足す場合， data Succ2F = Succ2F instance Apply Succ2F x (Succ (Succ x)) と，わざわざ書かなければならない． …

ピンチヒッターとしてLTではなく普通のセッションをいただきました！ スライドは以下： http://www.agusa.i.is.nagoya-u.ac.jp/person/sydney/ocaml/ocsigen-omt2009-black.pdf# slideshareがこのスライドを受けとってくれません

明日の OCaml Meeting Tokyo 2009 で Eliom/Ocsigen について LTします！ これに備えて、 Eliom と PG'OCaml を使ったサンプルアプリを準備しました！ Eliom は OCaml 用の Webプログラミングのライブラリです。 Ocsigen上で動作します。 OCaml の静的型付け…

Camlp4: Uncaught exception: DynLoader.Error ("/opt/local/lib/ocaml/site-lib/pcre/pcre.cma", "error loading shared library: dllpcre_stubs.so: dlopen(dllpcre_stubs.so, 138): image not found")と出た。 .bashrc に、 export DYLD_FALLBACK_LIBRARY…

いつも似たようなことをやっているのでいいかげんメモしておく。 (あとで追記するかも) サーバのインストール port install postgresql84 port install postgresql84-server mkdir /opt/local/var/db/postgresql84 chown postgres:postgres /opt/local/var/d…

EliomではXHTMLを表現する型でページを構成する．たとえば、 というタグは型 [>`Html ] XHTML.M.elt の値として扱う． このおかげで、Eliomが出力するXHTMLは必ずwell-formedかつ(ほぼ?)validだ． [>`Html ] XHTML.M.elt という型を見れば分かるように、 幽…

以前 ここで書いた 電子メールアドレスを表現するリクエストパラメータの param_type で let email_string s = Eliom_parameters.regexp emailregex "$0" s と書くと、 なぜか 文字列 "ocsigen" が帰ってくる。 正規表現の $0 はマッチする文字列全体を指す…

Eliomで、とある講義の受講申し込みアプリを作っている。こういうのにありがちだが、リクエストパラメータはすぐに増えてしまう。このパラメータの山はなんとかならないか。 フォームを作る関数 get_form や post_form は、パラメータの個数分ネストされた対…

例えばEliomでextlibを使う場合 <library findlib-package="extlib"/> とする。</library>

よくある話、正規表現でメールアドレスっぽくない文字列を弾きたい． Eliom の, 正規表現で入力値を弾く param_type を生成する Eliom_parameters.regexp を使う OCamlには pcre-ocamlというPCREインタフェースがあるのでそれを使う． ソース (* どこかから…

(Ocsigenは Webサーバーの名前なので フレームワークの名前 Eliom で呼ぶことにした) 昨日の記事で、 入力値バリデーションに失敗して元のページに戻るとテキストが消えてしまう問題 について書いた． 重要な機能が欠けている気がするのだが、こんなことでせ…

2年前に触ったときのソースをここに置いたのだった。 http://tsukimi.agusa.i.is.nagoya-u.ac.jp/~sydney/eliomsample.tar.gz しかしおそらく古すぎて動かないと思う。

Ocsigenで簡単なサンプルを書いた。 簡単すぎて悲しくなるけど、最初はこんなもんだろう。今週でこれをそこそこの規模に成長させる予定です。 足し算アプリ Struts にあるような入力値の検査機能(その業界ではバリデーションといいます)はOcsigenにはないの…

与太話。 Haskell でもお手軽にWebアプリ書きたいんですが、 どうせならいま流行の軽量な感じに書けたら嬉しいのです。そしたら皆にも使ってもらえるよね。 型がうれしいHaskellで軽量にWebアプリが書けたらもう向かう所敵なしだと思う。 アイデア： リクエ…