On merging of two asynchronous queues

This is a personal note on what I implemented for this signature https://github.com/keigoi/ocaml-mpst/blob/master/lib/lwt/mstream.mli. Comments are appreciated, but the followings are not meant to be read by others than myself. ---- Suppos…

制御の逆転 〜 OchaCaml と限定継続でイベンドハンドラをダイレクトスタイルで書く

昔、こういう記事を書いた:OchaCamlで限定継続/answer type modificationを勉強する - keigoiの日記もっと shift/reset で何か身の回りの例を書いてみたい。そこで限定継続を使って、イベントハンドラをコールバックではなくダイレクトスタイルで書けるよう…

OCamlと順序付き線形型で効率のよいXML処理 (to be continued)

この記事は OCaml Advent Calendar 2012 の 24日目の記事です。 が、実際にアップロードしたのは2013年1月18日です。 本当はもっと実用的なネタを書く予定だったのですが、飽きた ので、いっそ思い切り趣味に走った記事を書くことにしました。追記: 動作す…

最強OCamlでセッション型を実現

この記事は OCaml Advent Calendar 2012 の 18日目の記事です。OCamlでセッション型を実装した、というお話です。ちょっと時間がないので簡潔に書いています。 ソースはこちら セッション型 セッション型とは: 通信チャネルの型です プライベートな二者間の…

OCamlで使える同値再帰型 (equi-recursive types) は恐ろしいけど、すごい

この記事は OCaml Advent Calendar 2012 の 17日目の記事です。同値再帰型が何であるか知りたい方は、今後発売される TAPL日本語版を読むと良いと思います(私も翻訳しています。*1)。 Wikipedia英語版にもありますね。 同値再帰型は、再帰型の定式化の方法…

第一級モジュールでジェネリックなSet操作

この記事は OCaml Advent Calendar 2012 の 8日目の記事です。昨日のエントリでは無理矢理 'a t の形で扱える Setモジュールを作りましたが、これには欠点があり、 'a t型をもつ各集合で、'aの同値性の付け方が異なってしまいます。 昨日の記事に @garriguej…

第一級モジュールでSetの多相性を復活させてみよう

この記事は OCaml Advent Calendar 2012 の 7日目の記事です。OCaml 3.12より導入され、4.00でさらに便利になった 第一級モジュール (First-class modules)を使った小技を紹介します。ある種の単相的に定義された抽象データ型(ADT)を多相的にするという技で…

OchaCamlで限定継続/answer type modificationを勉強する

限定継続は面白いのですが、型がつくとイマイチ自分にはよくわからなくなってしまいます…。 何度目かの正直で、 去年の Continuation Workshop 2011 Tutorialで紹介された OchaCaml を使って勉強してみます。 何となくしか限定継続を分かってない自分用メモ…

実務で使うOCaml - 泥臭い仕事をサクっとこなす方法

プログラマが実務で出会うのは、問題が整理されたキレイな仕事ばかりじゃない。プロダクトに本質的じゃない部分でもプログラムを書く必要に迫られる。いわゆる開発方法論では抽象化されてしまう、今ここにいるソフトウェア開発者の悩みだ。今日は、私が仕事…

「すごいHaskellたのしく学ぼう!」は気配りと楽しさがすごい

本書はHaskellの入門書です。とっても親しみやすい内容と文体で、構成についても、順序を踏んで丁寧に書かれているようです。また日本語(マルチバイト文字)の扱いを付録で解説しているのもポイント高いですね。以下、ざっくり目を通して、これは!と思った点…

ConduitとPersistentを使って高パフォーマンスなDB処理を目指す

