Qiita
You are not logged in to any team
Log in to Qiita:Team...
Community
List of all usersList of all organizatioinsAdvent Calendar
Qiitadon (β)
Community GuidelineHow to write good articles
Sign upLog in
1473692660 @reki2000
Edited at
エムスリー Advent Calendar 2017 Day 17

JEP 286 を調べていたはずなのにいつのまにか Kotlin で Hindley-Milner 型推論を実装していた

JavaKotlinコンパイラ型推論Java10

この記事は、エムスリーアドベントカレンダー2017 の 17日目の記事です。

@nishiba のガチ記事のあとで気が引けますが、最近は生後半年の娘がかわいすぎて脳が溶け、記憶力も理解力もかなり低下しているのでご容赦ください。

はじめに

さて、エムスリーでは、今、世間にも増して Kotlin が熱いです。参加メンバーも熱いです。アプリもフロントもサーバサイドもやれるポテンシャル、確かにありますね、そう、Kotlinなら。

とはいえ、まだまだ Java ベースのシステムも多いのは事実で、Javaのコーディングストレスを軽減する別案としての Alt-Java のニーズは、もう10年以上、Groovy, Scala, Kotlin と数年ごとに対象を変えながら盛り上がりを見せてきました。

Alt-Java に行かず Java の世界でも、Lombok や Play1 の黒魔術が Java の未来を垣間見せたりする中、本家 Java も ダイヤモンド演算子や Lambda、Stream API など緩やかに進化してきました。IDEも頑張っています。ばかばかしいとはいえ自動生成できるので、ゲッタセッタ書くのが面倒などという必要はありません。

……が、いうまでもなく、Java の進化はほかの言語に比べて緩やかすぎました。

Java9 の時点でも、私が Java のコードがほかの Alt Java 言語に比べてもっとも「つらい」と感じるのは、変数の宣言のたびに、都度、変数名の前に型を明記させられるところです。コードを書く流れ的にIDEが補完できないので痛いところです。

Optional<Map<String, List<String>>> myMap = Optional.of(new HashMap<>());

……ごちゃっと感がつらい、つらすぎます。

しかし、ついに Java のコードがスッキリする時が来ました。

JEP 286: Local-Variable Type Inference です。

2018/03/20 にGA予定の Java10 に入るとのことで、全然遠くない未来です！ これで Kotlin の体感にちょっと近づきますね！（言い過ぎ）

286と聞くと反射的に16bit感がするのは気のせいです。

JEP 286 の概要

  • ローカル変数の初期化で var を使うことができる
    • クラスのフィールドやメソッド引数には使えない
    • for の index には使える for (var hoge : hoges) 1
  • コンパイラが適切な型を推論し、その型に置き換えたバイトコードを出力するので、バイトコードレベルでは違いはない
  • 再代入不可のための val は提供されないが、final var で再代入不可にできる
  • 以下のような、右辺の型が推測できないような初期化はできない
varで型推論できない例
  var list = { 1, 2, 3 };              // new int[] { 1, 2, 3 }; ならOK
  var list = Collections.emptyList();  // Collections.<String>emptyList() ならOK
  var func = x -> x + 1;               // これが推論できないのはまあわかる
  var func = () -> "abc";              // 頑張って Supplier<String> に推論 …… というのはたしかに難しい
  var func = String::trim;             // Function<String, String> と推論せよというのもつらい

おかげでこんなコードが

BufferedReader reader = new BufferedReader(new InputStreamReader(errorStream, Charsets.UTF_8));
StringBuilder sb = new StringBuilder();
Optional<Map<String, List<String>>> myMap = Optional.of(new HashMap<>());

こんな風になります！！！

var reader = new BufferedReader(new InputStreamReader(errorStream, Charsets.UTF_8));
var sb = new StringBuilder();
var myMap = Optional.of(new HashMap<String, List<String>>());

素敵すぎる！！

……あれ、最後の行のみたいにわざとスゴい例をあげないとそこまでうれしくないのかもしれない

