読者です 読者をやめる 読者になる 読者になる

kmizuの日記

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

Klassic開発日誌(2016/11/20): Hindley-Milner型推論はじめました

以前、

kmizu.hatenablog.com

という記事を書いたことがあったのですが、このときはまだ多相型を実装しておらず、Dynamicという謎の型でごまかしていましたが、その辺の制限をとっぱらいましたという話です。

型推論というと、最近はやりの言語はだいたい型推論を持っているとか言われそうだけど、それは誤解なのです(といいつつ、自分も長いものには巻かれろ的な感じで、そういう意味で型推論という言葉を使うことがよくありますが…)。おそらく、そういう方の思い浮かべる型推論というのは、

val x = expression //x: typeOf(expression)として推論される

というようなexpressionの型を単にそのままxの型として付与するというようなものだと思います。

このようなものはより一般には(たぶん)局所型推論(local type inference)と呼ばれ、型推論のごく限定的なパターンでしかありません。

型推論アルゴリズムとしておそらく最も著名で、その後色々なアルゴリズムの基盤になったものに、Hindley-Milnerの型推論アルゴリズムがあります。これは、先程のように単方向なものでなく、双方向に推論が行われます。

たとえば、現在(2016/11/20)、Klassicのプログラムで階乗は次のように書けます。

def fact(x) = {
  if(x < 2) 1 else n * fact(n - 1)
}

このfact関数の型は、引数の型も返り値の型もいっさい書いていないにも関わらず、Int => Intと推論されます。これは、Hindley-Milnerの型推論アルゴリズムを使うと、そういう感じの推論がされるようになります。

Hindley-Milnerの型推論の原理については、ぐぐれば色々情報が出て来ると思いますが、Standard ML, OCaml, HaskellとかはいずれもHindley-Milner(の拡張)なので、同様のプログラムを型注釈いっさいなしで書くことができます。

ともあれ、これでようやく多相型が動き始めたので多相型がないと書きづらい標準関数とかも整備し始めています。headとかtailとかconsとかその他色々。