Type Checking Ruby Programs with Anntations

RubyKaigi 2017で話す内容です。


当日使ったスライドを公開します。

Type Checking Ruby Programs with Annotations // Speaker Deck

多すぎて飛ばした分も入っています。全体の内容としては、この記事を読めばほとんどそれで良いんじゃないかと思います。


さて、まずは「Rubyプログラムを型検査する」とはどういうことなのかを考えましょう。ご存じの通り、Rubyというのはすでに型安全な言語です。この場合に、型検査をしてなにをしたいのかは、いまいち自明ではありません。

型安全性とは「型検査をパスしたプログラムを実行しても、未定義の状態にならない」という性質です。Rubyのような型なしの言語を考える場合には「常に成功する型検査をする」と考えます。Rubyは、Cなどと違って、実行中に未定義の状態になることはありません。配列の範囲外にアクセスすれば nil になることが定義されていますし、存在しないインスタンス変数にアクセスしたときにも nil が得られることが定義されています。メソッドがなければ NoMethodError が発生することも定義されています。

自明ではないので、適当に都合が良さそうなものを定義しましょう。こんな感じでどうでしょうか。

  • 型検査をパスしたRubyプログラムを実行しても、 NoMethodErrorArgumentError が発生しないこと

この性質を「Rubyプログラムの型検査の健全性」と言うことにして、型検査ツールの開発ではこれを目指すことにします。

実際には、

raise NoMethodError

とかプログラム中に書くこともできるので、この定義には問題がありますが、まー

"".map {|x| ... }
1 + "3"

みたいな明らかに型検査ではじいてしまいたいようなプログラムは上手く取り扱えるので良いことにしましょう。

Rubyプログラムを型検査したいと思った人たち

Rubyプログラムを型検査したいというのは、最近になって考え出された新しいアイディアではなくて、少なくとも10年くらい前からは考えている人がいます。とりあえず、FurrとMatsumotoの論文があります。

  • 2007, S. Matsumoto and Y. Minamide. Type Inference for Ruby Programs based on Polymorphic Record Types
  • 2008, M. Furr, J. hoon (David) An, J. S. Foster, and M. Hicks. Static Type Inference for Ruby

Matsumotoというのは私です。Furrはちょっとどういう人なのかわからなかったのですが、多分Fosterさんのところにいた学生だと思います。Fosterさんはまた後で出てくるので覚えておいてください。

この人たちは、Rubyプログラムを型検査しようと思っていたのですが、Rubyというのは型なしのプログラミング言語なので、ソースコード中には型が書いてありません。なんとかするために「型推論」と呼ばれるテクノロジーで立ち向かいました。そして負けました。(火曜日にはもう少し説明するつもりです。)

なぜ負けたのでしょうか?どうすれば勝てるのでしょうか?

ここまでの話は、「型検査」について次のようなゴールを暗黙に仮定していました。

  • 正しいこと(健全性)
  • Rubyプログラムを実行しないこと
  • 型推論によって既存のRubyプログラムをそのまま検査できること

これで負けたので、勝てるようなゲームに前提条件を変えるのが良いでしょう。それぞれの条件を緩めて、

  • 正しくなくても良いことにする
  • 実行しながら型検査しても良いことにする
  • 既存のRubyプログラムに型を書いてから検査して良いことにする

というのを考えてみましょう。

正しくなくても良いかもしれない

「型検査は健全であって欲しい」というのが、全ての型検査器を開発する人間の思いですが、別に「健全でないと何の役にも立たない」ということもありません。

「健全ではないけどなんとなく便利に使える」というなんらかのツールを作る方法があります。こういうツールは、

  • TypeScriptの様な「だいたい健全だけど現実のために一部を諦めた」ものから
  • RuboCopの様な「雰囲気でルールを追加していく」もの

まで、まーいろいろと考えられると思います。

個人的には、あんまり興味がありません。Rubyでこれを始めると、多分なにもわからなくなって結局 -cw になるか、それ以上を頑張ろうとするとRuboCopになると思います。

実行しながら型検査しても良いことにする

「実行せずに型検査しようとするから難しくなるのであって、実行しながら型検査すれば良いのではないか」というアイディアです。さっき出てきたFosterさんのチームは、実行せずに型検査する戦略にさっさと見切りを付けて、ずっとこれをやっています。

  • 2016, B. M. Ren and J. S. Foster. Just-in-Time Static Type Checking for Dynamic Languages

