はてなブックマーク

この記事は OCaml Advent Calendar 2012 の 24日目の記事です。 が、実際にアップロードしたのは2013年1月18日です。 本当はもっと実用的なネタを書く予定だったのですが、飽きた ので、いっそ思い切り趣味に走った記事を書くことにしました。 追記： 動作するものを github にアップロードしました。 https://github.com/keigoi/olt_ocaml 追記：ちゃんと書きませんでしたが、OCamlによるXML処理ができる実装が既に著者らによって公開されています。 http://www.fos.kuis.kyoto-u.ac.jp/~ksuenaga/x-p/ 順序付き線形型とXML(木) 児玉・末永・小林による この論文 (日本語の文献) は、XMLなどの木構造を再帰的にトラバースするプログラムを、より効率のよいストリーム処理プログラムに変換

この記事は OCaml Advent Calendar 2012 の 17日目の記事です。 同値再帰型が何であるか知りたい方は、今後発売される TAPL日本語版を読むと良いと思います（私も翻訳しています。*1）。 Wikipedia英語版にもありますね。 同値再帰型は、再帰型の定式化の方法のひとつで、「型の再帰構造が外からまる見えな型」といった風情の型です。例えば無限リストは、普通の(同型)再帰型なら type 'a inflist = InfList of 'a * 'a inflist let rec ones = InfList(1, ones) などと、ヴァリアント等を介さないと定義できませんが、 -rectypesオプションで同値再帰型が有効になっている場合、タプルを組み合わせるだけで無限リストを作れます。 let rec ones : int * 'a as 'a = 1, o

この記事は OCaml Advent Calendar 2012 の 18日目の記事です。 OCamlでセッション型を実装した、というお話です。ちょっと時間がないので簡潔に書いています。 ソースはこちら セッション型 セッション型とは: 通信チャネルの型です プライベートな二者間のメッセージ送受信が整合していることを保証してくれます。(定義によっては多者間) 例えば let thread1 () = send c "Hello"; send c 123 という関数は文字列と整数をチャネルcに送るが (send c vはチャネルcに値vを送るプリミティブとする。以下同様)、 let thread2_bad () = let i = recv c in let j = recv c in print_int (i+j) は整数を２つチャネルcで受けるため(recv cはcで受信した値を返す)、

プログラマが実務で出会うのは、問題が整理されたキレイな仕事ばかりじゃない。プロダクトに本質的じゃない部分でもプログラムを書く必要に迫られる。いわゆる開発方法論では抽象化されてしまう、今ここにいるソフトウェア開発者の悩みだ。 今日は、私が仕事で書いたOCamlのコードを晒して、如何にOCamlがプログラマの仕事の道具として優れているかを主張したい。泥臭く、関数的でない、エレガントさのかけらもない、生活臭のあるコードだ。勤務先はOCamlをメイン言語として使っている。研究所とかではなく普通に受託開発を生業としている会社だ。OCamlは理論一辺倒で、マニア向けで、現実のソフトウェア開発には使えない、という誤解が万が一あるかもしれないが、全くそんなことはない。 (Haskellもそうだけど、それはまたの機会に) いかにOCamlが優れているかについての概論めいた話は、OCamlを数十人体制で10年

本書はHaskellの入門書です。とっても親しみやすい内容と文体で、構成についても、順序を踏んで丁寧に書かれているようです。また日本語(マルチバイト文字)の扱いを付録で解説しているのもポイント高いですね。 以下、ざっくり目を通して、これは！と思った点をまとめました。 イントロはHaskellの概要をやさしい文体で、でもしっかり説明しています。 Haskellがもつ純粋さと参照透明性の重要さ、必要最小限の計算を行う遅延評価であること。型付けが重要なのは当然として、型推論がすばらしいこと。さいごに「Haskellはエレガントで簡潔です」。 全体として：気配り 翻訳が読みやすいです！親しみやすさが日本語になってグッと増した感があります。翻訳文であることを全く感じさせません。 また随所で、著者の気配りを感じさせられます。 文中の補足説明やNOTEが親切です。たとえば、初見ではワケわからない型の周り