とはいえ、変数の登場位置がそろうというのは、地味だけど読みやすさに大きく貢献します。

以前、実案件で lombok2 の var を検討したときは、その不安定性から採用をあきらめましたが、今度こそ var を使える日が来そうです。

型推論すばらしい！

型推論 Deep Dive

私はコンピュータサイエンスはちゃんと学んだことのない野良エンジニア3なのですが、型推論について興味が出てきたので、調べてみることにしました。

初めの一歩は Wikipedia 様から

Wikipedia - 型推論

var のことだけを型推論と言っちゃいけないよ、などとあります。確かに。ふむふむ。

もう少し情報量がほしいので英語のページも見てみます。

Wikipedia英語版 - Type Inference

なにやら Hindley Miler Type System を勉強すべし、と言われている気がしてきました。よし、 Hindley Milner Type System も読破だ！

おっと…… そっ閉じ……

というわけにも行かず、のけぞりつつ読んでいくと、

  • 1969年に Hindley先生が、1978年に Milner先生がそれぞれ独自に発表した型システム。通称HM
    • Milner 先生は ML (SML や OCaml の原型) をつくった偉い人
    • 50年前(UNIXのリリースより前!) にこういうこと考えていたというスゴさ
  • 「多相型付きラムダ計算」の型システムの一種である。
    • 多相 とは List<T> みたいに不明な型を含む型のこと
    • HMは パラメトリック多相 であって アドホック多相 ではないとか、型クラスはパラメトリック多相で表現できるらしいとか少しわかってきた気もしましたが、うかつなことを書くといろいろマサカリが飛んできそう
    • オブジェクト指向ちっくな「継承」はできない
  • この型システムを使えば、型に関するヒントがなくても、ラムダ式だけから適切な型が推論できる
  • 型推論アルゴリズムとして Algorithm W があり、これを使うと必ず適切な型が推論できることが証明されている

手ごわいのでいくつか日本語の記事をあさってみました。

やっていることのイメージをつかむにはよかったです。

こちらは Scala の神、Odersky先生のコードだそうですが、「もともとわかっている人向け」っぽくて、文章自体、何を言っているのかサッパリわからなかったです…… 4

Scala だけではなくいろいろな言語で型推論器が書かれているので、あさっていくうちに少しずつ理解できてきました。

これらのソースをもとに、実際に型推論する処理の動作をひとつひとつ手でトレースしてみて、ようやく内容がつかめました。

せっかくなので、今熱い Kotlin に移植してみました。

https://github.com/reki2000/hyndley-milner-kotlin/blob/master/HindleyMilner.kt

Kotlin力が足りずいろいろ苦労しましたが、何とか完成！それぞれの関数の役割について理解できたことをコメントに追記しています。

アルゴリズムの動作を理解する

準備部分

構文木の要素の定義

今回の型推論の対象となる構文木は上記の要素からなります。Term と名付けましたが Syntax とかでもよかったかもしれません。

  • Lamdaが関数定義
  • Idが変数やリテラル
  • Applyが関数適用（関数の呼び出し）
  • Letが値の変数への束縛（よくある a=5 みたいなの）
  • Letrec が再帰ありの束縛（定義のなかで自分自身を参照する）
sealed class Term()
data class Lambda(val v: String, val body: Term) : Term()
data class Id(val name: String) : Term()
data class Apply(val fn: Term, val arg: Term) : Term()
data class Let(val v: String, val defn: Term, val body: Term) : Term()
data class Letrec(val v: String, val defn: Term, val body: Term) : Term()

人にやさしい言語で書いたコードからこの構文木への変換は、単純な置き換えなのですがすこし面倒です。

例えば以下のような式を構文木に置き換えてみましょう。

if (n == 0) 1 else (n - 1)

数値計算部分をガチで組むと別の世界にいってしまうので、ゼロ判定してくれる zero と、 1 減算してくれる prev という関数を導入します。

