Idrisのどん語を解読する

Idrisは超ざっくり言うと文法はHaskellにそっくりで機能的にはCoqに近い、依存型を使う言語です。Idris自体の簡単な紹介は前に書いたスライドがあるので、興味がある方はそっちを読んでみてください。

yoda-jp.hatenablog.com

今回は Type Driven Development with Idris に出てくる練習問題の中で、ちょっとシュールなものを紹介しようと思います。 

問題

以下のシグネチャを持つ関数 same_lists を実装してみましょう。

--- 関数のシグネチャ
same_lists : {xs : List a} -> {ys : List a} -> x = y -> xs = ys -> x :: xs = y :: ys
--- ここに実装を書く

シグネチャが既に実装みたいになってますが、シグネチャでしかありません。 x = y と xs = ys の2つが関数の受け取る値の型で、 x::xs = y::ys が返り値の型です。

{} で囲まれているのは暗黙的な引数で、呼び出し時に渡す必要はありません。 今回は xs = ys が（明示的な）引数にあるので、わざわざ xs や ys を個別に渡す必要はないということです。

この関数のやっていることを言葉で説明すると List a 型の値xsと List a 型の値 ysについて、x = y かつ xs = ys が成り立っていれば、x::xs = y::ys が成り立つ ということになります。

同じもの同士をくっつけているので同じになるのはわかるんですが、プログラムとして書けと言われるとｳｯとなりますね。

解答

実装はこんな感じになります。

same_lists : {xs : List a} -> {ys : List a} -> x = y -> xs = ys -> x :: xs = y :: ys
same_lists Refl Refl = Refl

Refl …

この実装は「関数の引数が Refl と Refl であれば Refl を返す」としか言ってません。

もう一度言うと、この関数が指しているのは List a 型の値xsと List a 型の値 ysについて、x = y かつ xs = ys が成り立っていれば、x::xs = y::ys が成り立つ ということです。

これじゃ どんでんの「そらそうよ」 か田舎のおばちゃんの会話レベルで色々すっ飛ばされているので、ちゃんと順を追って見てみようと思います。

解説

前提知識

まず x = y について考えてみます。これは2つの値をとる型を中置で書いたものという風に見てください。一般的なプログラミング言語でも型に対して型をパラメータで渡す（ List String など）ことは多いと思いますが、Idris では型に値を含めることができます（これが依存型）。たとえば 1 = 1 という型が存在するわけです。そして Refl は x = x という型の値を作ることのできる、ただひとつのコンストラクタです。Refl は x をパラメータとしてとるわけではなく、型推論で必要なxを判定して自動的に x = x 型の値を作ります。

ではこの知識を元に、答えの Refl 連発まで導いてみましょう。

導出

Atom + Idris プラグインの人は各行程をショートカットキーで行えるので、それも一緒に書いておきます。

シグネチャの暗黙的な引数は無視して、とりあえず1つ目のパラメータ（x=y 型の値）と2つ目のパラメータ（xs=ys 型の値）に対応する変数 prf と prf1 を置きます。答えはまだわからないので ?result としています（ホールといいます）。ショートカットは Ctrl+Alt+a です。

same_lists : {xs : List a} -> {ys : List a} -> x = y -> xs = ys -> x :: xs = y :: ys
same_lists prf prf1 = ?result

次に prf と prf1 を Refl に置き換えます。Maybe a のパラメータを Just a や Nothing と書けるように、x = y や xs = ys もコンストラクタの Refl として表すことができます。ショートカットはCtrl+Alt+c （を2回）です。

same_lists : {xs : List a} -> {ys : List a} -> x = y -> xs = ys -> x :: xs = y :: ys
same_lists Refl Refl = ?result

値を Refl で書くことは非常に重要です。なぜなら、x = y 型の値ではなく、Refl と書くことで Idris の型チェッカーから以下の推論が可能になるからです。

• 関数が受け取る値の型は x = y である
• x = y 型の値はコンストラクタ Refl によって作られている
• Refl で作られた値の型は x = x である
• したがって x = y は x = x と表すことができるはずであり、 y は x に置き換えることができる

Idris はこのように型レベルで同じと判定できる値を見つけると、内部的に型の値を書き換えていきます（この様子はステップの前後で Ctrl+Alt+t をすると確認できます）。

つまり、Idris からは関数のシグネチャは以下のように見えています。

same_lists : {xs : List a} -> x = x -> xs = xs -> x :: xs = x :: xs
same_lists Refl Refl = ?result

最終的に返したい値の型は x :: xs = x :: xs になりました。これは左辺と右辺が同じなので、返したい値のところに Refl と書くだけで推論して x::xs = x::xs 型の値を作ることができます。ショートカットは Ctrl+Alt+s です。

same_lists : {xs : List a} -> x = x -> xs = xs -> x :: xs = x :: xs
same_lists Refl Refl = Refl

無事ゴールまでたどり着けましたね。

パターンマッチはプログラミング言語の標準的な機能となりつつありますが、ただ値を分解してくれるだけではなくて、そこから値同士の関係性を導き出して関数全体を簡単にしていくというのは依存型ならではかなと思います。依存型すごい（書けるとは言っていない）。

そら（x=y で xs=ys なら）そう（x::xs=y:ys）よ。

そら、そうよ ~勝つ理由、負ける理由

Type-Driven Development with Idris