Iteratee/Enumerator系の話題がHaskell界隈で騒がれて久しい (日本語の紹介記事)。これらはHaskellで細粒度のリソース制御ができるストリーム処理の方法で、例外処理もやりやすい、という触れ込みだった。曰く、ストリーム処理はリソースの消費量の点で（オンメモリに全てを置くよりも）優れているが、hGetContents::IO Handle->Stringのような遅延IOはファイルのクローズなどリソースの制御が難しい。それを改良したのがIteratee/Enumerator系のライブラリだそうだ。 Conduit iteratee/enumeratorの改良を試みているのが Conduit （コンディット？）だ（日本語の紹介記事）。 最近でもずっと改良がつづいているようで(参考：tanakhさんの発表資料)、例えばSource/Conduit/Sinkの型がPipeに統

これは Haskell Advent Calendar 2011 の5日目の記事です。 去年も書きましたが、その記事はこちら → Haskell厨を6年やってる俺がOCamlを仕事で2ヶ月使ってみた - keigoiの日記 先日の記事 Haskell＋タグレスな型付きDSLで楽々！C言語コード生成 - keigoiの日記 をちょっとブラッシュアップした。前回はコードについては全く説明しなかったので、改めて解説する。 おさらい HaskellやOCamlなどの関数型言語は、プログラミング言語の処理 ― 構文解析とコード生成 ― がとても得意だ。 大手のソフトウェア企業として知られる NTTデータも既存コードの処理 (構文解析〜リバースエンジニアリング) のために Haskell を使っているそうだ。 (函数プログラミングの集い2011より。インドに外注する部分もあるそう togetter 1

VSTTE 2012 Software Verification Competition というソフトウェア検証のコンペがあった。参加はオープンで、問題文もPDFで配布されている。 id:yoshihiro503 がチームtebasakiというチームでがんばっていた。僕はCoqに慣れていなかったのでチームに入るのは見送った（というかチームの人数上限4人で入れなかった）。 仕事や出張の片手間でやっていたので、結局一問も検証できなかったけど、楽しかった。 検証にはCFMLというツールを勉強しながら使った。 これを使えば OCaml のソースコードを Coq で検証できる。 それも ref型による破壊的代入つきの手続き的なOCamlを含む。 そして Coqと違い、プログラムは停止しなくてもいい。 つまり、CFMLを使えば、 手続き型プログラムを、ホーア論理+分離論理(のようなもの;後述)を使って

関数型プログラミング言語とコード生成 HaskellやOCamlなどはコンパイラなどの言語処理系の実装を得意としている。さすがに日常的にコンパイラを実装している人はそう多くないと思うけど、例えばコード自動生成はすぐ試せる割に効き目が大きく、仕事を効率化する方法としてぜひ試してみたい選択肢だ。 今回は、Haskellの言語内DSLからC言語のコードを生成する方法（の一つ）を簡単に紹介する。 この方法で、Haskell上のEDSLを使って (1) C言語のソースコードを生成でき、 (2) Haskellの式として評価できる。 このように、わざわざパーサを書かなくても、コンビネータを適当に作ればすぐにDSLを作ってしまえるのも、関数型言語の魅力かもしれない。 taglessな方法 ただし、ちょっと他と違う方法を試す。 OlegさんのサイトにTyped Tagless Interpretation

線形λ計算というのは、「変数をちょうど一度だけ使わなければならない」という線形型をもったλ計算だ。これを Haskell で実装してみた。「ファイルが開かれたら必ず閉じる」という制約のような、線形型 (linear type) が必要な DSL の実装の参考になるかもしれない。 線形λ計算の実装は、既に Olegさんがやっている。それは変数参照をde Bruijn indexを使って書くようになっている。 一方、この実装は、よりHaskellに近い記法で書けるようになっている。 使用例 λ抽象の前に lam, 関数適用の前に app, 変数参照の前に var が必要である以外は Haskell と同じ記法で書ける。 Linear Lambda Calculus の頭文字をとって LLC モナドという名前にしてある。 LLCモナドの型は LLC t ii jj a となっていて、 t 型のタ

分離論理は、ヒープ領域に関する論理結合子をもつ論理体系だ。ホーア論理の拡張であり、ヒープを使うプログラムの仕様を書いたり検証したりといったことに使える。 具体的には、 A ∧ B (AかつB) によく似た、 A ** B という論理結合子が追加されている。これは Aで言及しているポインタと、 Bで言及しているポインタが指しているヒープ領域が、分離されている(≒エイリアシングがない)ことをいっている。 Affeldtさんが、Coqで分離論理を書いて、しかもそれを公開してくださっている。 http://staff.aist.go.jp/reynald.affeldt/seplog/ C言語で書かれたOSのヒープマネージャや、SmartMIPSのアセンブラで書かれた暗号プリミティブの検証をCoqでやっている。 こういったことを自分でも触れるようになりたいので、ICFEM2006のソースを写経して

Androidで動作するOCamlインタプリタ OCaml toplevel on Android を Android Market に公開しました。 OCamlのトップレベル(インタプリタ)をAndroid上で操作できます。 enjoy! 仕組み OCamlトップレベルはネイティブ実行されます(OCamlバイトコード+libcamlrun.a)が、AndroidのアプリはJava VM(dalvikvm)上で動作するため、両者のブリッジが必要でした。 いくつかの方法があり、一部は先日書きましたが、今回の OCaml toplevel on Androidはこのなかのどれでもない、最もイージーな方法を使っています…。 それは 「あるスレッドでocamlトップレベルをバイトコード実行し、標準入出力を介してAndroidアプリのメインスレッドと通信する」という方法です。 stdoutを入力とし

pa_monad は OCamlで モナドを使いやすくするための構文拡張だ． ついこの前 id:camlspotter さんが pa_monad の拡張を書いてくださった．ありがたや． 早速使ってみようと思い，コンパイルした．hg clone https://bitbucket.org/camlspotter/pa_monad_custom でダウンロードしたあとは make一発です． ただ，ちょっと ocamlc から試そうと思ったら，俺 camlp4 のコマンドラインオプションを全然覚えてないよ，ということに気づいた． いつも忘れるので書いておく． ocamlc -pp 'camlp4of pa_monad.cmo' a.ml ocamlc/ocamloptのオプション -pp に続けてプリプロセッサのコマンドラインを書く． しかしそもそも camlp4of とはなんだろう？ caml

O'Caml on Android というパッチを作っている． 柔軟かつ信頼性の高いOCamlでAndroidのアプリを書くのが目標だ． ここ2ヶ月ほどocamljs (OCamlからJavaScriptへのコンパイラ) を使っていて、OCamlの信頼感と柔軟性にとても満足したので，ではAndroidでもOCamlだ、とばかりに開発を再開している． iPhoneやiPadのObjective-Cと違い，AndroidではJavaの型の扱いやJVMとの相互作用が必要でありなかなか厄介だ． しかしiPhoneではいくつかの開発 事例もあるのでAndroidでもそれなりに有効ではないかと信じている．がんばりたい． OCamlを使う利点 もはや自分の中では言い古した感があるのだけど，念のため列挙してみる． 信頼性 OCamlには null値がない．このため NullPointerException

Haskell Advent Calendar jp 2010のためのエントリです（17日目）． 6日目の id:camlspotterさんの 経験15年のOCaml ユーザーが Haskell を仕事で半年使ってみた に対するカウンター（になってるかどうか分からないですが）みたいな感じです． 近くて遠い隣人：HaskellとOCaml OCamlはHaskellと違って副作用があり，更にHM型推論をもつためプログラマは本質的な部分の記述に注力しつつ，コードのチューニングもできる． つまり働くHaskellプログラマがシリアスなソフトウェアを書く時に使えるほとんど唯一の選択肢だ．しかし，同じ静的型付けの関数型言語でありながら，OCamlとHaskellの見た目はかなり異なる． この記事では， HaskellプログラマがOCamlを使い始めると，どういうトラップにハマるかを書く． なかでも，

Language.CはHaskell用の、C言語のソースコードを構文解析するライブラリである。 Language.CはパーザとともにC言語の構文木に相当するデータ型を提供しており、C言語のソースコードをHaskellのデータとして操作可能である。このため、Language.CはC言語のコードを色々と解析・変換するのに便利である。さらに意味解析に役立ついくつかの補助関数も定義されている。 組込みソフトウェアに関する研究で必要になったため、Language.C を用いてC言語のソースコードを変換する簡単なプログラムを書いた。 動機 JHC (Haskellのコンパイラ；ISO C互換のコードを吐く)は Haskellのソースから C99のコードを生成する ツール(ARMバイナリを生成するコンパイラ)の制約でgcc 2.95(19991024)しか手元にない。 gcc 2.95はC89しか受け付

(追記：アドオンを作った。) HTML5 には オフラインでwebアプリケーションを動作させるためにファイルをキャッシュする手段が指定されている． cache manifest というファイル に，「どのファイルをキャッシュするか」を記述しておき、htmlタグの manifest 属性で指定する． 例： test.manifest CACHE MANIFEST test.html a.jpeg b.jpeg ...test.html <html manifest='test.manifest'> ... このように書いておけば インターネット接続が無い環境でも test.html が閲覧できるようになり，たとえば接続が途切れやすいモバイル環境でもハッピーになれるというわけだ． オフラインキャッシュを使ったwebアプリケーションのサンプルが hacks.mozilla.orgで公開されている

追記：「東京Node学園#1「非同期プログラミングの改善」のエッセンス」というスライドで、似たようなテクニックが使われているのを見た(p.32-)。 そんなにスジは悪くないのかもしれない。 JavaScriptでは非同期的に関数を呼ぶことが多い。例えばimgタグのロードが終わったら次にAを処理して、それが終わったらBをして…など。 こういうときCPS形式でプログラムを書くはめになる。 func1(arg1, function(res1){ func2(arg2, function(arg3, res2){..})}) かようにJavaScriptでは関数リテラルがすこぶる扱いづらい -- 'function' とか 'return' とか {} のネストとか…あとカリー化するにも一苦労 -- JavaScriptプログラマはどう書くんだろう？ こういう非同期呼び出しをうまく同期的に記述する

今日は関数型言語の型で副作用(入出力)の制約を表現する、というお話を書きます。 (勢いで書いたので、わかりやすいかどうか不明です。) Safeio in OCaml ガリグ先生による Caml-list への投稿に Safeio というお話があります。 任意個のチャネルへの入出力に関して、 開かれたチャネルは必ず閉じられる 入力専用で開いたチャネルには入力しかできない 出力専用で開いたチャネルには出力しかできない このような制限をOCamlの型で表現できるんですよ、というお話です。すごいですね。 Haskellで同じようなことをやっているネタとして、セッション型をHaskellで実装するお話があります。が、複数のチャネルを扱うために、どれも型クラスにヘビーに依存していたり(私やMatthew Sackmanの実装)、型クラスを使わない実装では複数のチャネルを管理するためにswapとかpop

multi-promptな限定継続の方が型がわかりやすい件について。 なんだかshift/resetの型付けはむつかしいなーと思っていた。 限定継続のOCaml実装を見てみたくて、Olegさんのdelimccライブラリとその論文を眺めていた。 こちらはmulti-promptな限定継続といい、複数の限定継続を同時に扱える体系の実装なのだけど、こちらの方が型が分かりやすかった。 理論的基礎はDybvig, Peyton Jones, Sabryの論文で、cc-delcontというHaskell版の実装がHackageにある。この実装も indexed monad ではなく普通のモナドなので型は理解しやすいはず。 これらのライブラリでは、 newPrompt, pushPrompt, withSubCont, pushSubCont の 4つのプリミティブを使う。また扱うデータ型も、「プロンプ

この記事の続きはこちら 三次会では Olegさんによる限定継続モナド を触っていた。 これまで皆が使っているのを指をくわえて見ていたけど、自分でもやっと使いこなせるようになってきた気がする。うれしくなったのでこの記事を書く。 説明では疑似Haskellっぽい構文を使う。実際にOlegの限定継続モナドを使う場合はそれっぽく型を合わせる必要がある。 私の限定継続の理解 私の shift と reset はこういう理解： reset e 内側(引き数)にshiftが無ければ、中身(e)をそのまま返す shiftがあれば、shiftによる大域脱出の効果をそこまでに限定する (つまりこの時点での継続を「捕まえておく」) shift f 限定継続kを取り出して、f k を計算し、その値で reset まで大域脱出する (つまりresetで捕まえていた継続を呼ぶ) このkは、引き数を渡すと shift

GHC API のラッパー hint を使えばHaskellでも手軽にリフレクションっぽいことができる。例えば動的にHaskellのソースをロードして関数を呼び出す、といったことが数行で書ける。 ところでリフレクション周りで色々やろうとすると、すぐに関数の型を解析したくなるのだけど、hint は 型推論の結果を文字列で返すのでHaskell的には使いにくい。情けない話だが、どうやら GHC APIがそうなっているので仕方ないようだ。Haskellのパーサが必要になる。 haskell-src-exts を使えば、Haskellの型をparse できる。 似たようなことをやる方法に template haskellとか haskell-src という標準のアレがあるけれど、いくつかの拡張構文をサポートしていない。その点 haskell-src-exts はほぼすべての GHC拡張をサポートし

超久しぶりに小粒なTIPSを． 使いどころも限られますが… javac の出力するメッセージを，英語 英文にしたい時のTIPS． Windowsでは，環境変数LANGを設定してもダメでした．次のようにします： javac -J-Duser.language=en -J の後に続けて JVMへ渡すオプションを書きます． Locale.getDefault()の返り値を指定するuser.language を指定してやれば，javacのメッセージのロケールも変わるという訳です． 一方．コマンドプロンプトで， en/jp 等でコードページを切り替えてもOK …かと思いきや，jdk1.5 からは普通に日本語メッセージを出力してくれやがります． だから↑の方法を使いましょう．

full-sessionsの新バージョン 0.6.1 を HackageDBにアップロード しました。 full-sessions は、Haskellにおけるマルチスレッド/ネットワークプログラミングのライブラリです。 Sessionモナドという新しいモナドを使ってプログラムを書きます。 チャネルの型表現にπ計算の型理論の一つであるセッション型を採用しています。セッション型のおかげで、チャネルの「使われ方（プロトコル）」がスレッド間で整合していることを実行前の型検査によりチェックできます。これにより、ある種のデッドロックや型の不整合は型検査で排除できるようになります。 さらにHaskellの型推論でセッション型を推論させれば、プログラムがチャネルを意図通りに使っていることを型表現からチェックできます。 full-sessions は、HList等で見られるような型レベルプログラミングのテク

マルチスレッドでOCamlからCを呼ぶ場合、または CからOCamlにコールバックする場合、 C側からOCaml のデータを触るとき C側からOCaml のコードを呼ぶとき は、その部分を (OCamlを触らないコード) leave_blocking_section(); (OCamlを触るコード) enter_blocking_section(); (OCamlを触らないコード) のように配置する*1． 2本目のスレッドがOCaml側にやってきたときは、leave_blocking_sectionでコンテキストスイッチまで待たされることになる。 注意： camlspotterさんの記事 等も参考にすること。 実際にFFIでCのコードに入った直後は他のOCamlスレッドがブロックされているので、enter_blocking_section() して、 fopen などブロックする関数を呼び