はじめに
Idrisという、Haskellに似ていて、依存型 dependent type を持っている言語がある。依存型を持った言語なんて他にもあるのだけれども、Idrisは general purpose を謳っている。わざわざ汎用って謳っているあたり、依存型ってのはもっと色々に使えるものなんだぞって主張があるように思う。
そんなIdrisなんだけど、日本語による文献はとても少ない。今のところ、Idrisをやろうって人はまず英語のチュートリアル読まなきゃいけない。僕はIdris初心者でまだIdrisらしいプログラミングがどんなものか分からないのだけれども、日本語による学習ノートを残しておこうと思う。もしかしたらデタラメ書いてるかもしれないので、はてブかTwitter @mandel59で教えて下さい。
Idris
Idris チュートリアル (英文) Programming in Idris
ハロー、依存型プログラミングの世界
型も値だ
依存型ってのは「型が値に依存」しているってことなんだけど、それは一旦忘れよう。まず、Idrisにおいては型も値です。これを覚えて下さい。つまり、型が出てくる式は、別に普通の式と区別が無いってことです。（ここでゆっくりとした動作でIdrisを立ち上げる）
~$ idris
____ __ _
/ _/___/ /____(_)____
/ // __ / ___/ / ___/ Version 0.9.9
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
/___/\__,_/_/ /_/____/ Type :? for help
Idris> 42
42 : Integer
Idris> Integer
Integer : Type
Idris> Haskellとは : と :: が逆だから注意してね。型注釈が : でリストやベクトルのコンストラクタが :: だからね。
42と入力すると、評価されて値がInteger型の42となる。じゃあIntegerを評価するとどうなるの? というのがその次で、Integerの型はTypeになっている。
じゃあTypeの型はなんなんだよって思った方いらっしゃると思うんですけど、ちょっと説明面倒なので後回し。
依存型
the という函数を見てみよう。
Idris> the Nat 42 42 : Nat
theのひとつめの引数に型を指定すると、「指定された型だけを取る」id函数になる。ok? つまり the Nat : Nat -> Nat ってわけ。42はIntegerだけど、Idrisはこれを fromInteger 42と解釈します。なので結局Nat型の42が返ります。
theの型を調べよう。
Idris> :t the Builtins.the : (a : Type) -> a -> a
(a : Type) -> a -> a なんて変な型が出てきた。 (a : Type) というのは名前付きの引数だ。これは引数の名前がaで引数の型はTypeであるということを表している。そして続く a -> a は、引数aで渡された値に依存する型である。つまり、最初の引数の値に依存して、返される値の型が決まる。このように値に依存した型を依存型という。
the函数を使うと、型を指定できるので、REPL上だと曖昧さのせいでうまく行かない場合に使うことができる。たとえばリストを入力すると
Idris> [1, 2] Can't disambiguate name: Prelude.List.::, Prelude.Vect.::
[1, 2] は 1 :: 2 :: Nil のシンタックスシュガーなんだけど、実はIdrisのPreludeでは::がふたつ定義されているってことが分かる。リストもベクトルも [1, 2] のように表せる一方で、さきほどの42の例とは違ってこちらは型が曖昧な場面だとエラーになる。ここでthe函数を使うと
Idris> the (List Integer) [1, 2] [1,2] : List Integer
うまく行きましたね。
型推論
先ほどの例は曖昧性がある場合にはthe函数が使えるよ、という話であって、リスト使うときはいつでもthe函数を使わないといけないってことではない。Idrisには型推論があるから、リストであってベクトルではないと推論できるなら、当然指定せずとも使えるわけだ。
先ほどの例では、リストであるということだけ指定できればよかったので、Integerという指定は冗長だ。できればここは自動で推論してほしい。そんな時は、アンダースコアが使える。
Idris> the (List _) [1, 2] [1,2] : List Integer
ベクトルの場合は要素数と要素の型を指定するのだけれども、そういう場合もアンダースコアを使えばよい。
Idris> the (Vect 2 Integer) [1, 2] [1,2] : Vect 2 Integer Idris> the (Vect _ _) [1, 2] [1,2] : Vect 2 Integer
暗黙の引数
もうひとつ、idの型を調べてみる。
Idris> :t id Builtins.id : a -> a
実は、これは暗黙の引数 implicit argument があるだけで、id函数はthe函数と同じものだ。この場合、暗黙の引数は a だ。暗黙の引数があることをはっきりさせれば、id : {a : Type} -> a -> aとなって、the函数と同じものだとはっきり分かる。
暗黙の引数は通常は型推論によって補われるが、必要なら明示的に指定することもできる。明示的に指定するには、函数の直後に引数名と値を {引数名=値} のように指定する。
Idris> id 42
42 : Integer
Idris> id {a=Nat} 42
42 : Nat
