[Paper, ICFP09] ICFP09 papers: review 2

by syoyo

[Paper, ICFP09] ICFP09 papers: review1 の続きです.

A Universe of Binding and Computation

束縛(binding)と計算(computation)をミックスしたデータ型をサポートする論理フレームワークを作り上げます.
依存的に型付けされたプログラミング言語 Agda 2 の世界(universe)でこれを実装します.
well-scoped な de Brujin incides を用いて、束縛を代名詞的(pronominally)に表現します.つまり型は変数のスコーピングに関する理由(reason)として使うことができます.

weakening, substitution, exchange, contraction and subordination-based strengthening のデータ型ジェネリックな実装が我々の世界では用意されます.
したがってプログラマは彼らが定義する言語において、自由にこれらの操作を使うことができます.
我々のミックスされて代名詞的な設定のもとでは、weakning と substituion は型のいくつかの条件の元でのみ有効であり、しかしこれらの制約条件は多くの場合自動で解放させることもできることを示します.

最後に、この研究の分野から、いろいろなよくある困難なテストケース、たとえば型無しラムダ計算の評価による正規化(normalization-by-evaluation)などをプログラムし、クリーンかつ簡潔なコードを保ちつつも、プログラムの型の中で変数の利用についての詳細な不変性を表現できることを示します.

(コメント) まだいったいどんなことができる論文なのか私の知識では分かりません.

Attribute Grammars Fly First-Class: How to do aspect oriented programming in Haskell

アトリビュート文法(attribute grammar)プログラムは二つの軸に分解することができます. 関数軸(function axis)とデータ軸(data axis)です.その結果、これらは用意に適応させたり拡張させたりすることができます.

問題は、プログラミングに対してのアトリビュート文法のアプローチが組み込みドメイン固有言語(embedded domain specific language, EDSL)として Hasnell に実装することができるかどうかです .

本論文では、これらが型クラスの機構を広く利用することで達成することができることを示します.
本論文は、アトリビュート文法の固有の性質を見つけ出し、それらをエミュレートする方法を示し、いままでの試みが持っていたいくつかの問題を克服する方法を示します.

最後に、どのようにアトリビュート文法プログラミングにおいて見つかる共通のパターンが明示的に得られ、それが我々の EDSL の主要な拡張となっているかを示します.

(コメント) んー? aspect 指向プログラミングを Haskell で実現する手法っぽい.

… 残り 28 papers くらいです.

Advertisements