kmizuの日記

プログラミングや形式言語に関係のあることを書いたり書かなかったり。

Crystalの型システムで遊んでみた

この記事はCrystal Advent Calendar 2015 23日目の記事です。

まず最初にお断りしておきますが、私はCrystal言語に関しては初心者もいいところです。じゃあなぜCrystal Advent Calendarにわざわざ参加したかというと、Crystalは実用言語としてはやや特殊な静的型システムをもっており、静的型スキーの自分にとって面白くうつったからです。なお、Crystalの型システムについて正確に知りたい場合, Crystalの型とメソッドについてのドキュメントの方がよほど参考になるかと思います。

typeof(X)

Crystalにはtypeof式というものがあり、引数に与えた式の型をClass型のオブジェクトとして返してくれます。この記事では、Crystalの色々な式をtypeofに渡すことで、Crystalの型システムを探検してみたいと思います。

全ての値はオブジェクト（オブジェクトにのみ型がつく）

CrystalではRubyと同様、全ての値は（オブジェクト指向言語における）オブジェクトです。そして、オブジェクトにのみ型がつきます。これは、実用オブジェクト指向言語ではかなり珍しい型システムだと思います。

たとえば、Array#mapメソッドについて考えてみます。普通の静的型付きオブジェクト指向言語では、mapメソッドにおおむね次のような型を割り当てることでしょう（なお、配列の要素型についてはT型が割り当てられているものとします）：

map: forall U. (T -> U) -> Array(U)

これは、型引数Uに対して、Tを受け取ってUを返す関数（Rubyでいうブロック）を渡すと、要素型がUのArrayが返ってくるということを意味しています。細かい型の表記法の違いを除けば、Scalaでも

http://www.scala-lang.org/api/2.11.7/index.html#scala.collection.immutable.List@mapB:List[B])

Javaでも

C#でも

https://msdn.microsoft.com/ja-jp/library/bb548891(v=vs.110).aspx

基本的な部分はだいたい同じです（これらの言語ではいずれもメソッドを値として取り出すことはできませんが）。

しかし、Crystalではmapメソッドの定義の時点では型が付きません。では、どこで型が付くかというと、mapメソッドを呼び出した結果に対して初めて型が付くのです。呼び出した結果に対して型がつくというのが重要です。

試しに次のようなCrystalプログラムを実行してみましょう。

def a_method(obj)
  if false
    obj + obj
  end
  obj
end
puts typeof(a_method(1))
puts typeof(a_method(1.0))
puts typeof(a_method("Hoge"))
#puts typeof(a_method(true))

a_methodでは引数として受け取ったオブジェクトの型を出力だけして、その他には何も行いません（obj + objは決して実行されない）。このプログラムを実行すると、

Int32
Float64
String

と表示されます。これは、a_methodが引数の型ごとにインスタンス化されていることを示しています。

一方、最後の行のコメントを外すと、次のような型エラーが出ます

Error in ./hoge.cr:10: instantiating 'a_method(Bool)'

puts typeof(a_method(true))
            ^~~~~~~~

in ./hoge.cr:3: undefined method '+' for Bool

    obj + obj
        ^

================================================================================

Bool trace:

  ./hoge.cr:1

    def a_method(obj)
                 ^

ポイントは、a_method(true)の呼び出し先のフローまで探索し、Bool + Boolのようなメソッドが存在しない事がわかってからコンパイルエラーにしている点です。これは、Crystalがプログラムのグローバルな解析を行っているからこそ可能になっています（なお、if false ...endで囲んであるのは、実行時エラーでないことを示すためです）。

ところで、プログラムのグローバルな解析を前提にしたこのような型システム、分割コンパイルを言語仕様レベルで妨げている気がするのですが、プログラムの規模が大きくなったとき、果たして大丈夫なのでしょうか...。

Union型

Crystalは、制御フローによって結果の型が変わるようなプログラムも扱うことができます。たとえば、次のようなCrystalプログラム

a = nil
puts typeof(a)
if true
  a = "r < 5"
  puts typeof(a)
else
  a = 1
  puts typeof(a)
end

puts typeof(a)

は、次のような結果を表示します。

Nil
String
(String | Int32)