if (zero(n)) 1 else prev(n)

木構造を明確にするためLISP風に書き下します。

(lambda n (if (zero n) 1 (prev n)))

今回の構文木では、関数は引数を一つしか取れないので全部カリー化します

(lambda n (((if (zero n)) 1) (prev n)))

lambda 以外は、全部のカッコの中身が 関数 - 引数 の 2つだけの要素の並びになっているはずです。

ここまでくるとそのまま今回の構文木に変換できます。カッコを全部 Apply にして、リテラルを全部 Id にします。

Lambda("n", 
   Apply(Apply(Id("if"), 
       Apply(Id("zero"),Id("n"))),
       Id("1")),
       Apply(Id("prev"),Id("n")))))

パーサーを作れば元のような記述をこのような形に変換するところまでできるのですが、今回は自分でこのような構文木を書いて推論器に渡してやることになります。

型の表現

つづいて型をあらわすクラス群（ややこしい表現……）の定義です。

  • Type が型全体をあらわすためのクラス
  • TypeVariable が、具体的な型が不明な型変数。instance に推論結果が入ります。変数名を表示するときのために a とか b とか適当な名前をつけるしくみを持っています。
  • TypeOperator は、一つまたは複数の型の組み合わせからなる型
  • Function : TypeOperator の一種で、関数型。from と to を持つ
  • INTEGER, BOOLEAN : いうまでもなく数値型と真偽型
  • UNKNOWN : まだ具体的な型がわかっていないことを示すマーカー。TypeVariable の instance にセットする

// 型にかかわる要素（型変数、型演算子）の定義
sealed class Type()
var nextVariableName: Char = 'a'
class TypeVariable() : Type() {
    override fun toString(): String {
        if (name == "") {
            name = "${nextVariableName++}" // 変数名を表示するときに無駄にアルファベットを消費しない工夫
        }
        return name
    }
    var name: String = ""
    var instance: Type = UNKNOWN
}

open class TypeOperator(val name: String, val types: List<Type>) : Type() {
    override fun toString() = name + " " + types.map { it.toString() }.joinToString(" ")
}

// 具体的な型をいくつか定義する
class Function(name: String, types: List<Type>) : TypeOperator(name, types) {
    constructor(fromType: Type, toType: Type) :  this("->", listOf(fromType, toType))
    override fun toString() = types[0].toString() + "->" + types[1].toString()
}

val INTEGER = TypeOperator("int",  emptyList())
val BOOLEAN = TypeOperator("bool", emptyList())
val UNKNOWN = TypeOperator("unknown", emptyList())

推論部分

analise(): 推論フローの制御部分

関数名(analyse)はたぶんフランス語です。

構文木の要素に応じて、推論の処理をすすめます。

環境(env)は、その時点までに定義されている Id のもつ型(Type)への Map です。

  • Id は 環境にその名前が登録されていれば、その内容の型
  • Function は推論することはなく、「(引数の型) -> (関数本体の戻り値) という関数型だ」という結果を返す
  • Let も推論することはなく、束縛した変数を環境に追加して本体部分を評価した結果をそのまま返す
  • Letrec も Let に似ているが、本体部分を評価するまえに変数の型を推論する必要がある。（ちょっとここはまだ理解が不十分）

推論の上で重要な働きをするのは、Apply （関数の適用）の処理です。

「apply される関数の型」 と、「(apply する 引数の型) -> (結果の型) という関数の型」 が一致しなければならない ということを利用し、これらを後で登場する unify にかけていくことで不明な型変数の型を一つずつ特定していきます。

次にでてくるunifyは (結果の型) の instance に推論結果をセットしてくれます。