Iteratee/Enumerator系の話題がHaskell界隈で騒がれて久しい (日本語の紹介記事)。これらはHaskellで細粒度のリソース制御ができるストリーム処理の方法で、例外処理もやりやすい、という触れ込みだった。曰く、ストリーム処理はリソースの消費量の点で(オ…

型クラスで tagless DSL メタプログラミング

これは Haskell Advent Calendar 2011 の5日目の記事です。 去年も書きましたが、その記事はこちら → Haskell厨を6年やってる俺がOCamlを仕事で2ヶ月使ってみた - keigoiの日記先日の記事 Haskell+タグレスな型付きDSLで楽々!C言語コード生成 - keigoiの日…

OCamlコードをCoqで検証できる "CFML" で 証明コンペに挑戦 (未完)

Coq

VSTTE 2012 Software Verification Competition というソフトウェア検証のコンペがあった。参加はオープンで、問題文もPDFで配布されている。 id:yoshihiro503 がチームtebasakiというチームでがんばっていた。僕はCoqに慣れていなかったのでチームに入るの…

最近の話

論文でました EPTCSというオンライン論文集に私の論文が掲載されました。 指導教員の先生との共著になっています。 Session Type Inference in Haskell WOCS9で発表します 第9回クリティカルソフトウェアワークショップ (WOCS9) @ パシフィコ横浜 (11/17木-…

Haskell+タグレスな型付きDSLで楽々!C言語コード生成

関数型プログラミング言語とコード生成 HaskellやOCamlなどはコンパイラなどの言語処理系の実装を得意としている。さすがに日常的にコンパイラを実装している人はそう多くないと思うけど、例えばコード自動生成はすぐ試せる割に効き目が大きく、仕事を効率化…

Alloyでλ計算(完全版)

ついに、Alloy を使って完全な λ計算 (β簡約) を表現できた…。(前回 は中途半端だった。) なかなか面白いのは、Alloy がうまくノードを使って無駄なくβ簡約しているところ(Ω=(λx.xx)(λx.xx) で Ω→Ωなど。後に載せる)。(8/22)フレーム条件のバグを直した…

Alloyでλ計算(β簡約)する

フォロー記事あり前回 (Alloyでλ式をつくる) では、λ式を表現するグラフをAlloyで構築した。 今回は、λ計算の核となるβ簡約の一部をAlloyで記述してみる。 扱えるλ式の制限 面倒だったので、モデルに次の制限を導入した。 このため、正確にはβ簡約とはいいが…

Alloyでλ式をつくる

Alloyでλ式を作ってみた。 フォロー記事あり あまり役に立たない気はするけど、関係の逆(~)を取ったり(反射)推移閉包(*,^)を使う良い練習になった。(バグがみつかり次第、色々修正している。以下のモデル図はソースを修正しながら作っているので、エンバグ…

線形型DSL on Haskell (前回参照) の基本的アイデアと難しい点

前回は、線形型をもつ DSL の例として 線形λ計算を挙げ、実装を示した。 これをもっと押し進めれば、ファイルやネットワーク接続などのリソースの「使い方」をより詳しく指定できる DSL をエンコードできるはずだ (きれいに書けるか、使う人が居るかは別問題…

線形型つきドメイン特化言語 (DSL) を Haskell上に実装する

線形λ計算というのは、「変数をちょうど一度だけ使わなければならない」という線形型をもったλ計算だ。これを Haskell で実装してみた。「ファイルが開かれたら必ず閉じる」という制約のような、線形型 (linear type) が必要な DSL の実装の参考になるかもし…

Coqで分離論理(separation logic)

Coq

分離論理は、ヒープ領域に関する論理結合子をもつ論理体系だ。ホーア論理の拡張であり、ヒープを使うプログラムの仕様を書いたり検証したりといったことに使える。 具体的には、 A ∧ B (AかつB) によく似た、 A ** B という論理結合子が追加されている。これ…

one限量で複数の変数を宣言する

Alloyの言語仕様をゴリゴリ読み進めていた。 非常に勉強になります。Software Abstractions (1st ed., p.288): So although a quantified constraint with multiple declarations may be regarded, for some quantifiers, as a shorthand for nested constra…

OCaml toplevel on Android : マジカルなラクダをAndroidで飼おう

Androidで動作するOCamlインタプリタ OCaml toplevel on Android を Android Market に公開しました。 OCamlのトップレベル(インタプリタ)をAndroid上で操作できます。 enjoy! 仕組み OCamlトップレベルはネイティブ実行されます(OCamlバイトコード+libcamlr…

pa_monad を通して camlp4 のコマンドラインを思い出す

pa_monad は OCamlで モナドを使いやすくするための構文拡張だ. ついこの前 id:camlspotter さんが pa_monad の拡張を書いてくださった.ありがたや. 早速使ってみようと思い,コンパイルした.hg clone https://bitbucket.org/camlspotter/pa_monad_custo…

OCamlベースのAndroidアプリに向けて

O'Caml on Android というパッチを作っている. 柔軟かつ信頼性の高いOCamlでAndroidのアプリを書くのが目標だ. ここ2ヶ月ほどocamljs (OCamlからJavaScriptへのコンパイラ) を使っていて、OCamlの信頼感と柔軟性にとても満足したので,ではAndroidでもOCam…

Haskell厨を6年やってる俺がOCamlを仕事で2ヶ月使ってみた

Haskell Advent Calendar jp 2010のためのエントリです(17日目). 6日目の id:camlspotterさんの 経験15年のOCaml ユーザーが Haskell を仕事で半年使ってみた に対するカウンター(になってるかどうか分からないですが)みたいな感じです. 近くて遠い隣…

モジュールの集約に多相バリアントを使ってみた

OCamlならではの型機能である多相バリアントとプライベート列型を「なんとなく」使ってみた話.タイトルはやや(かなり?)大げさで,小ネタです. 追記: プライベート列型は使わなくて済んだ… ストーリー 仕事でOCamlを使っている. ボスに命ぜられた通り,…

ocamljs を使おう : OCamlからJavaScriptへの変換

ocamljs は OCamlから JavaScript へのトランスレータだ。前回の記事と順番が逆になってしまったけれど今回はocamljsについて書く (基本的に http://jaked.github.com/ocamljs/ 以外のことは書いてないです。)。 JavaScriptは歴史的経緯とその簡潔さからweb…

ocamljsが生成したソースをclosure compilerで圧縮する

ocamljsは OCamlからJavaScriptへのトランスレータ。 closure compilerは JavaScriptのコードを圧縮/最適化するツール。 ocamljsが生成するJavaScriptのソースは大きくなりがちなので、minifier等でできるかぎり小さくできることが望ましい。その点で closur…

ビットとview pattern

小ネタ。 ビットパターンをHaskellでパターンマッチできたらいいよね、ということでview patternを使ってみた。 {-# LANGUAGE ViewPatterns #-} import Data.Bits -- | ビット。 I は 1, O は 0 data B = I | O deriving Show -- | 8ビット。 左がMSB, 右がL…