2009-01-01から1年間の記事一覧

OcsigenについてLTしました

オープンソースカンファレンス2009 Nagoya で OCaml の Webフレームワーク Ocsigen についてLTしてきました。 中身のあることは殆ど言ってませんがこちらにスライドを置きます:OCaml Webフレームワーク Ocsigen概説 @ OSC2009NagoyaView more documents fro…

Jakarta Commons Codec による Base64符号の末尾に改行が付加される件について

Amazon の Web API (Product Advertising API) が、最近 クエリーに署名を要求するようになったので、Javaで書かれた手元のアプリを修正した。 サンプルが与えられているのでまずはこれをコピペした。 http://docs.amazonwebservices.com/AWSECommerceServic…

Qtでハマったこと

C++

(8/17追記)この記事は間違っているような気がするので真に受けないで下さい。 手元で試しても再現しないし、 ソースを読むと QList::iterator::operator先日、某所のヘルプのため Qt (C++向けのクロスプラットフォームGUIツールキット)でほんの少しだけプロ…

メンテナンス中画面を出す本当に正しい作法?

メンテナンス中画面を出す正しい作法と.htaccessの書き方 | Web担当者Forum を見て設定してみたのだが、この通りにやると、 Apacheのエラーログに <<URL>>: RewriteRule: invalid HTTP response code for flag 'R'と出る。 コメント欄でも指摘されているね。 Rewr</url>…

Mac OS X における Ocsigenのインストール

OcsigenはOCamlのWebアプリケーションフレームワークです。 (2年前に触っていて記事も少し書いたのですが飽きてやめちゃいました。) Webアプリケーションの全てを型安全に構成できる素晴らしいこのフレームワークによる開発環境を Macで準備します。 とりあ…

Haskell+GADTで定理証明 その1: 型レベル自然数の等価性

実は、私のfull-sessionsというセッション型のライブラリは中で unsafeCoerce#を使っているので型安全でない。使ってくれる人にとってそれは心もとないだろうし、そもそもunsafeなんとかは、いけがみさんによればSPJとSimon Marlowしか使ってはいけないこと…

型変数の比較3 - 非等価性は矛盾する

TypeEq による型の非等価性判定は結果として矛盾することがある,というお話.型変数の比較で,引数の型が異なることを表現する関数を作ろうとして次のようなコードを書いたとする: typeEq' x y = type'eq x y :: HFalse ここでGHCのeagerなcontext reducti…

型変数の比較2

http://d.hatena.ne.jp/keigoi/20090709/1247155626 の続き.この話は無駄にUpdateとかの型レを使っていてややこしかったです.ここで紹介したコードを ghciでロードして,次を入力すればわかります: ghci> :t type'eq undefined undefined type'eq undefin…

Text.Printf, もっと安全なprintf

可変長引数のテクニックは普通に Text.Printfで使われてるんですね。 型レ以外ではHaskellをヘビーに触るわけではないので知りませんでした…型安全な printf (引数の過不足や型ミスマッチをチェックできる)については Olegさんの最近のポスト http://okmij.o…

型変数の比較

もっと簡単な例で追記しましたHaskellの型レでは型変数同士の比較ができないぜーというお話をしたんですが、OlegさんのReversing Haskell typechecker: converting from undefined to defined のTypeEqを試したらば、できちゃいました。Haskell型レのバイブ…

Haskell98可変長引数ハックにみる,各処理系のcontext reductionの違い

Olegさんの Generic polyvariadic printf in Haskell98 は、プレーンなHaskell98で可変長引数関数をつくり,printfを実現しています. 関数の型(a->r)は型構築子(->)と型引数a rからなる型 (->) a r なわけで,型クラスのインスタンスでうまいこと回せば、こ…

HackageDB!

full-sessions を hackageDB にアップロードしました!

Sessionモナドの読み方

初回に, Sessionモナドは indexed monad だと説明しましたが具体的にどういう制約が入っているのかをちゃんと説明しませんでした. すべてを一度に説明するのは難しいのですが,とりあえずおおざっぱに説明を試みます 事前条件・事後条件 と プロトコルの差…

セッション型のduality

セッション型の読み方について説明します. セッション型の種類 私のfull-sessionsにおけるセッション型を次のTable 2に示す: セッション型は論文によって表記法が著しく異なるが,多かれ少なかれだいたいここで示した機能(と再帰)がすべてである. Send / …

セッション型の分岐

セッション型を備えた 「型付きErlang」みたいなのがあればいいのになあ、と思うんですが(ある?)、一から型推論やら多相性やらを作り上げるのは面倒でしょうしHaskellやMLよりも便利で安全な型システムなんてあろうはずもないので(ぉぃ)、私たちはHaskellで…

既存の セッション型の実装 on Haskell