fun analyse(node: Term, env: Map<String, Type>, nonGeneric: Set<Type> = emptySet()): Type {
    return when (node) {
        is Id -> getType(node.name, env, nonGeneric)
        is Apply -> {
            val funType = analyse(node.fn, env, nonGeneric)
            val argType = analyse(node.arg, env, nonGeneric)
            val resultType = TypeVariable()
            unify(Function(argType, resultType), funType)
            resultType
        }
        is Lambda -> {
            val argType = TypeVariable()
            val resultType = analyse(node.body, env + (node.v to argType), nonGeneric + argType)
            Function(argType, resultType)
        }
        is Let -> {
            val defnType = analyse(node.defn, env, nonGeneric)
            analyse(node.body, env + (node.v to defnType), nonGeneric)
        }
        is Letrec -> {
            val newType = TypeVariable()
            val newEnv = env + (node.v to newType)
            val defnType = analyse(node.defn, newEnv, nonGeneric + newType)
            unify(newType, defnType)
            analyse(node.body, newEnv, nonGeneric)
        }
    }
}

unify(): 推論のコア部分

いくつかの補助処理を飛ばして(fresh がなぜ必要かまだよく理解できていない）、本体部分です。

右辺 t1 と左辺 t2 は同じ型 という条件のもと、t1, t2 の中に不明な型変数があらわれたら反対側の辺の型を代入していくという動作をします。

prune は、型変数がでてきたらその instance の型で置き換える、というのを、まだ推論できていないものがでてくるまで繰り返す処理です。

fun unify(t1: Type, t2: Type) {
    val a = prune(t1)
    val b = prune(t2)
    if (a is TypeVariable) {
        if (a != b) {
            if (occursInType(a, b))
                throw Exception("recursive unification")
            else
                a.instance = b
        }
    } else if (a is TypeOperator && b is TypeVariable) {
        unify(b, a)
    } else if (a is TypeOperator && b is TypeOperator) {
        if (a.name != b.name || a.types.count() != b.types.count()) {
            throw Exception("Type mismatch ${a} != ${b}")
        }
        a.types.zip(b.types).forEach { (p,q) -> unify(p, q) }
    }
}

実際の動作を追ってみる

先ほどの関数の fn n -> if zero(n) 1 else prev(n) の型を推論してみます。

LISP 風表記だと (lambda n (((if (zero n) 1) (prev n))) です。

中で出てくる if と zero と prev の型は定義しておく必要があるので、以下とします。

if: bool -> x -> x -> x
zero: bool -> int
prev: int -> int

この関数の型、最終的に推論したい型ですが、これをを不明な型 a? とします。この項は関数定義 Lambda なので、引数の n を別の不明な型 b? として環境 env に追加し、body の推論を進めます。

(lambda n ((if (zero n)) 1) (prev(n))) : a?
        n: b?

body の最上位の項は Apply です。関数部分が ((if (zero n)) 1) で引数が (prev n) です。この項の結果の型を c? としつつ、まずは関数部分の推論を進めます。

(lambda n ((if (zero n)) 1) (prev(n))) : a?
        n: b?
          ((if (zero n)) 1): c?

次も Apply 、関数部分は (if (zero n)) 、引数は 1 です。この項の結果の型を d? としつつ、関数部分の推論を進めます。

(lambda n ((if (zero n)) 1) (prev n))) : a?
        n: b?
          ((if (zero n)) 1) (prev n)): c?
           (if (zero n)) 1): d?

次も Apply、関数部分は if、 引数は (zero n) です。関数部分の型はわかっているので、引数 (zero n) の評価に進みます。おっと、この項の結果は e? にしておきます。