POPLとかPLDIとか、超有名な国際会議で発表されている話で、とてもすごい。

def foo(x)
  "".bar if x
end

素のRubyはあるメソッドを呼び出した瞬間に初めてチェックが行われて、そのメソッドがなかったら NoMethodError を上げるという処理を行います。これだと例えば上のプログラムを foo false としたときには、エラーにはなりません。これをそのちょっと前、具体的には foo が呼び出された瞬間に検査することにするという話だと思います。(すみません。全然きちんと読んでいません。)

そうすると

  • 素のRubyよりは網羅的に検査するので foo false でも問題が検出できる
  • 実行時の検査なので String#bar を追加するようなメタプログラミングにも対応ができる

という嬉しさがあります。嬉しくなさとしては、

  • 実行時の環境に依存するので、ユニットテストとかで変なライブラリが追加されていたりすると変なことが起きるのでは??

と思いますが、まー現実的にはこれは問題にならないとは思います。

既存のRubyプログラムに型を書いてから検査して良いことにする

ここからが本題です。

Steep

型を書いて検査するツールを作りました。

READMEにはウソしか書いてないので、注意してください。(今から直します。)

RubyGemにはなっているので

$ gem install steep --pre

とするとインストールできます。

さっそく型検査をしてみましょう。Steepでプログラミングするには、まず型定義が必要です。適当なファイル hello.rbi などに、次のように書いてください。

class Conference
  def initialize:(name: String, year: Integer) -> any
  def name: -> String
  def year: -> Integer
end

def initialize: の後に : が必要なのが抜けていたのを直しました。

Conference というクラスを定義して、nameyearというメソッドがあることがわかります。

これを実装する前に、このクラスを使うプログラムを書いてみましょう。適当に test.rb などとファイルを作ってください。

# @type const Conference: Conference.module
# @type var year: Integer

conference = Conference.new(name: :RubyKaigi, year: 2017)
year = conference.name

型注釈は二つです。Conferenceという定数とyearというローカル変数の型を宣言しています。定数の注釈が必要なところが特徴です。このプログラムには(わざと)エラーが含まれていて、Conference.newnameSymbolを指定しているところと、Integerのはずのyearに文字列を代入しようとしているところがエラーです。

$ steep check -I hello.rbi test.rb
test.rb:4:13: ArgumentTypeMismatch: type=Conference.module, method=new

Conference.newの引数の型が合わないというエラーが見つかりました。しかし、yearの代入ではエラーになっていません。これは、conferenceの型がanyになってしまっているからです。conferenceの型アノテーションはないので、右辺から推論しようとします。ところが右辺の型は全くわからないままだったので、anyになってしまったというわけです。

anyというのは型なしの言語をシミュレーションするための型で、要するに「なんでもあり」です。なんでもありなので、Integerに変換することもできてしまいます。:RubyKaigi"``RubyKaigi``"に直すとどうなるでしょう。

$ steep check -I hello.rbi test.rb
test.rb:5:0: IncompatibleAssignment: lhs_type=Integer, rhs_type=String

今度はちゃんと代入でエラーが見つかりました。この辺りはローカル型推論とかGradual Typing呼ばれる話と大体一致していると思います。

クラスの実装はこんな感じになります。

class Conference
  # @implements Conference

  attr_reader :name
  attr_reader :year

  def initialize(name:, year:)
    @name = name
    @year = year
  end
end

@implementsというのが新しい注釈で、このクラスがシグネチャで与えられたクラスを実装していることを示します。これがあると、

  • メソッドの型をシグネチャから調べて引数や返り値の型を検査する
  • シグネチャにあるメソッドが全部定義されているかチェックする

などの処理をします。検査してみましょう。

$ steep check -I hello.rbi hello.rb
hello.rb:1:0: MethodDefinitionMissing: module=Conference, method=name
hello.rb:1:0: MethodDefinitionMissing: module=Conference, method=year

nameyearのメソッド定義がないと怒られてしまいました。Steepはattr_readerを理解しないのでこういうことがおきます。このためには@dynamicという注釈が用意しています。これを使いましょう。

  # @dynamic name
  attr_reader :name
  # @dynamic year
  attr_reader year

これで検査ができました。

これだけではつまらないので、一つメソッドを追加します。

class Conference
  def initialize: (name: String, year: Integer) -> any
  def name: -> String
  def year: -> Integer
  def succ: -> instance
end 

ここの initialize:が抜けていた……

