Hatena::Groupocaml-nagoya

yoshihiro503の関数的日記

2009-12-13 (Sun)

オブジェクト指向言語モデルFJのラムダ計算への埋め込みを使ったFJへの構造的部分型の導入

| 21:02 | オブジェクト指向言語モデルFJのラムダ計算への埋め込みを使ったFJへの構造的部分型の導入 - yoshihiro503の関数的日記 を含むブックマーク はてなブックマーク - オブジェクト指向言語モデルFJのラムダ計算への埋め込みを使ったFJへの構造的部分型の導入 - yoshihiro503の関数的日記

Rubyなどの動的型を持つオブジェクト指向言語は便利でお手軽なため多岐に利用されているが, 静的なチェックがないために単純なミスによる不具合(バグ)が起こることがある. でも静的なチェックによってRubyの柔軟性が失われることは嫌だ.

本文書ではなるべくRubyの柔軟性を生かしつつ, しかしより高信頼なプログラム開発を実現する検証器を実装するために型システムを考えた. この検証器を使えば、存在しないメソッドの呼び出しや引数の数の間違いを防ぐだけでなく, インターフェイス記述によって大規模開発や拡張を可能とすると考えている.

この型システムを使えば次の様なコードが検証できる. 次のFJコードの例を見てみよう.

まずDuckとCarというclass定義したとする.

class Duck
  def sound
    'クワックワッ'
  end
  def swim
    ...
  end
end
class Car
  def sound
    'ブーブー'
  end
  def putOil(oil)
    ...
  end
end

クラスともsoundというメソッドを持っている. ここで, 引数で与えられたオブジェクトのsoundメソッドを呼ぶ関数を次の様に定義した.

def test(x)
  puts x.sound
end

このとき以下の実行は両方共有効なはずである.

test(new Duck)
test(new Car)

Javaなどの静的型チェックはこのようなコードをはじいてしまうが、本型システムはこれを型付け可能である. もちろんメソッドの呼び出しが定義されていない場合は型エラーである.

前回同様TeXで書いた。

http://www.itpl.co.jp/ocaml-nagoya/index.php?plugin=attach&refer=%C8%AF%C9%BD%BB%F1%CE%C1&openfile=doc2.pdf

2009-12-07 (Mon)

オブジェクト指向言語モデルFJのラムダ計算への埋め込み

| 23:05 | オブジェクト指向言語モデルFJのラムダ計算への埋め込み  - yoshihiro503の関数的日記 を含むブックマーク はてなブックマーク - オブジェクト指向言語モデルFJのラムダ計算への埋め込み  - yoshihiro503の関数的日記

2009-05-07を読んで「オブジェクト指向言語より関数型言語の方が表現力が高い」と思ったので証明してみた。

OO言語モデルはこのまえid:keigoiさんと飲んだときに教えてくれたFJ(Featherweight Java)を使用した。そして、関数型言語モデルはおなじみラムダ計算レコード不動点演算を入れた単純拡張ラムダ計算(λ+と呼ぶ)を利用した。

2節ではFJサーベイし、3節ではλ+をサーベイする。そして4節で埋め込み関数定義し、それがうまいこと行ってることを証明した。

証明とかはハテダよりTeXの方が書きやすかったのでTeXで書いてみた。http://www.itpl.co.jp/ocaml-nagoya/index.php?plugin=attach&refer=%C8%AF%C9%BD%BB%F1%CE%C1&openfile=doc.pdf