(lambda n (((if (zero n) 1) (prev(n))) : a?
        n: b?
          (((if (zero n)) 1) (prev n)): c?
           ((if (zero n)) 1): d?
            (if (zero n): e?

また Apply です。関数部分 zero の型は int -> bool です。引数 n の型は b? です。ここでようやく unify の出番です。

この項の結果を f? とすると、int -> bool が b? -> f? と等しいわけなので、b: int 、f: bool とわかります。以降、確定した型は ? を除いて書くことにします

(lambda n (((if (zero n) 1) (prev(n))) : a?
        n: b?
          (((if (zero n)) 1) (prev n)): c?
           ((if (zero n)) 1): d?
            (if (zero n)): e?
                (zero n): f?

                int -> bool === b? -> f?
                b: int
                n: int
                f: bool

引数の型が bool とわかったのでひとつ前 (if (zero n)) に戻ります。if の型 bool -> x -> x -> x と 今回の適用全体の型である bool -> e? が等しいので、e: x -> x-> x であることがわかります。

(lambda n (((if (zero n) 1) (prev(n))) : a?
        n: int
          (((if (zero n)) 1) (prev n)): c?
           ((if (zero n)) 1): d?
            (if [bool]  ): e?

            bool -> x -> x -> x === bool -> e?
            e: x -> x -> x

もうひとつ上 ((if (zero n)) 1) に戻ります。引数 1 の型は int なので、x -> x -> x と int -> d が等しい。ゆえに x: int 、d: int -> int ということがわかります

(lambda n (((if (zero n) 1) (prev(n))) : a?
        n: int
          (((if (zero n)) 1) (prev n)): c?
           ([x -> x -> x] int): d?

            x -> x -> x === int -> d?
            x: int
            d: x -> x 
            d: int -> int

一番最初にもどります。引数 (prev n) の型 g? は prev が int -> int 、 n はすでに n: int でした。よって unify の対象は int -> int と int -> g。 よって g: int

(lambda n (((if (zero n) 1) (prev(n))) : a?
        n: int
          ([int -> int]     (prev n)): c?
                            (prev n): g?

                             int -> int == int -> g?
                             g: int

ようやく body の型がわかります。 int -> int が int -> c? に等しい。c: int ということがわかります。

(lambda n (((if (zero n) 1) (prev(n))) : a?
        n: int
          ([int -> int]     [int]): c?

            int -> int == int -> c?
            c: int

引数の n は int だったので、最終的に知りたかった関数の型は int -> int ということがわかりました！

(lambda [int] ([int]) : a?

            a: int -> int

いやー型推論って大変ですね……

動作確認

実際に作ったコードを動かして試してみます。

fun factorial(n) = if (n == 0) 1 else n * factorial(n - 1)
factorial(5)

に相当する letrec 構文木を作り推論してみた結果は……

int

ちゃんと int と推論してくれました！スゴイ

Lambda("n", Lambda("m", Id("5"))

はa->b->int です！ おおー

今後

継承を含む型システムでの推論はどうなってるんだろう、と、もうすこし勉強しようと思っていたところ、タイムリーに OCaml でも採用されているレベルベースの多相型型推論とは という記事が公開されていました！言語実装 Advent Calendar なんてあったの知らなかったよ！！

まとめ

  • JEP 286 楽しみ
  • Kotlin 書くの楽しい
  • 型推論は大変。コンパイラやIDEに感謝しよう
  • 型推論に興味が出てきたら HM推論器の Algorithm W から入門するとよさそう
  • JEP 286 の話のはずが脱線しすぎ

参考記事

JEP 286: Local-Variable Type Inference

First Contact With ‘var’ In Java 10

  1. hoge の複数形って hoges?  ↩

  2. Lombok での var の実現手段は lombok.var というクラスでした。内部では、AST（抽象構文木）のツリーをたどり、このクラスの変数宣言をしているノードが出てきたら、右辺の値の型を推論して、その型を宣言するようなノードに書き換えていたようです。 ↩

  3. @gakuzzzz 先生に借りた TaPL本を2年かけて5章までしか読み進められなかったのはナイショです。一応、全ページを見ることは見た ↩

  4. 文中のソースコードに誤植（欠け）がありました。原文は Scala by example (PDF) で、こちらのソースコードは大丈夫でした。 ↩

  5. 上原さーんお元気ですか？ waba の時はお世話になりました。もう20年前ww ↩

Report article

Help us understand the problem. What is going on with this item?


Feedback

We don't reply to any feedback.
If you need help with Qiita, please send a support request from here.