最初のputsでは、aは必ずnilに初期化されるのでNil型に、その次のputs(ifの条件式がtrueなので必ずこちらが実行される）では、文字列が代入されるのでString、最後のputsでは、if式の実行結果次第で型が変わるので（elseが決して実行されないのはこのケースでは自明だが、一般には実行時にならないとわからない）、StringまたはInt32のどちらかの型をあらわすUnion型String | Int32になります。

このように、Crystalでは制御フローに依存した型をUnion型を用いて表現することができます。

型注釈

Crystalではメソッドの引数および返り値の型を書かなくても可能な限り頑張って推論してくれますが、その結果、わけのわからないコンパイルエラーのトレースに悩まされる可能性もあります。Crystalでは引数および返り値の型を明記することmもできます。

例えば、次のようなプログラム

def plus(a : Number, b : Number) : Number
  a + b
end
plus(1, 2)
plus(true, false)

は次のようなコンパイルエラーになります。

Error in ./hoge.cr:5: no overload matches 'plus' with types Bool, Bool
Overloads are:
 - plus(a : Number, b : Number)

plus(true, false)
^~~~

plusメソッドが(Number, Number)を受け取って、Numberを返すメソッドであることを明記したことによって、plusの呼び出し先でコンパイルエラーになるのを防げています。

ちなみに、型注釈を外すと次のようなコンパイルエラーになります。

Error in ./hoge.cr:5: instantiating 'plus(Bool, Bool)'

plus(true, false)
^~~~

in ./hoge.cr:2: undefined method '+' for Bool

  a + b
    ^

================================================================================

Bool trace:

  ./hoge.cr:1

    def plus(a, b)
             ^

plusメソッドの呼び出し先まで表示されるので型エラーの原因がわかりにくくなっています。

共変と反変

Crystalでは配列はジェネリックな型を持ちます。たとえば、

["A", "B", "C"]

の型はArray(String)型になります。さて、ここで気になるのは、ジェネリックな型同士の関係は一体どうなるのかということです。まずは、共変の場合についてです。

def covariant(arr : Array(Object))
  # arr[0] = 1
  puts typeof(arr)
end
arr = ["A", "B", "C"]
puts typeof(arr)
covariant(arr)

メソッドcovariantは引数としてArray(Object)を受け取りますが、それに対してArray(String)を渡そうとしています。結果は次のようになります。

Array(String)
Array(String)

コンパイルが通ったので、配列の要素型は共変な型になっているのかとも思いましたが、メソッド内部でも型がArray(String)のままなので、どうもそうではなく型引数のObjectが単純に無視されているようです。念のため、反変型引数の場合についても試してみましたが、やはり型注釈がスルーされているようです：

def contravariant(arr : Array(Object)) : Array(String)
  arr
end

contravariant(["A", "B", "C"])

この点について、Crystalのドキュメントを読んでも納得の行く解釈が得られなかったので、識者の方には、この挙動の意味について教えていただけると助かります。

停止しない式の型？

Crystalの型チェッカはどうやら、制御フローも見て型を決定しているようなので、こういう式はちゃんと型がつくのか？というので試してみました：

def f(exp)
  if exp.is_a?(Array(Int32))
    f(Array(String).new(1))
  elsif exp.is_a?(Array(String))
    f(Array(Float32).new(1))
  elsif exp.is_a?(Array(Float32))
    f([1])
  else
    1
  end
end
puts typeof(f([1]))

このプログラム、fを実際に呼び出すと無限に再帰してしまいますが、typeofの結果は…

Int32

てっきり型チェッカが停止しなくなるかと期待（？）したのですが、ちゃんと停止した上で、何故かInt32が推論されました。ちなみに、

def f(exp)
  if exp.is_a?(Array(Int32))
    f(Array(String).new(1))
  elsif exp.is_a?(Array(String))
    f(Array(Float32).new(1))
  elsif exp.is_a?(Array(Float32))
    f([1])
  else
    f(1)
  end
end
puts typeof(f([1]))

のようにすると、評価結果が返ってこない式の型をあらわすと思われるNoReturnになります。

Crystalには他にもtypeofを使った魔術の例が載っているのですが、型推論のアルゴリズムがいまいち判然としませんね…。

ともあれ、Crystalはプログラムのグローバル解析を利用した、凄まじく柔軟な型付けを行っていることが確認できました。今後、Crystalを実用で使うことがあるかはわかりませんが、玩具としては丁度いいのではないかと思えてきました(^^: