著者

松本 宗太郎 南出 靖彦

出版者

一般社団法人情報処理学会

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.49, no.3, pp.39-54, 2008-03-15

参考文献数

9

---

本研究では,多相レコード型に基づいてRubyプログラムの型推論ツールを設計,実装した.型推論ツールは,組み込みライブラリの型を記述したシグネチャとRubyプログラムを入力とし,プログラムの型を推論し,誤りを検出する.しかし,Rubyの柔軟性を表現できる,実用的で健全な型体系を設計しようとすると,体系は非常に複雑になる.それを避けるため,多相レコード型によって拡張されたMLの型推論アルゴリズムを,直接,Rubyに適用した.型体系は,非常に制限されたRubyプログラムに対しては,健全になるように設計した.Rubyにおいては,組み込みクラスなどの既存のクラスを拡張することが許されており,実際に多くのプログラムで既存のクラスが拡張されている.このようなプログラムを処理するために,シグネチャとプログラムを分離して型推論するのではなく,プログラムの一部としてシグネチャが含まれるよう型体系を設計した.実際のRubyプログラムを型付けする場合には,多相レコード型の表現力やMLの型推論アルゴリズムにおける再帰的な定義の型推論に関する多相性の制限から,いくつかの問題が生じることが分かった.これらの制限は,特に組み込みライブラリの型付けにおいて問題になることから,クラス定義を複製し展開することによって型推論を行った.We design and implement a type inference tool for Ruby programs. The type system is based on polymorphic record types of Garrigue. The tool takes two inputs, a type signature of the built-in classes and a Ruby program, and then infers the type of the Ruby program and detect type errors. The type system is a direct adaptation of that of ML with polymorphic records, and designed to be sound only for a restricted tiny subset of Ruby. Ruby allows programmers to modify existing classes and many programs actually modify existing (built-in) classes. Thus we design our type system so that type signatures and method implementation coexist in a class definition. We encounter difficulties when typing common Ruby programs, since polymorphic methods are not expressible in our type system and the ML type inference does not infer polymorphic types in recursive definitions. We alleviate these difficulties by introducing transformations that duplicate class definitions.