succメソッドで、次の年のカンファレンスを返すようにしてみましょう。 instanceというのは、このクラスのインスタンスの型です。この場合はConferenceと書いても良いのですがselfを返すようなメソッドだと、意味が違ってきます。

class Conference
  ...
  def succ
    Conference.new(name: name, year: year+1)
  end
end

検査します。

$ steep check -I hello.rbi hello.rb
$

上手く検査できたように見えますが、本当でしょうか?全部の式の型を見るために --dump-all-types というオプションも用意してありますが、ここでは--fallback-any-is-errorを使いましょう。

Steepのanyには、二つの意味があります。

  • なんでも良い型を示す
  • 上手く型を付けられなかったときに先に進めるために使う

後者は、どちらかと言えば型エラーに近いはずなので、表示したい気持ちにもなります。

$ steep check --fallback-any-is-error -I hello.rbi hello.rb
hello.rb:15:4: FallbackAny

見つかりました。これがなにかというと、Conferenceという定数の参照でした。Conferenceがここでなんの値になるのかは、プログラム全体を実行してみないとわからないので、Steepにはなんとも言えません。もちろん私たちはこれがConferenceクラスを表す定数であると信じていますので、注釈を追加して対応します。

class Conference
  ...
  # @type const Conference: Conference.module
  ...
end

これで型検査ができました。

工夫

Structural SubtypingとかLocal Type Inferenceの話は省略します。まーいいでしょう。

工夫は、

  • 型と実装は全く別のものとして定義して、その二つの関連づけはユーザーの責任に押しつける

という点です。

先に見せたように、Steepは定数とクラスの関連づけすら行いません。これはRubyの性質として、定数になにが代入されているかはプログラム全体を見ないとわからないし、プログラム全体を見ると言うことはどのタイミングで実行されるのかも考える必要があるしで、要するのこの辺が難しいというところです。そして、それを全部プログラマに押しつけることによって解決を図ります。機械にやらせるのは難しいことでも、人間のプログラマーは大体自分でできる程度の知性を持っているので、まーそんなに困らないんじゃないですかね……

メタプログラミングも、上で見たattr_readerにように、一切を無視します。実際のところ、

あるメソッドを読んだときに、最初の1回はメソッドがないけど2回目ではメソッドが追加されている

みたいなことは希です。希なので、そのクラスの実装を外側から観察したときには、大体型が付けられるはずで、@dynamicのような注釈を用意しておけばそれなりに上手くやっていけるんじゃ無いかと思います。

この辺りの直感とか@dynamicという名前には、Objective Cでの経験が反映されています。

エクステンション

シグネチャには、classとかmoduleとかを用意してありますが、最後の一つはextensionです。これは、要するにC#とかObjective CとかSwiftのアレだと思ってもらえば良くて、既存のクラスにメソッドを生やすためものです。

Steepのシグネチャではクラスやモジュールは開かれていません。オープンクラス的なものでメソッドを追加するにはextensionを使います。

extension Object (Pathname)
  def Pathname: (String) -> Pathname
end

今の実装では、エクステンションは常に有効です。↑のようなPathnameエクステンションを定義したら、常にPathnameが呼べることになります。これは不便なので、選択的に有効にするような方法を用意したいと思っています。

Rubyを直さないとできないこと

Steepは、Ruby処理系とは別のソフトウェアとして実装されていて、注釈はコメントで書くようになっていますが、この先、Rubyを拡張しないとできないことがいくつかあります。

  • 注釈をRubyプログラムの式としてかっこよく書く
  • 実行時に、本当にアノテーションが正しいか検査する

前者はまあ自明だと思うのでおいておいて、後者の話はというと、 Object#is_a?は継承の関係を見ているだけなのでStructural SubtypingなSteepの意味と違っていて役に立たない、という話です。Structural Subtypingの関係をテストする述語が欲しいのですが、そのためには実行時にメソッド定義の型を全部引っ張って回らないといけないので、けっこう大がかりな改修になるんじゃないかと思います。少なくとも、僕が自分で実装しようとは思わない程度には難しそうです。

その他

Steepの機能としては

  • Union Typeがあるので便利!
  • メソッドのオーバーローディングがそのまま型として書けるようになっていて便利
  • interfaceというのを定義できるようになっているので、クラスじゃないやつもなんとかするよ!

などあります。

(でもまだ全然実装はいろいろぶっ壊れているので、動かなくても失望しないでください……)