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

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

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

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

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

まだ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…