セッション型のような型は,関数型言語の型システムでは作れないのが普通だ.しかしながらセッション型の機能の一部を関数型言語で実現しようとする試みはいくつか存在する. つい最近では, Kiselyov, Peyton Jones, Shanの Fun with type functions のよう…

セッション型 on Haskell

セッション型は プロトコルを表現する型で, 15年くらい前から π計算の型理論の1つとして研究されてきました(文献リスト(一部)).並行・分散ソフトウェアの普及を鑑みるに,セッション型のような仕組みは次世代の型安全かつ表現力の高いプログラミングのため…

型レベルプログラミング会議

# トラックバックをバラまいてしまいました m(_ _)m スミマセン…型レベルプログラミング会議 に行ってきました。 帰りの新幹線でこれを書いています。随時更新予定。 私の発表 最後の TCast がメインなのですがそれはソース参照 スライド1とHaskellソース ht…

Logical Relationという名前

sumiiさんの記事によれば,どうも私は [お勉強]とタグをつけたのをいいことにデマを振りまいていたようなので訂正しました.型付きλ計算の型でcharacterizeしてるから論理的,というのなら,正直 Curry-Howard同型による,という説明でもそれほど間違ってな…

ActiveDirectory でユーザ登録する時は LDAP の CN と アカウント名を統一すること

Windows Server の話. 背景 ActiveDirectory は LDAP プロトコルで認証できる. LDAPでは, CN=hogehoge,OU=foobar,... という形(DN)で エントリを一意に指定する. 現象 某F社検疫が通らない 原因 Windows の 「ActiveDirectory ユーザとコンピュータ」か…

論理関係は(型環境について)単調

ATTAPL続き. 論理関係とは 論理関係は λ計算の項の間の2項関係で, 型でインデックスがついている(つまり型を含めれば3項関係). 論理関係は「論理的」な関係である(Curry-Howard的な意味で). すなわち,論理関係とは R(s1, t1, T1->T2) かつ R(s2, t2, T1) …

プログラムの等価性と型

ATTAPLの6章は 論理関係という方法を使ったプログラムの等価性検査について書いてある.6.3節では, 前準備として, 基本型がプログラムの等価性に影響を与える場合について述べている.ここではλ計算にUnit型を入れてプログラムの等価性を議論している. Unit…

型レベルプログラミングの会

ここ読んでいる人で知らない人はいないと思いますが、 型レベルプログラミングの会 というものが開催される予定で、 既に満員で、場所も決まっていて、すごい感じです。 いろいろとすごい人とか一度会ってみたかった人とかPPLでお世話になった人とかがいらっ…

型レベルプログラミング会議

ぜひやりたいですね! ただ、私は他の言語で何ができるのかイマイチ私はよくわかってないのですが そんな界隈が(国内で?)存在しうるという時点ですごい。開催地は普通に東京が良いんでしょうねえ。

PPL2009 のみかいにて

マジメな話は省略、主に自分の話だけメモ飲み会は2日目だけ参加しました。 kinabaさん→id:osiire さん、 「リストの重複を省く関数(多相的)を作るときに Setモジュールが使えない」 OCaml の Set モジュールが多相的に使えない問題。 let uniq xs cmp = let …

A full implementation of Session Types

π計算の型に セッション型というのがあって、そいつを Haskell上に実装して PPL2009 で発表しました。 ソースコードはこちら 発表論文はこちら 質問 なぜ Associated Types や Type Families ではなく Functional Dependencies か? 他の言語に応用可能か? …

MacPortsでlablgtk2をインストールするときはFindlibに手動で登録しよう

背景 MacPorts は、 OCaml周りのいろんなライブラリのダウンロード・ビルド・インストールを "port install パッケージ名" 一発でこなしてくれる。 Findlib に、 OCaml のライブラリを登録しておけば、 "ocamlfind ocamlc -package パッケージ名" で パッケ…

Alloyでパックマン

Alloyを使ってみた。 数年前に使ったときはなんでこんなの使うのと思っていたけど考えが変わったのだ。 ちょっとした規模のプログラムを書くには設計が必要だ。 コードを書く前に、問題の本質的な部分を知っておこう。 本質がわかっていれば、 適切な部分に…

dateコマンド と crontab の コマンドライン中の %(パーセント)記号

FAQだろうけど、 crontabの話 crontab の標準出力を 日付入りファイル名で保存 30 2 * * * pdumpfs /backups/latest /backups >/backups/backup-`date '+%Y%m%d%H%M'`.txtという crontabを書いた。 2時30分に pdumpfsを起動し、 その標準出力を backup-20090…

新しく Windows XP を インストールする時にやること(Shell Foldersの変更)

ほとんどカスタマイズしないんですがこれだけはなぜかやっている。 ジャンクションを使って Documents and Settings とか デスクトップ とか My Documents の別名を作成してそれを使う。 特に日本語フォルダ名が化けたり、空白を含むパスをうまく扱えないツ…