研究

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

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

カバレッジテストの自動化

いきなり何を言い出すのかと思われるかもしれないが、最近はCやJavaのソースコードを解析してカバレッジテストを自動化する方法を調べている。 私、この分野に関しては全くの素人なので、何か知っている人はぜひコメント欄や twitter (@keigoi) で教えて欲し…

full-sessions-0.6.1

full-sessionsの新バージョン 0.6.1 を HackageDBにアップロード しました。 full-sessions は、Haskellにおけるマルチスレッド/ネットワークプログラミングのライブラリです。 Sessionモナドという新しいモナドを使ってプログラムを書きます。 チャネルの型…

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つとして研究されてきました(文献リスト(一部)).並行・分散ソフトウェアの普及を鑑みるに,セッション型のような仕組みは次世代の型安全かつ表現力の高いプログラミングのため…

A full implementation of Session Types

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