わかりやすい依存型入門その１

型について

HaskellやJavaような言語にある型システムは、以下のような役割があります。

実行前にエラーを検出する。
コンパイラの最適化を可能にする。
コードをわかりやすくする。

依存型は、プログラムが論理的に正しいかの検証をすることができます。(今度説明します)

依存型とは

依存型(dependent type)とは、値によってパラメタライズされた型です。

どういうことなのか、例を見ていきましょう。

依存型は、数学世界との親和性が高いです。

例えば、線形代数では、実数上のn次元ベクトルの集合を $\mathbb{R}^n$ と書きますね。

これをプログラム世界で考えると、n次元ベクトルを表す型を Vec n と書くことになりますが、このVecという型は、自然数(int型)の値であるnを受け取っています。

実際、Vec nはnの値次第で、Vec 0やVec 1になるわけです。これが依存型です。

標準のHaskellではMaybe Intのように型が型引数を受け取ることはあっても、値を受け取れることはありませんでした(Maybe 0なんて型はありませんね)。

(Just 0)は型ではなく値であることに注意してください。この先、型と値の違いを意識してください。

ベクトルを定義したので内積も定義しましょう。数学世界では、ベクトルの内積は $\mathbb{R}^n × \mathbb{R}^n \rightarrow \mathbb{R}$ の写像です。

これを型で考えると、 Vec n -> Vec n -> Numberのようになります。(Numberは適当な数値型と考えてください)

ここに依存型の強みの1つがあります。

もし標準のHaskellで内積をつくったなら、Vec -> Vec -> Doubleのようになるでしょう(依存型がないとベクトル型はVecと書くしかありません)。その内積にVec型の値として(1,2)と(1,2,3)を渡すとどうなるでしょう。型検査は通過しますが、内積は次元の違うベクトルに対して定義されないので、実行時エラーになってしまいます。

しかし依存型で定義した型は、同じ次元のベクトルの組しか受け取りません(Vecの次元がnで固定されているので)、もしそんな引数を渡そうものなら型エラーを叩き返してくれるでしょう。

このような依存型を扱う言語には、Agda、Idris、Coqなどがあります。

上の例じゃなくても、長さnのList型List nとか n×m行列型Mat n mとかでも同じ説明ができますね。

次回に続くかも